feat(Algebra/Homology): two descriptions of the derived category as a…

… localized category (#9660)

In this PR, it is shown that under certain conditions on the complex shape `c`, the category `HomologicalComplexUpToQuasiIso C c` of homological complexes up to quasi-isomorphisms, which is a localization of the category of homological complexes, is also a localization of the homotopy category. In particular, in the case of cochain complexes indexed by the integers, this means that the derived category of an abelian category `C` can be obtained either in a single step by formally inverting the quasi-isomorphisms in the category of cochain complexes, or in two steps by first passing to the homotopy category (which is a quotient category) and then formally inverting the quasi-isomorphisms in the homotopy category.

Mathlib/Algebra/Homology/Localization.lean

@@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 
+import Mathlib.Algebra.Homology.HomotopyCofiber
 import Mathlib.Algebra.Homology.QuasiIso
 import Mathlib.Algebra.Homology.HomotopyCategory
 import Mathlib.CategoryTheory.Localization.HasLocalization
+import Mathlib.CategoryTheory.Localization.Composition
 
 /-! The category of homological complexes up to quasi-isomorphisms
 
@@ -19,7 +21,7 @@ particular case of the complex shape `ComplexShape.up ℤ`.
 Under suitable assumptions on `c` (e.g. chain complexes, or cochain
 complexes indexed by `ℤ`), we shall show that `HomologicalComplexUpToQuasiIso C c`
 is also the localized category of `HomotopyCategory C c` with respect to
-the class of quasi-isomorphisms (TODO).
+the class of quasi-isomorphisms.
 
 -/
 
@@ -143,4 +145,149 @@ class ComplexShape.QFactorsThroughHomotopy {ι : Type*} (c : ComplexShape ι)
   areEqualizedByLocalization {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g) :
     AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g
 
+namespace HomologicalComplexUpToQuasiIso
+
+variable {C c}
+variable [c.QFactorsThroughHomotopy C]
+
+lemma Q_map_eq_of_homotopy {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g) :
+    Q.map f = Q.map g :=
+  (ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization h).map_eq Q
+
+/-- The functor `HomotopyCategory C c ⥤ HomologicalComplexUpToQuasiIso C c` from the homotopy
+category to the localized category with respect to quasi-isomorphisms. -/
+def Qh : HomotopyCategory C c ⥤ HomologicalComplexUpToQuasiIso C c :=
+  CategoryTheory.Quotient.lift _ HomologicalComplexUpToQuasiIso.Q (by
+    intro K L f g ⟨h⟩
+    exact Q_map_eq_of_homotopy h)
+
+variable (C c)
+
+/-- The canonical isomorphism `HomotopyCategory.quotient C c ⋙ Qh ≅ Q`. -/
+def quotientCompQhIso : HomotopyCategory.quotient C c ⋙ Qh ≅ Q := by
+  apply Quotient.lift.isLift
+
+lemma Qh_inverts_quasiIso : (HomotopyCategory.quasiIso C c).IsInvertedBy Qh := by
+  rintro ⟨K⟩ ⟨L⟩ φ
+  obtain ⟨φ, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective φ
+  rw [HomotopyCategory.quotient_map_mem_quasiIso_iff φ,
+    ← HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso]
+  exact (NatIso.isIso_map_iff (quotientCompQhIso C c) φ).2
+
+instance : (HomotopyCategory.quotient C c ⋙ Qh).IsLocalization
+    (HomologicalComplex.quasiIso C c) :=
+  Functor.IsLocalization.of_iso _ (quotientCompQhIso C c).symm
+
+/-- The homology functor on `HomologicalComplexUpToQuasiIso C c` is induced by
+the homology functor on `HomotopyCategory C c`. -/
+noncomputable def homologyFunctorFactorsh (i : ι ) :
+    Qh ⋙ homologyFunctor C c i ≅ HomotopyCategory.homologyFunctor C c i :=
+  Quotient.natIsoLift _ ((Functor.associator _ _ _).symm ≪≫
+    isoWhiskerRight (quotientCompQhIso C c) _ ≪≫
+    homologyFunctorFactors C c i  ≪≫ (HomotopyCategory.homologyFunctorFactors C c i).symm)
+
+section
+
+variable [(HomotopyCategory.quotient C c).IsLocalization
+  (HomologicalComplex.homotopyEquivalences C c)]
+
+/-- The category `HomologicalComplexUpToQuasiIso C c` which was defined as a localization of
+`HomologicalComplex C c` with respect to quasi-isomorphisms also identify to a localization
+of the homotopy category with respect ot quasi-isomorphisms. -/
+instance : HomologicalComplexUpToQuasiIso.Qh.IsLocalization (HomotopyCategory.quasiIso C c) :=
+  Functor.IsLocalization.of_comp (HomotopyCategory.quotient C c)
+    Qh (HomologicalComplex.homotopyEquivalences C c)
+    (HomotopyCategory.quasiIso C c) (HomologicalComplex.quasiIso C c)
+    (homotopyEquivalences_subset_quasiIso C c)
+    (HomotopyCategory.quasiIso_eq_quasiIso_map_quotient C c)
+
+end
+
+end HomologicalComplexUpToQuasiIso
+
 end
+
+section Cylinder
+
+variable {ι : Type*} (c : ComplexShape ι) (hc : ∀ j, ∃ i, c.Rel i j)
+  (C : Type*) [Category C] [Preadditive C] [HasBinaryBiproducts C]
+
+/-- The homotopy category satisfies the universal property of the localized category
+with respect to homotopy equivalences. -/
+def ComplexShape.strictUniversalPropertyFixedTargetQuotient (E : Type*) [Category E] :
+    Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c)
+      (HomologicalComplex.homotopyEquivalences C c) E where
+  inverts := HomotopyCategory.quotient_inverts_homotopyEquivalences C c
+  lift F hF := CategoryTheory.Quotient.lift _ F (by
+    intro K L f g ⟨h⟩
+    have : DecidableRel c.Rel := by classical infer_instance
+    exact h.map_eq_of_inverts_homotopyEquivalences hc F hF)
+  fac F hF := rfl
+  uniq F₁ F₂ h := Quotient.lift_unique' _ _ _ h
+
+lemma ComplexShape.quotient_isLocalization :
+    (HomotopyCategory.quotient C c).IsLocalization
+      (HomologicalComplex.homotopyEquivalences _ _) := by
+  apply Functor.IsLocalization.mk'
+  all_goals apply c.strictUniversalPropertyFixedTargetQuotient hc
+
+lemma ComplexShape.QFactorsThroughHomotopy_of_exists_prev [CategoryWithHomology C] :
+    c.QFactorsThroughHomotopy C where
+  areEqualizedByLocalization {K L f g} h := by
+    have : DecidableRel c.Rel := by classical infer_instance
+    exact h.map_eq_of_inverts_homotopyEquivalences hc _
+      (MorphismProperty.IsInvertedBy.of_subset _ _ _
+        (Localization.inverts _ (HomologicalComplex.quasiIso C _))
+        (homotopyEquivalences_subset_quasiIso C _))
+
+end Cylinder
+
+section ChainComplex
+
+variable (C : Type*) [Category C] {ι : Type*} [Preadditive C]
+  [AddRightCancelSemigroup ι] [One ι] [HasBinaryBiproducts C]
+
+instance : (HomotopyCategory.quotient C (ComplexShape.down ι)).IsLocalization
+    (HomologicalComplex.homotopyEquivalences _ _) :=
+  (ComplexShape.down ι).quotient_isLocalization (fun _ => ⟨_, rfl⟩) C
+
+variable [CategoryWithHomology C]
+
+instance : (ComplexShape.down ι).QFactorsThroughHomotopy C :=
+  (ComplexShape.down ι).QFactorsThroughHomotopy_of_exists_prev (fun _ => ⟨_, rfl⟩) C
+
+example [(HomologicalComplex.quasiIso C (ComplexShape.down ι)).HasLocalization] :
+    HomologicalComplexUpToQuasiIso.Qh.IsLocalization
+    (HomotopyCategory.quasiIso C (ComplexShape.down ι)) :=
+  inferInstance
+
+/- By duality, the results obtained here for chain complexes could be dualized in
+order to obtain similar results for general cochain complexes. However, the case of
+interest for the construction of the derived category (cochain complexes indexed by `ℤ`)
+can also be obtained directly, which is done below. -/
+
+end ChainComplex
+
+section CochainComplex
+
+variable (C : Type*) [Category C] {ι : Type*} [Preadditive C] [HasBinaryBiproducts C]
+
+instance : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).IsLocalization
+    (HomologicalComplex.homotopyEquivalences _ _) :=
+  (ComplexShape.up ℤ).quotient_isLocalization (fun n => ⟨n - 1, by simp⟩) C
+
+variable [CategoryWithHomology C]
+
+instance : (ComplexShape.up ℤ).QFactorsThroughHomotopy C :=
+  (ComplexShape.up ℤ).QFactorsThroughHomotopy_of_exists_prev (fun n => ⟨n - 1, by simp⟩) C
+
+/-- When we define the derived category as `HomologicalComplexUpToQuasiIso C (ComplexShape.up ℤ)`,
+i.e. as the localization of cochain complexes with respect to quasi-isomorphisms, this
+example shall say that the derived category is also the localization of the homotopy
+category with respect to quasi-isomorphisms. -/
+example [(HomologicalComplex.quasiIso C (ComplexShape.up ℤ)).HasLocalization] :
+    HomologicalComplexUpToQuasiIso.Qh.IsLocalization
+      (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) :=
+  inferInstance
+
+end CochainComplex