feat(category_theory/idempotents): an equivalence of categories for homological complexes (#17569)

This PR constructs an equivalence of categories `karoubi_homological_complex_equivalence C c :  karoubi (homological_complex C c) ≌ homological_complex (karoubi C) c`. The automation for `karoubi` categories is also made better by the introduction of the simp lemma `karoubi.comp_f`.

Author: joelriou

src/algebraic_topology/dold_kan/n_reflects_iso.lean

@@ -46,7 +46,7 @@ instance : reflects_isomorphisms (N₁ : simplicial_object C ⥤ karoubi (chain_
   have h₁ := homological_complex.congr_hom (karoubi.hom_ext.mp (is_iso.hom_inv_id (N₁.map f))),
   have h₂ := homological_complex.congr_hom (karoubi.hom_ext.mp (is_iso.inv_hom_id (N₁.map f))),
   have h₃ := λ n, karoubi.homological_complex.p_comm_f_assoc (inv (N₁.map f)) (n) (f.app (op [n])),
-  simp only [N₁_map_f, karoubi.comp, homological_complex.comp_f,
+  simp only [N₁_map_f, karoubi.comp_f, homological_complex.comp_f,
     alternating_face_map_complex.map_f, N₁_obj_p, karoubi.id_eq, assoc] at h₁ h₂ h₃,
   /- we have to construct an inverse to f in degree n, by induction on n -/
   intro n,

src/algebraic_topology/dold_kan/normalized.lean

@@ -128,12 +128,12 @@ def N₁_iso_normalized_Moore_complex_comp_to_karoubi :
   hom_inv_id' := begin
     ext X : 3,
     simp only [P_infty_to_normalized_Moore_complex_comp_inclusion_of_Moore_complex_map,
-      nat_trans.comp_app, karoubi.comp, N₁_obj_p, nat_trans.id_app, karoubi.id_eq],
+      nat_trans.comp_app, karoubi.comp_f, N₁_obj_p, nat_trans.id_app, karoubi.id_eq],
   end,
   inv_hom_id' := begin
     ext X : 3,
     simp only [← cancel_mono (inclusion_of_Moore_complex_map X),
-      nat_trans.comp_app, karoubi.comp, assoc, nat_trans.id_app, karoubi.id_eq,
+      nat_trans.comp_app, karoubi.comp_f, assoc, nat_trans.id_app, karoubi.id_eq,
       P_infty_to_normalized_Moore_complex_comp_inclusion_of_Moore_complex_map,
       inclusion_of_Moore_complex_map_comp_P_infty],
     dsimp only [functor.comp_obj, to_karoubi],

src/algebraic_topology/dold_kan/p_infty.lean

@@ -197,10 +197,10 @@ begin
   /- We use the three equalities h₃₂, h₄₃, h₁₄. -/
   rw [← h₃₂, ← h₄₃, h₁₄],
   simp only [karoubi_functor_category_embedding.map_app_f, karoubi.decomp_id_p_f,
-    karoubi.decomp_id_i_f, karoubi.comp],
+    karoubi.decomp_id_i_f, karoubi.comp_f],
   let π : Y₄ ⟶ Y₄ := (to_karoubi _ ⋙ karoubi_functor_category_embedding _ _).map Y.p,
   have eq := karoubi.hom_ext.mp (P_infty_f_naturality n π),
-  simp only [karoubi.comp] at eq,
+  simp only [karoubi.comp_f] at eq,
   dsimp [π] at eq,
   rw [← eq, reassoc_of (app_idem Y (op [n]))],
 end

src/algebraic_topology/dold_kan/split_simplicial_object.lean

@@ -224,13 +224,13 @@ def to_karoubi_nondeg_complex_iso_N₁ : (to_karoubi _).obj s.nondeg_complex ≅
     comm := by { ext n, dsimp, simp only [comp_id, P_infty_comp_π_summand_id], }, },
   hom_inv_id' := begin
     ext n,
-    simpa only [assoc, P_infty_comp_π_summand_id, karoubi.comp, homological_complex.comp_f,
-      ι_π_summand_eq_id],
+    simpa only [assoc, P_infty_comp_π_summand_id, karoubi.comp_f,
+      homological_complex.comp_f, ι_π_summand_eq_id],
   end,
   inv_hom_id' := begin
     ext n,
-    simp only [karoubi.comp, homological_complex.comp_f,
-      π_summand_comp_ι_summand_comp_P_infty_eq_P_infty, karoubi.id_eq, N₁_obj_p],
+    simp only [π_summand_comp_ι_summand_comp_P_infty_eq_P_infty, karoubi.comp_f,
+      homological_complex.comp_f, N₁_obj_p, karoubi.id_eq],
   end, }
 
 end splitting
@@ -275,9 +275,9 @@ nat_iso.of_components (λ S, S.s.to_karoubi_nondeg_complex_iso_N₁)
   (λ S₁ S₂ Φ, begin
     ext n,
     dsimp,
-    simp only [to_karoubi_map_f, karoubi.comp, homological_complex.comp_f,
-      splitting.to_karoubi_nondeg_complex_iso_N₁_hom_f_f, N₁_map_f, nondeg_complex_functor_map_f,
-      alternating_face_map_complex.map_f, assoc, P_infty_f_idem_assoc],
+    simp only [karoubi.comp_f, to_karoubi_map_f, homological_complex.comp_f,
+      nondeg_complex_functor_map_f, splitting.to_karoubi_nondeg_complex_iso_N₁_hom_f_f,
+      N₁_map_f, alternating_face_map_complex.map_f, assoc, P_infty_f_idem_assoc],
     erw ← split.ι_summand_naturality_symm_assoc Φ (splitting.index_set.id (op [n])),
     rw P_infty_f_naturality,
   end)

src/category_theory/idempotents/biproducts.lean

@@ -63,11 +63,10 @@ def bicone [has_finite_biproducts C] {J : Type} [fintype J]
   ι_π := λ j j', begin
     split_ifs,
     { subst h,
-      simp only [biproduct.bicone_ι, biproduct.ι_map, biproduct.bicone_π,
-        biproduct.ι_π_self_assoc, comp, category.assoc, eq_to_hom_refl, id_eq,
-        biproduct.map_π, (F j).idem], },
-    { simpa only [hom_ext, biproduct.ι_π_ne_assoc _ h, assoc,
-        biproduct.map_π, biproduct.map_π_assoc, zero_comp, comp], },
+      simp only [assoc, idem, biproduct.map_π, biproduct.map_π_assoc, eq_to_hom_refl,
+        id_eq, hom_ext, comp_f, biproduct.ι_π_self_assoc], },
+    { simp only [biproduct.ι_π_ne_assoc _ h, assoc, biproduct.map_π,
+        biproduct.map_π_assoc, hom_ext, comp_f, zero_comp, quiver.hom.add_comm_group_zero_f], },
   end, }
 
 end biproducts
@@ -83,15 +82,15 @@ lemma karoubi_has_finite_biproducts [has_finite_biproducts C] :
       rw [sum_hom, comp_sum, finset.sum_eq_single j], rotate,
       { intros j' h1 h2,
         simp only [biproduct.ι_map, biproducts.bicone_ι_f, biproducts.bicone_π_f,
-          assoc, comp, biproduct.map_π],
+          assoc, comp_f, biproduct.map_π],
         slice_lhs 1 2 { rw biproduct.ι_π, },
         split_ifs,
         { exfalso, exact h2 h.symm, },
         { simp only [zero_comp], } },
       { intro h,
         exfalso,
         simpa only [finset.mem_univ, not_true] using h, },
-      { simp only [biproducts.bicone_π_f, comp,
+      { simp only [biproducts.bicone_π_f, comp_f,
           biproduct.ι_map, assoc, biproducts.bicone_ι_f, biproduct.map_π],
         slice_lhs 1 2 { rw biproduct.ι_π, },
         split_ifs, swap, { exfalso, exact h rfl, },
@@ -119,12 +118,12 @@ has_binary_biproduct_of_total
   inr := P.complement.decomp_id_i,
   inl_fst' := P.decomp_id.symm,
   inl_snd' := begin
-    simp only [decomp_id_i_f, decomp_id_p_f, complement_p, comp_sub, comp,
+    simp only [decomp_id_i_f, decomp_id_p_f, complement_p, comp_sub, comp_f,
       hom_ext, quiver.hom.add_comm_group_zero_f, P.idem],
     erw [comp_id, sub_self],
   end,
   inr_fst' := begin
-    simp only [decomp_id_i_f, complement_p, decomp_id_p_f, sub_comp, comp,
+    simp only [decomp_id_i_f, complement_p, decomp_id_p_f, sub_comp, comp_f,
       hom_ext, quiver.hom.add_comm_group_zero_f, P.idem],
     erw [id_comp, sub_self],
   end,
@@ -144,14 +143,14 @@ def decomposition (P : karoubi C) : P ⊞ P.complement ≅ (to_karoubi _).obj P.
         ← decomp_id, id_comp, add_right_eq_self],
       convert zero_comp,
       ext,
-      simp only [decomp_id_i_f, decomp_id_p_f, complement_p, comp_sub, comp,
+      simp only [decomp_id_i_f, decomp_id_p_f, complement_p, comp_sub, comp_f,
         quiver.hom.add_comm_group_zero_f, P.idem],
       erw [comp_id, sub_self], },
     { simp only [← assoc, biprod.inr_desc, biprod.lift_eq, comp_add,
         ← decomp_id, comp_id, id_comp, add_left_eq_self],
       convert zero_comp,
       ext,
-      simp only [decomp_id_i_f, decomp_id_p_f, complement_p, sub_comp, comp,
+      simp only [decomp_id_i_f, decomp_id_p_f, complement_p, sub_comp, comp_f,
         quiver.hom.add_comm_group_zero_f, P.idem],
       erw [id_comp, sub_self], }
   end,

src/category_theory/idempotents/functor_categories.lean

@@ -27,7 +27,24 @@ namespace category_theory
 
 namespace idempotents
 
-variables (J C : Type*) [category J] [category C]
+variables {J C : Type*} [category J] [category C] (P Q : karoubi (J ⥤ C)) (f : P ⟶ Q) (X : J)
+
+@[simp, reassoc]
+lemma app_idem :
+  P.p.app X ≫ P.p.app X = P.p.app X := congr_app P.idem X
+
+variables {P Q}
+
+@[simp, reassoc]
+lemma app_p_comp : P.p.app X ≫ f.f.app X = f.f.app X := congr_app (p_comp f) X
+
+@[simp, reassoc]
+lemma app_comp_p : f.f.app X ≫ Q.p.app X = f.f.app X := congr_app (comp_p f) X
+
+@[reassoc]
+lemma app_p_comm : P.p.app X ≫ f.f.app X = f.f.app X ≫ Q.p.app X := congr_app (p_comm f) X
+
+variables (J C)
 
 instance functor_category_is_idempotent_complete [is_idempotent_complete C] :
   is_idempotent_complete (J ⥤ C) :=
@@ -81,32 +98,12 @@ def obj (P : karoubi (J ⥤ C)) : J ⥤ karoubi C :=
       have h := congr_app P.idem j,
       rw [nat_trans.comp_app] at h,
       slice_rhs 1 3 { erw [h, h], },
-    end },
-  map_id' := λ j, by { ext, simp only [functor.map_id, comp_id, id_eq], },
-  map_comp' := λ j j' j'' φ φ', begin
-    ext,
-    have h := congr_app P.idem j,
-    rw [nat_trans.comp_app] at h,
-    simp only [assoc, nat_trans.naturality_assoc, functor.map_comp, comp],
-    slice_rhs 1 2 { rw h, },
-    rw [assoc],
-  end }
+    end }, }
 
 /-- Tautological action on maps of the functor `karoubi (J ⥤ C) ⥤ (J ⥤ karoubi C)`. -/
 @[simps]
 def map {P Q : karoubi (J ⥤ C)} (f : P ⟶ Q) : obj P ⟶ obj Q :=
-{ app := λ j, ⟨f.f.app j, congr_app f.comm j⟩,
-  naturality' := λ j j' φ, begin
-    ext,
-    simp only [comp],
-    have h := congr_app (comp_p f) j,
-    have h' := congr_app (p_comp f) j',
-    dsimp at h h' ⊢,
-    slice_rhs 1 2 { erw h, },
-    rw ← P.p.naturality,
-    slice_lhs 2 3 { erw h', },
-    rw f.f.naturality,
-  end }
+{ app := λ j, ⟨f.f.app j, congr_app f.comm j⟩, }
 
 end karoubi_functor_category_embedding
 
@@ -117,20 +114,18 @@ variables (J C)
 def karoubi_functor_category_embedding :
   karoubi (J ⥤ C) ⥤ (J ⥤ karoubi C) :=
 { obj := karoubi_functor_category_embedding.obj,
-  map := λ P Q, karoubi_functor_category_embedding.map,
-  map_id' := λ P, rfl,
-  map_comp' := λ P Q R f g, rfl, }
+  map := λ P Q, karoubi_functor_category_embedding.map, }
 
 instance : full (karoubi_functor_category_embedding J C) :=
 { preimage := λ P Q f,
   { f :=
     { app := λ j, (f.app j).f,
       naturality' := λ j j' φ, begin
-        slice_rhs 1 1 { rw ← karoubi.comp_p, },
+        rw ← karoubi.comp_p_assoc,
         have h := hom_ext.mp (f.naturality φ),
-        simp only [comp] at h,
-        dsimp [karoubi_functor_category_embedding] at h ⊢,
-        erw [assoc, ← h, ← P.p.naturality φ, assoc, p_comp (f.app j')],
+        simp only [comp_f] at h,
+        dsimp [karoubi_functor_category_embedding] at h,
+        erw [← h, assoc, ← P.p.naturality_assoc φ, p_comp (f.app j')],
       end },
     comm := by { ext j, exact (f.app j).comm, } },
   witness' := λ P Q f, by { ext j, refl, }, }
@@ -161,24 +156,6 @@ begin
       refl, }, }
 end
 
-variables {J C} (P Q : karoubi (J ⥤ C)) (f : P ⟶ Q) (X : J)
-
-
-@[simp, reassoc]
-lemma app_idem (X : J) :
-  P.p.app X ≫ P.p.app X = P.p.app X := congr_app P.idem X
-
-variables {P Q}
-
-@[simp, reassoc]
-lemma app_p_comp : P.p.app X ≫ f.f.app X = f.f.app X := congr_app (p_comp f) X
-
-@[simp, reassoc]
-lemma app_comp_p : f.f.app X ≫ Q.p.app X = f.f.app X := congr_app (comp_p f) X
-
-@[reassoc]
-lemma app_p_comm : P.p.app X ≫ f.f.app X = f.f.app X ≫ Q.p.app X := congr_app (p_comm f) X
-
 end idempotents
 
 end category_theory

src/category_theory/idempotents/functor_extension.lean

@@ -60,7 +60,7 @@ def map {F G : C ⥤ karoubi D} (φ : F ⟶ G) : obj F ⟶ obj G :=
     comm := begin
       have h := φ.naturality P.p,
       have h' := F.congr_map P.idem,
-      simp only [hom_ext, karoubi.comp, F.map_comp] at h h',
+      simp only [hom_ext, karoubi.comp_f, F.map_comp] at h h',
       simp only [obj_obj_p, assoc, ← h],
       slice_rhs 1 3 { rw [h', h'], },
     end, },
@@ -70,7 +70,7 @@ def map {F G : C ⥤ karoubi D} (φ : F ⟶ G) : obj F ⟶ obj G :=
     have h := φ.naturality f.f,
     have h' := F.congr_map (comp_p f),
     have h'' := F.congr_map (p_comp f),
-    simp only [hom_ext, functor.map_comp, comp] at ⊢ h h' h'',
+    simp only [hom_ext, functor.map_comp, comp_f] at ⊢ h h' h'',
     slice_rhs 2 3 { rw ← h, },
     slice_lhs 1 2 { rw h', },
     slice_rhs 1 2 { rw h'', },
@@ -88,10 +88,10 @@ def functor_extension₁ : (C ⥤ karoubi D) ⥤ (karoubi C ⥤ karoubi D) :=
   map_id' := λ F, by { ext P, exact comp_p (F.map P.p), },
   map_comp' := λ F G H φ φ', begin
     ext P,
-    simp only [comp, functor_extension₁.map_app_f, nat_trans.comp_app, assoc],
+    simp only [comp_f, functor_extension₁.map_app_f, nat_trans.comp_app, assoc],
     have h := φ.naturality P.p,
     have h' := F.congr_map P.idem,
-    simp only [hom_ext, comp, F.map_comp] at h h',
+    simp only [hom_ext, comp_f, F.map_comp] at h h',
     slice_rhs 2 3 { rw ← h, },
     slice_rhs 1 2 { rw h', },
     simp only [assoc],
@@ -113,13 +113,13 @@ begin
       ext,
       dsimp,
       simp only [comp_id, eq_to_hom_f, eq_to_hom_refl, comp_p, functor_extension₁.obj_obj_p,
-        to_karoubi_obj_p, comp],
+        to_karoubi_obj_p, comp_f],
       dsimp,
       simp only [functor.map_id, id_eq, p_comp], }, },
   { intros F G φ,
     ext X,
     dsimp,
-    simp only [eq_to_hom_app, F.map_id, karoubi.comp, eq_to_hom_f, id_eq, p_comp,
+    simp only [eq_to_hom_app, F.map_id, comp_f, eq_to_hom_f, id_eq, p_comp,
       eq_to_hom_refl, comp_id, comp_p, functor_extension₁.obj_obj_p,
       to_karoubi_obj_p, F.map_id X], },
 end