feat(Algebra/Homology): compatibilities for homology functors (#35938)

We add compatibility lemmas for the comparison of the homology functors on the categories of cochain complexes, the homotopy category or the derived category.

Author: joelriou

Mathlib/Algebra/Homology/DerivedCategory/HomologySequence.lean

@@ -6,6 +6,7 @@ Authors: Joël Riou
 module
 
 public import Mathlib.Algebra.Homology.DerivedCategory.Basic
+public import Mathlib.CategoryTheory.Shift.ShiftedHom
 
 /-!
 # The homology sequence
@@ -39,12 +40,36 @@ noncomputable def homologyFunctorFactors (n : ℤ) : Q ⋙ homologyFunctor C n 
     HomologicalComplex.homologyFunctor _ _ n :=
   HomologicalComplexUpToQuasiIso.homologyFunctorFactors C (ComplexShape.up ℤ) n
 
+variable {C} in
+@[reassoc (attr := simp)]
+lemma homologyFunctorFactors_hom_naturality
+    {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ) :
+    (homologyFunctor C n).map (Q.map f) ≫ (homologyFunctorFactors C n).hom.app L =
+    (homologyFunctorFactors C n).hom.app K ≫ HomologicalComplex.homologyMap f n :=
+  (homologyFunctorFactors C n).hom.naturality f
+
 /-- The homology functor on the derived category is induced by the homology
 functor on the homotopy category of cochain complexes. -/
 noncomputable def homologyFunctorFactorsh (n : ℤ) : Qh ⋙ homologyFunctor C n ≅
     HomotopyCategory.homologyFunctor _ _ n :=
   HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh C (ComplexShape.up ℤ) n
 
+@[reassoc]
+lemma homologyFunctorFactorsh_hom_app_quotient_obj (K : CochainComplex C ℤ) (n : ℤ) :
+    (homologyFunctorFactorsh C n).hom.app ((HomotopyCategory.quotient _ _).obj K) =
+    (homologyFunctor C n).map ((quotientCompQhIso C).hom.app K) ≫
+      (homologyFunctorFactors C n).hom.app K ≫
+        (HomotopyCategory.homologyFunctorFactors C (.up ℤ) n).inv.app _ :=
+  HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj ..
+
+@[reassoc]
+lemma homologyFunctorFactorsh_inv_app_quotient_obj (K : CochainComplex C ℤ) (n : ℤ) :
+    (homologyFunctorFactorsh C n).inv.app ((HomotopyCategory.quotient _ _).obj K) =
+    (HomotopyCategory.homologyFunctorFactors C (.up ℤ) n).hom.app _ ≫
+      (homologyFunctorFactors C n).inv.app K ≫
+        (homologyFunctor C n).map ((quotientCompQhIso C).inv.app K) :=
+  HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj ..
+
 variable {C} in
 lemma isIso_Qh_map_iff {X Y : HomotopyCategory C (ComplexShape.up ℤ)} (f : X ⟶ Y) :
     IsIso (Qh.map f) ↔ HomotopyCategory.quasiIso C _ f := by
@@ -67,8 +92,38 @@ noncomputable instance : (homologyFunctor C 0).ShiftSequence ℤ :=
   Functor.ShiftSequence.induced (homologyFunctorFactorsh C 0) ℤ
     (homologyFunctor C) (homologyFunctorFactorsh C)
 
+lemma shift_homologyFunctor (n : ℤ) :
+    (homologyFunctor C 0).shift n = homologyFunctor C n := rfl
+
 variable {C}
 
+@[reassoc]
+lemma shiftMap_homologyFunctor_map_Qh
+    {K L : HomotopyCategory C (.up ℤ)} {n : ℤ} (f : K ⟶ L⟦n⟧)
+    (a a' : ℤ) (h : n + a = a') :
+    (homologyFunctor C 0).shiftMap (ShiftedHom.map f Qh) a a' h =
+    (homologyFunctorFactorsh C a).hom.app _ ≫
+      (HomotopyCategory.homologyFunctor C (.up ℤ) 0).shiftMap f a a' h ≫
+        (homologyFunctorFactorsh C a').inv.app _ :=
+  Functor.ShiftSequence.induced_shiftMap ..
+
+@[reassoc]
+lemma shiftMap_homologyFunctor_map_Q
+    {K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ L⟦n⟧)
+    (a a' : ℤ) (h : n + a = a') :
+    (homologyFunctor C 0).shiftMap (ShiftedHom.map f Q) a a' h =
+    (homologyFunctorFactors C a).hom.app _ ≫
+      (HomologicalComplex.homologyFunctor C (.up ℤ) 0).shiftMap f a a' h ≫
+        (homologyFunctorFactors C a').inv.app _ := by
+  rw [← ShiftedHom.map_naturality_1 f (quotientCompQhIso C),
+    ShiftedHom.mk₀_comp, ShiftedHom.comp_mk₀,
+    Functor.shiftMap_comp', Functor.shiftMap_comp,
+    ShiftedHom.comp_map, shiftMap_homologyFunctor_map_Qh,
+    homologyFunctorFactorsh_hom_app_quotient_obj,
+    homologyFunctorFactorsh_inv_app_quotient_obj,
+    HomotopyCategory.homologyFunctor_shiftMap]
+  simp [shift_homologyFunctor, ← Functor.map_comp, ← Functor.map_comp_assoc]
+
 namespace HomologySequence
 
 /-- The connecting homomorphism on the homology sequence attached to a distinguished

Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.CategoryTheory.Shift.InducedShiftSequence
 public import Mathlib.CategoryTheory.Shift.Localization
+public import Mathlib.CategoryTheory.Shift.ShiftedHom
 public import Mathlib.Algebra.Homology.HomotopyCategory.Shift
 public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
 public import Mathlib.Algebra.Homology.QuasiIso
@@ -203,7 +204,7 @@ lemma homologyShiftIso_hom_app (n a a' : ℤ) (ha' : n + a = a') (K : CochainCom
 lemma homologyFunctor_shiftMap
     {K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ L⟦n⟧) (a a' : ℤ) (h : n + a = a') :
     (homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap
-      ((quotient _ _).map f ≫ ((quotient _ _).commShiftIso n).hom.app _) a a' h =
+      (ShiftedHom.map f (quotient _ _)) a a' h =
         (homologyFunctorFactors _ _ a).hom.app K ≫
           (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
             (homologyFunctorFactors _ _ a').inv.app L := by

Mathlib/Algebra/Homology/Localization.lean

@@ -191,6 +191,24 @@ noncomputable def homologyFunctorFactorsh (i : ι) :
     Functor.isoWhiskerRight (quotientCompQhIso C c) _ ≪≫
     homologyFunctorFactors C c i ≪≫ (HomotopyCategory.homologyFunctorFactors C c i).symm)
 
+@[reassoc]
+lemma homologyFunctorFactorsh_hom_app_quotient_obj
+    (K : HomologicalComplex C c) (i : ι) :
+    (homologyFunctorFactorsh C c i).hom.app ((HomotopyCategory.quotient _ _).obj K) =
+    (homologyFunctor C c i).map ((quotientCompQhIso C c).hom.app K) ≫
+      (homologyFunctorFactors C c i).hom.app K ≫
+        (HomotopyCategory.homologyFunctorFactors C c i).inv.app K :=
+  (Quotient.natTransLift_app ..).trans (by simp)
+
+@[reassoc]
+lemma homologyFunctorFactorsh_inv_app_quotient_obj
+    (K : HomologicalComplex C c) (i : ι) :
+    (homologyFunctorFactorsh C c i).inv.app ((HomotopyCategory.quotient _ _).obj K) =
+    (HomotopyCategory.homologyFunctorFactors C c i).hom.app K ≫
+      (homologyFunctorFactors C c i).inv.app K ≫
+        (homologyFunctor C c i).map ((quotientCompQhIso C c).inv.app K) :=
+  (Quotient.natTransLift_app ..).trans (by simp)
+
 section
 
 variable [(HomotopyCategory.quotient C c).IsLocalization