refactor: introduce the new homology API for homological complex and …

…rename the old one (#7954)

This PR renames definitions of the current homology API (adding a `'` to `homology`, `cycles`, `QuasiIso`) so as to create space for the development of the new homology API of homological complexes: this PR also contains the new definition of `HomologicalComplex.homology` which involves the homology theory of short complexes.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Mathlib/Algebra/Homology/Additive.lean

@@ -120,8 +120,8 @@ namespace HomologicalComplex
 instance eval_additive (i : ι) : (eval V c i).Additive where
 #align homological_complex.eval_additive HomologicalComplex.eval_additive
 
-instance cycles_additive [HasEqualizers V] : (cyclesFunctor V c i).Additive where
-#align homological_complex.cycles_additive HomologicalComplex.cycles_additive
+instance cycles'_additive [HasEqualizers V] : (cycles'Functor V c i).Additive where
+#align homological_complex.cycles_additive HomologicalComplex.cycles'_additive
 
 variable [HasImages V] [HasImageMaps V]
 
@@ -130,11 +130,11 @@ instance boundaries_additive : (boundariesFunctor V c i).Additive where
 
 variable [HasEqualizers V] [HasCokernels V]
 
-instance homology_additive : (homologyFunctor V c i).Additive where
+instance homology_additive : (homology'Functor V c i).Additive where
   map_add {_ _ f g} := by
-    dsimp [homologyFunctor]
+    dsimp [homology'Functor]
     ext
-    simp only [homology.π_map, Preadditive.comp_add, ← Preadditive.add_comp]
+    simp only [homology'.π_map, Preadditive.comp_add, ← Preadditive.add_comp]
     congr
     ext
     simp

Mathlib/Algebra/Homology/Exact.lean

@@ -37,6 +37,9 @@ these results are found in `CategoryTheory/Abelian/Exact.lean`.
   categories?)
 * Two adjacent maps in a chain complex are exact iff the homology vanishes
 
+Note: It is planned that the definition in this file will be replaced by the new
+homology API, in particular by the content of `Algebra.Homology.ShortComplex.Exact`.
+
 -/
 
 
@@ -84,22 +87,22 @@ open ZeroObject
 /-- In any preadditive category,
 composable morphisms `f g` are exact iff they compose to zero and the homology vanishes.
 -/
-theorem Preadditive.exact_iff_homology_zero {A B C : V} (f : A ⟶ B) (g : B ⟶ C) :
-    Exact f g ↔ ∃ w : f ≫ g = 0, Nonempty (homology f g w ≅ 0) :=
+theorem Preadditive.exact_iff_homology'_zero {A B C : V} (f : A ⟶ B) (g : B ⟶ C) :
+    Exact f g ↔ ∃ w : f ≫ g = 0, Nonempty (homology' f g w ≅ 0) :=
   ⟨fun h => ⟨h.w, ⟨by
     haveI := h.epi
     exact cokernel.ofEpi _⟩⟩,
    fun h => by
     obtain ⟨w, ⟨i⟩⟩ := h
     exact ⟨w, Preadditive.epi_of_cokernel_zero ((cancel_mono i.hom).mp (by ext))⟩⟩
-#align category_theory.preadditive.exact_iff_homology_zero CategoryTheory.Preadditive.exact_iff_homology_zero
+#align category_theory.preadditive.exact_iff_homology_zero CategoryTheory.Preadditive.exact_iff_homology'_zero
 
 theorem Preadditive.exact_of_iso_of_exact {A₁ B₁ C₁ A₂ B₂ C₂ : V} (f₁ : A₁ ⟶ B₁) (g₁ : B₁ ⟶ C₁)
     (f₂ : A₂ ⟶ B₂) (g₂ : B₂ ⟶ C₂) (α : Arrow.mk f₁ ≅ Arrow.mk f₂) (β : Arrow.mk g₁ ≅ Arrow.mk g₂)
     (p : α.hom.right = β.hom.left) (h : Exact f₁ g₁) : Exact f₂ g₂ := by
-  rw [Preadditive.exact_iff_homology_zero] at h ⊢
+  rw [Preadditive.exact_iff_homology'_zero] at h ⊢
   rcases h with ⟨w₁, ⟨i⟩⟩
-  suffices w₂ : f₂ ≫ g₂ = 0; exact ⟨w₂, ⟨(homology.mapIso w₁ w₂ α β p).symm.trans i⟩⟩
+  suffices w₂ : f₂ ≫ g₂ = 0; exact ⟨w₂, ⟨(homology'.mapIso w₁ w₂ α β p).symm.trans i⟩⟩
   rw [← cancel_epi α.hom.left, ← cancel_mono β.inv.right, comp_zero, zero_comp, ← w₁]
   have eq₁ := β.inv.w
   have eq₂ := α.hom.w

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -803,10 +803,10 @@ theorem mk_d_1_0 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 0 = d₀ := by
 #align chain_complex.mk_d_1_0 ChainComplex.mk_d_1_0
 
 @[simp]
-theorem mk_d_2_0 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁ := by
+theorem mk_d_2_1 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁ := by
   change ite (2 = 1 + 1) (𝟙 X₂ ≫ d₁) 0 = d₁
   rw [if_pos rfl, Category.id_comp]
-#align chain_complex.mk_d_2_0 ChainComplex.mk_d_2_0
+#align chain_complex.mk_d_2_0 ChainComplex.mk_d_2_1
 
 -- TODO simp lemmas for the inductive steps? It's not entirely clear that they are needed.
 /-- A simpler inductive constructor for `ℕ`-indexed chain complexes.

Mathlib/Algebra/Homology/Homotopy.lean

@@ -781,34 +781,34 @@ variable [HasEqualizers V] [HasCokernels V] [HasImages V] [HasImageMaps V]
 
 /-- Homotopic maps induce the same map on homology.
 -/
-theorem homology_map_eq_of_homotopy (h : Homotopy f g) (i : ι) :
-    (homologyFunctor V c i).map f = (homologyFunctor V c i).map g := by
-  dsimp [homologyFunctor]
+theorem homology'_map_eq_of_homotopy (h : Homotopy f g) (i : ι) :
+    (homology'Functor V c i).map f = (homology'Functor V c i).map g := by
+  dsimp [homology'Functor]
   apply eq_of_sub_eq_zero
   ext
-  simp only [homology.π_map, comp_zero, Preadditive.comp_sub]
+  simp only [homology'.π_map, comp_zero, Preadditive.comp_sub]
   dsimp [kernelSubobjectMap]
   simp_rw [h.comm i]
   simp only [zero_add, zero_comp, dNext_eq_dFrom_fromNext, kernelSubobject_arrow_comp_assoc,
     Preadditive.comp_add]
   rw [← Preadditive.sub_comp]
   simp only [CategoryTheory.Subobject.factorThru_add_sub_factorThru_right]
-  erw [Subobject.factorThru_ofLE (D.boundaries_le_cycles i)]
+  erw [Subobject.factorThru_ofLE (D.boundaries_le_cycles' i)]
   · simp
   · rw [prevD_eq_toPrev_dTo, ← Category.assoc]
     apply imageSubobject_factors_comp_self
-#align homology_map_eq_of_homotopy homology_map_eq_of_homotopy
+#align homology_map_eq_of_homotopy homology'_map_eq_of_homotopy
 
 /-- Homotopy equivalent complexes have isomorphic homologies. -/
 def homologyObjIsoOfHomotopyEquiv (f : HomotopyEquiv C D) (i : ι) :
-    (homologyFunctor V c i).obj C ≅ (homologyFunctor V c i).obj D where
-  hom := (homologyFunctor V c i).map f.hom
-  inv := (homologyFunctor V c i).map f.inv
+    (homology'Functor V c i).obj C ≅ (homology'Functor V c i).obj D where
+  hom := (homology'Functor V c i).map f.hom
+  inv := (homology'Functor V c i).map f.inv
   hom_inv_id := by
-    rw [← Functor.map_comp, homology_map_eq_of_homotopy f.homotopyHomInvId,
+    rw [← Functor.map_comp, homology'_map_eq_of_homotopy f.homotopyHomInvId,
       CategoryTheory.Functor.map_id]
   inv_hom_id := by
-    rw [← Functor.map_comp, homology_map_eq_of_homotopy f.homotopyInvHomId,
+    rw [← Functor.map_comp, homology'_map_eq_of_homotopy f.homotopyInvHomId,
       CategoryTheory.Functor.map_id]
 #align homology_obj_iso_of_homotopy_equiv homologyObjIsoOfHomotopyEquiv
 

Mathlib/Algebra/Homology/HomotopyCategory.lean

@@ -144,34 +144,34 @@ variable (V c)
 variable [HasEqualizers V] [HasImages V] [HasImageMaps V] [HasCokernels V]
 
 /-- The `i`-th homology, as a functor from the homotopy category. -/
-def homologyFunctor (i : ι) : HomotopyCategory V c ⥤ V :=
-  CategoryTheory.Quotient.lift _ (_root_.homologyFunctor V c i) fun _ _ _ _ ⟨h⟩ =>
-    homology_map_eq_of_homotopy h i
-#align homotopy_category.homology_functor HomotopyCategory.homologyFunctor
+def homology'Functor (i : ι) : HomotopyCategory V c ⥤ V :=
+  CategoryTheory.Quotient.lift _ (_root_.homology'Functor V c i) fun _ _ _ _ ⟨h⟩ =>
+    homology'_map_eq_of_homotopy h i
+#align homotopy_category.homology_functor HomotopyCategory.homology'Functor
 
 /-- The homology functor on the homotopy category is just the usual homology functor. -/
-def homologyFactors (i : ι) :
-    quotient V c ⋙ homologyFunctor V c i ≅ _root_.homologyFunctor V c i :=
+def homology'Factors (i : ι) :
+    quotient V c ⋙ homology'Functor V c i ≅ _root_.homology'Functor V c i :=
   CategoryTheory.Quotient.lift.isLift _ _ _
-#align homotopy_category.homology_factors HomotopyCategory.homologyFactors
+#align homotopy_category.homology_factors HomotopyCategory.homology'Factors
 
 @[simp]
-theorem homologyFactors_hom_app (i : ι) (C : HomologicalComplex V c) :
-    (homologyFactors V c i).hom.app C = 𝟙 _ :=
+theorem homology'Factors_hom_app (i : ι) (C : HomologicalComplex V c) :
+    (homology'Factors V c i).hom.app C = 𝟙 _ :=
   rfl
-#align homotopy_category.homology_factors_hom_app HomotopyCategory.homologyFactors_hom_app
+#align homotopy_category.homology_factors_hom_app HomotopyCategory.homology'Factors_hom_app
 
 @[simp]
-theorem homologyFactors_inv_app (i : ι) (C : HomologicalComplex V c) :
-    (homologyFactors V c i).inv.app C = 𝟙 _ :=
+theorem homology'Factors_inv_app (i : ι) (C : HomologicalComplex V c) :
+    (homology'Factors V c i).inv.app C = 𝟙 _ :=
   rfl
-#align homotopy_category.homology_factors_inv_app HomotopyCategory.homologyFactors_inv_app
+#align homotopy_category.homology_factors_inv_app HomotopyCategory.homology'Factors_inv_app
 
-theorem homologyFunctor_map_factors (i : ι) {C D : HomologicalComplex V c} (f : C ⟶ D) :
-    (_root_.homologyFunctor V c i).map f =
-      ((homologyFunctor V c i).map ((quotient V c).map f) : _) :=
-  (CategoryTheory.Quotient.lift_map_functor_map _ (_root_.homologyFunctor V c i) _ f).symm
-#align homotopy_category.homology_functor_map_factors HomotopyCategory.homologyFunctor_map_factors
+theorem homology'Functor_map_factors (i : ι) {C D : HomologicalComplex V c} (f : C ⟶ D) :
+    (_root_.homology'Functor V c i).map f =
+      ((homology'Functor V c i).map ((quotient V c).map f) : _) :=
+  (CategoryTheory.Quotient.lift_map_functor_map _ (_root_.homology'Functor V c i) _ f).symm
+#align homotopy_category.homology_functor_map_factors HomotopyCategory.homology'Functor_map_factors
 
 end HomotopyCategory