feat: the homology functor on the homotopy category for the new API (#…

…8595)

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

Mathlib/Algebra/Homology/Homotopy.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.Algebra.Homology.Additive
+import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
 import Mathlib.Tactic.Abel
 
 #align_import algebra.homology.homotopy from "leanprover-community/mathlib"@"618ea3d5c99240cd7000d8376924906a148bf9ff"
@@ -21,7 +21,7 @@ open Classical
 
 noncomputable section
 
-open CategoryTheory CategoryTheory.Limits HomologicalComplex
+open CategoryTheory Category Limits HomologicalComplex
 
 variable {ι : Type*}
 
@@ -65,7 +65,7 @@ theorem dNext_comp_left (f : C ⟶ D) (g : ∀ i j, D.X i ⟶ E.X j) (i : ι) :
 @[simp 1100]
 theorem dNext_comp_right (f : ∀ i j, C.X i ⟶ D.X j) (g : D ⟶ E) (i : ι) :
     (dNext i fun i j => f i j ≫ g.f j) = dNext i f ≫ g.f i :=
-  (Category.assoc _ _ _).symm
+  (assoc _ _ _).symm
 #align d_next_comp_right dNext_comp_right
 
 /-- The composition `f j (c.prev j) ≫ D.d (c.prev j) j`. -/
@@ -94,14 +94,14 @@ theorem prevD_eq (f : ∀ i j, C.X i ⟶ D.X j) {j j' : ι} (w : c.Rel j' j) :
 @[simp 1100]
 theorem prevD_comp_left (f : C ⟶ D) (g : ∀ i j, D.X i ⟶ E.X j) (j : ι) :
     (prevD j fun i j => f.f i ≫ g i j) = f.f j ≫ prevD j g :=
-  Category.assoc _ _ _
+  assoc _ _ _
 #align prev_d_comp_left prevD_comp_left
 
 @[simp 1100]
 theorem prevD_comp_right (f : ∀ i j, C.X i ⟶ D.X j) (g : D ⟶ E) (j : ι) :
     (prevD j fun i j => f i j ≫ g.f j) = prevD j f ≫ g.f j := by
   dsimp [prevD]
-  simp only [Category.assoc, g.comm]
+  simp only [assoc, g.comm]
 #align prev_d_comp_right prevD_comp_right
 
 theorem dNext_nat (C D : ChainComplex V ℕ) (i : ℕ) (f : ∀ i j, C.X i ⟶ D.X j) :
@@ -224,13 +224,13 @@ def comp {C₁ C₂ C₃ : HomologicalComplex V c} {f₁ g₁ : C₁ ⟶ C₂} {
 /-- a variant of `Homotopy.compRight` useful for dealing with homotopy equivalences. -/
 @[simps!]
 def compRightId {f : C ⟶ C} (h : Homotopy f (𝟙 C)) (g : C ⟶ D) : Homotopy (f ≫ g) g :=
-  (h.compRight g).trans (ofEq <| Category.id_comp _)
+  (h.compRight g).trans (ofEq <| id_comp _)
 #align homotopy.comp_right_id Homotopy.compRightId
 
 /-- a variant of `Homotopy.compLeft` useful for dealing with homotopy equivalences. -/
 @[simps!]
 def compLeftId {f : D ⟶ D} (h : Homotopy f (𝟙 D)) (g : C ⟶ D) : Homotopy (g ≫ f) g :=
-  (h.compLeft g).trans (ofEq <| Category.comp_id _)
+  (h.compLeft g).trans (ofEq <| comp_id _)
 #align homotopy.comp_left_id Homotopy.compLeftId
 
 /-!
@@ -249,12 +249,12 @@ def nullHomotopicMap (hom : ∀ i j, C.X i ⟶ D.X j) : C ⟶ D where
   f i := dNext i hom + prevD i hom
   comm' i j hij := by
     have eq1 : prevD i hom ≫ D.d i j = 0 := by
-      simp only [prevD, AddMonoidHom.mk'_apply, Category.assoc, d_comp_d, comp_zero]
+      simp only [prevD, AddMonoidHom.mk'_apply, assoc, d_comp_d, comp_zero]
     have eq2 : C.d i j ≫ dNext j hom = 0 := by
       simp only [dNext, AddMonoidHom.mk'_apply, d_comp_d_assoc, zero_comp]
     dsimp only
     rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
-      add_zero, zero_add, Category.assoc]
+      add_zero, zero_add, assoc]
 #align homotopy.null_homotopic_map Homotopy.nullHomotopicMap
 
 /-- Variant of `nullHomotopicMap` where the input consists only of the
@@ -269,7 +269,7 @@ theorem nullHomotopicMap_comp (hom : ∀ i j, C.X i ⟶ D.X j) (g : D ⟶ E) :
     nullHomotopicMap hom ≫ g = nullHomotopicMap fun i j => hom i j ≫ g.f j := by
   ext n
   dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]
-  simp only [Preadditive.add_comp, Category.assoc, g.comm]
+  simp only [Preadditive.add_comp, assoc, g.comm]
 #align homotopy.null_homotopic_map_comp Homotopy.nullHomotopicMap_comp
 
 /-- Compatibility of `nullHomotopicMap'` with the postcomposition by a morphism
@@ -291,7 +291,7 @@ theorem comp_nullHomotopicMap (f : C ⟶ D) (hom : ∀ i j, D.X i ⟶ E.X j) :
     f ≫ nullHomotopicMap hom = nullHomotopicMap fun i j => f.f i ≫ hom i j := by
   ext n
   dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]
-  simp only [Preadditive.comp_add, Category.assoc, f.comm_assoc]
+  simp only [Preadditive.comp_add, assoc, f.comm_assoc]
 #align homotopy.comp_null_homotopic_map Homotopy.comp_nullHomotopicMap
 
 /-- Compatibility of `nullHomotopicMap'` with the precomposition by a morphism
@@ -570,9 +570,9 @@ def mkInductive : Homotopy e 0 where
         simp only [ChainComplex.next_nat_succ, dite_true]
         rw [mkInductiveAux₃ e zero comm_zero one comm_one succ]
         dsimp [xNextIso]
-        rw [Category.id_comp]
+        rw [id_comp]
     · dsimp [toPrev]
-      erw [dif_pos, Category.comp_id]
+      erw [dif_pos, comp_id]
       simp only [ChainComplex.prev]
 #align homotopy.mk_inductive Homotopy.mkInductive
 
@@ -709,9 +709,9 @@ def mkCoinductive : Homotopy e 0 where
         simp only [CochainComplex.prev_nat_succ, dite_true]
         rw [mkCoinductiveAux₃ e zero comm_zero one comm_one succ]
         dsimp [xPrevIso]
-        rw [Category.comp_id]
+        rw [comp_id]
     · dsimp [fromNext]
-      erw [dif_pos, Category.id_comp]
+      erw [dif_pos, id_comp]
       simp only [CochainComplex.next]
 #align homotopy.mk_coinductive Homotopy.mkCoinductive
 
@@ -734,6 +734,12 @@ structure HomotopyEquiv (C D : HomologicalComplex V c) where
   homotopyInvHomId : Homotopy (inv ≫ hom) (𝟙 D)
 #align homotopy_equiv HomotopyEquiv
 
+variable (V c) in
+/-- The morphism property on `HomologicalComplex V c` given by homotopy equivalences. -/
+def HomologicalComplex.homotopyEquivalences :
+    MorphismProperty (HomologicalComplex V c) :=
+  fun X Y f => ∃ (e : HomotopyEquiv X Y), e.hom = f
+
 namespace HomotopyEquiv
 
 /-- Any complex is homotopy equivalent to itself. -/
@@ -795,7 +801,7 @@ theorem homology'_map_eq_of_homotopy (h : Homotopy f g) (i : ι) :
   simp only [CategoryTheory.Subobject.factorThru_add_sub_factorThru_right]
   erw [Subobject.factorThru_ofLE (D.boundaries_le_cycles' i)]
   · simp
-  · rw [prevD_eq_toPrev_dTo, ← Category.assoc]
+  · rw [prevD_eq_toPrev_dTo, ← assoc]
     apply imageSubobject_factors_comp_self
 #align homology_map_eq_of_homotopy homology'_map_eq_of_homotopy
 
@@ -845,3 +851,65 @@ def Functor.mapHomotopyEquiv (F : V ⥤ W) [F.Additive] (h : HomotopyEquiv C D)
 #align category_theory.functor.map_homotopy_equiv CategoryTheory.Functor.mapHomotopyEquiv
 
 end CategoryTheory
+
+section
+
+open HomologicalComplex CategoryTheory
+
+variable {C : Type*} [Category C] [Preadditive C] {ι : Type _} {c : ComplexShape ι}
+  [DecidableRel c.Rel] {K L : HomologicalComplex C c} {f g : K ⟶ L}
+
+/-- A homotopy between morphisms of homological complexes `K ⟶ L` induces a homotopy
+between morphisms of short complexes `K.sc i ⟶ L.sc i`. -/
+noncomputable def Homotopy.toShortComplex (ho : Homotopy f g) (i : ι) :
+    ShortComplex.Homotopy ((shortComplexFunctor C c i).map f)
+      ((shortComplexFunctor C c i).map g) where
+  h₀ :=
+    if c.Rel (c.prev i) i
+    then ho.hom _ (c.prev (c.prev i)) ≫ L.d _ _
+    else f.f _ - g.f _ - K.d _ i ≫ ho.hom i _
+  h₁ := ho.hom _ _
+  h₂ := ho.hom _ _
+  h₃ :=
+    if c.Rel i (c.next i)
+    then K.d _ _ ≫ ho.hom (c.next (c.next i)) _
+    else f.f _ - g.f _ - ho.hom _ i ≫ L.d _ _
+  h₀_f := by
+    split_ifs with h
+    · dsimp
+      simp only [assoc, d_comp_d, comp_zero]
+    · dsimp
+      rw [L.shape _ _ h, comp_zero]
+  g_h₃ := by
+    split_ifs with h
+    · dsimp
+      simp
+    · dsimp
+      rw [K.shape _ _ h, zero_comp]
+  comm₁ := by
+    dsimp
+    split_ifs with h
+    · rw [ho.comm (c.prev i)]
+      dsimp [dFrom, dTo, fromNext, toPrev]
+      rw [congr_arg (fun j => d K (c.prev i) j ≫ ho.hom j (c.prev i)) (c.next_eq' h)]
+    · abel
+  comm₂ := ho.comm i
+  comm₃ := by
+    dsimp
+    split_ifs with h
+    · rw [ho.comm (c.next i)]
+      dsimp [dFrom, dTo, fromNext, toPrev]
+      rw [congr_arg (fun j => ho.hom (c.next i) j ≫ L.d j (c.next i)) (c.prev_eq' h)]
+    · abel
+
+lemma Homotopy.homologyMap_eq (ho : Homotopy f g) (i : ι) [K.HasHomology i] [L.HasHomology i] :
+    homologyMap f i = homologyMap g i :=
+  ShortComplex.Homotopy.homologyMap_congr (ho.toShortComplex i)
+
+/-- The isomorphism in homology induced by an homotopy equivalence. -/
+noncomputable def HomotopyEquiv.toHomologyIso (h : HomotopyEquiv K L) (i : ι)
+    [K.HasHomology i] [L.HasHomology i] : K.homology i ≅ L.homology i where
+  hom := homologyMap h.hom i
+  inv := homologyMap h.inv i
+  hom_inv_id := by rw [← homologyMap_comp, h.homotopyHomInvId.homologyMap_eq, homologyMap_id]
+  inv_hom_id := by rw [← homologyMap_comp, h.homotopyInvHomId.homologyMap_eq, homologyMap_id]

Mathlib/Algebra/Homology/HomotopyCategory.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Mathlib.Algebra.Homology.Homotopy
-import Mathlib.CategoryTheory.Quotient
+import Mathlib.Algebra.Homology.Additive
+import Mathlib.CategoryTheory.Quotient.Preadditive
 
 #align_import algebra.homology.homotopy_category from "leanprover-community/mathlib"@"13ff898b0eee75d3cc75d1c06a491720eaaf911d"
 
@@ -59,11 +60,21 @@ instance : Category (HomotopyCategory V v) := by
 -- TODO the homotopy_category is preadditive
 namespace HomotopyCategory
 
+instance : Preadditive (HomotopyCategory V c) := Quotient.preadditive _ (by
+  rintro _ _ _ _ _ _ ⟨h⟩ ⟨h'⟩
+  exact ⟨Homotopy.add h h'⟩)
+
 /-- The quotient functor from complexes to the homotopy category. -/
 def quotient : HomologicalComplex V c ⥤ HomotopyCategory V c :=
   CategoryTheory.Quotient.functor _
 #align homotopy_category.quotient HomotopyCategory.quotient
 
+instance : Full (quotient V c) := Quotient.fullFunctor _
+
+instance : EssSurj (quotient V c) := Quotient.essSurj_functor _
+
+instance : (quotient V c).Additive where
+
 open ZeroObject
 
 -- TODO upgrade this to `HasZeroObject`, presumably for any `quotient`.
@@ -141,6 +152,9 @@ def homotopyEquivOfIso {C D : HomologicalComplex V c}
 #align homotopy_category.homotopy_equiv_of_iso HomotopyCategory.homotopyEquivOfIso
 
 variable (V c)
+
+section
+
 variable [HasEqualizers V] [HasImages V] [HasImageMaps V] [HasCokernels V]
 
 /-- The `i`-th homology, as a functor from the homotopy category. -/
@@ -173,6 +187,34 @@ theorem homology'Functor_map_factors (i : ι) {C D : HomologicalComplex V c} (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
+
+section
+
+variable [CategoryWithHomology V]
+
+/-- The `i`-th homology, as a functor from the homotopy category. -/
+noncomputable def homologyFunctor (i : ι) : HomotopyCategory V c ⥤ V :=
+  CategoryTheory.Quotient.lift _ (HomologicalComplex.homologyFunctor V c i) (by
+    rintro K L f g ⟨h⟩
+    exact h.homologyMap_eq i)
+
+/-- The homology functor on the homotopy category is induced by
+the homology functor on homological complexes. -/
+noncomputable def homologyFunctorFactors (i : ι) :
+    quotient V c ⋙ homologyFunctor V c i ≅
+      HomologicalComplex.homologyFunctor V c i :=
+  Quotient.lift.isLift _ _ _
+
+-- this is to prevent any abuse of defeq
+attribute [irreducible] homologyFunctor homologyFunctorFactors
+
+instance (i : ι) : (homologyFunctor V c i).Additive := by
+  have := Functor.additive_of_iso (homologyFunctorFactors V c i).symm
+  exact Functor.additive_of_full_essSurj_comp (quotient V c) _
+
+end
+
 end HomotopyCategory
 
 namespace CategoryTheory

Mathlib/Algebra/Homology/QuasiIso.lean

@@ -220,6 +220,8 @@ end
 
 open HomologicalComplex
 
+section
+
 variable {ι : Type*} {C : Type u} [Category.{v} C] [HasZeroMorphisms C]
   {c : ComplexShape ι} {K L M K' L' : HomologicalComplex C c}
 
@@ -417,3 +419,43 @@ lemma quasiIso_of_arrow_mk_iso (φ : K ⟶ L) (φ' : K' ⟶ L') (e : Arrow.mk φ
     [∀ i, K'.HasHomology i] [∀ i, L'.HasHomology i]
     [hφ : QuasiIso φ] : QuasiIso φ' := by
   simpa only [← quasiIso_iff_of_arrow_mk_iso φ φ' e]
+
+namespace HomologicalComplex
+
+variable (C c)
+
+/-- The morphism property on `HomologicalComplex C c` given by quasi-isomorphisms. -/
+def qis [CategoryWithHomology C] :
+    MorphismProperty (HomologicalComplex C c) := fun _ _ f => QuasiIso f
+
+variable {C c}
+
+@[simp]
+lemma qis_iff [CategoryWithHomology C] (f : K ⟶ L) : qis C c f ↔ QuasiIso f := by rfl
+
+end HomologicalComplex
+
+end
+
+section
+
+variable {ι : Type*} {C : Type u} [Category.{v} C] [Preadditive C]
+  {c : ComplexShape ι} {K L : HomologicalComplex C c}
+
+section
+
+variable (e : HomotopyEquiv K L) [∀ i, K.HasHomology i] [∀ i, L.HasHomology i]
+
+instance : QuasiIso e.hom where
+  quasiIsoAt n := by
+    classical
+    rw [quasiIsoAt_iff_isIso_homologyMap]
+    exact IsIso.of_iso (e.toHomologyIso n)
+
+instance : QuasiIso e.inv := (inferInstance : QuasiIso e.symm.hom)
+
+lemma homotopyEquivalences_subset_qis [CategoryWithHomology C] :
+    homotopyEquivalences C c ⊆ qis C c := by
+  rintro K L _ ⟨e, rfl⟩
+  simp only [qis_iff]
+  infer_instance

Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean

@@ -3,8 +3,9 @@ Copyright (c) 2023 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
-import Mathlib.Algebra.Homology.HomologicalComplex
+import Mathlib.Algebra.Homology.Additive
 import Mathlib.Algebra.Homology.ShortComplex.Exact
+import Mathlib.Algebra.Homology.ShortComplex.Preadditive
 import Mathlib.Tactic.Linarith
 
 /-!
@@ -601,3 +602,32 @@ lemma isoHomologyπ₀_inv_naturality [L.HasHomology 0] :
     HomologicalComplex.isoHomologyπ_hom_inv_id_assoc]
 
 end CochainComplex
+
+namespace HomologicalComplex
+
+variable {C ι : Type*} [Category C] [Preadditive C] {c : ComplexShape ι}
+  {K L : HomologicalComplex C c} {f g : K ⟶ L}
+
+variable (φ ψ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i]
+
+@[simp]
+lemma homologyMap_neg : homologyMap (-φ) i = -homologyMap φ i := by
+  dsimp [homologyMap]
+  rw [← ShortComplex.homologyMap_neg]
+  rfl
+
+@[simp]
+lemma homologyMap_add : homologyMap (φ + ψ) i = homologyMap φ i + homologyMap ψ i := by
+  dsimp [homologyMap]
+  rw [← ShortComplex.homologyMap_add]
+  rfl
+
+@[simp]
+lemma homologyMap_sub : homologyMap (φ - ψ) i = homologyMap φ i - homologyMap ψ i := by
+  dsimp [homologyMap]
+  rw [← ShortComplex.homologyMap_sub]
+  rfl
+
+instance [CategoryWithHomology C] : (homologyFunctor C c i).Additive where
+
+end HomologicalComplex