feat(Algebra/Homology): the class of quasi-isomorphisms in the homoto…

…py category (#9686)

This PR introduces the class of quasi-isomorphisms in the homotopy category of homological complexes.

Mathlib/Algebra/Homology/HomotopyCategory.lean

@@ -154,6 +154,13 @@ def homotopyEquivOfIso {C D : HomologicalComplex V c}
       (by rw [quotient_map_out_comp_out, i.inv_hom_id, (quotient V c).map_id])
 #align homotopy_category.homotopy_equiv_of_iso HomotopyCategory.homotopyEquivOfIso
 
+variable (V c) in
+lemma quotient_inverts_homotopyEquivalences :
+    (HomologicalComplex.homotopyEquivalences V c).IsInvertedBy (quotient V c) := by
+  rintro K L _ ⟨e, rfl⟩
+  change IsIso (isoOfHomotopyEquiv e).hom
+  infer_instance
+
 lemma isZero_quotient_obj_iff (C : HomologicalComplex V c) :
     IsZero ((quotient _ _).obj C) ↔ Nonempty (Homotopy (𝟙 C) 0) := by
   rw [IsZero.iff_id_eq_zero]

Mathlib/Algebra/Homology/Localization.lean

@@ -5,56 +5,142 @@ Authors: Joël Riou
 -/
 
 import Mathlib.Algebra.Homology.QuasiIso
+import Mathlib.Algebra.Homology.HomotopyCategory
 import Mathlib.CategoryTheory.Localization.HasLocalization
 
 /-! The category of homological complexes up to quasi-isomorphisms
 
 Given a category `C` with homology and any complex shape `c`, we define
-the category `HomologicalComplexUpToQis C c` which is the localized
+the category `HomologicalComplexUpToQuasiIso C c` which is the localized
 category of `HomologicalComplex C c` with respect to quasi-isomorphisms.
 When `C` is abelian, this will be the derived category of `C` in the
 particular case of the complex shape `ComplexShape.up ℤ`.
 
-Under suitable assumptions on `c` (e.g. chain or cochain complexes),
-we shall show that `HomologicalComplexUpToQis C c` is also the
-localized category of `HomotopyCategory C c` with respect to
+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).
 
 -/
 
 open CategoryTheory Limits
 
+section
+
 variable (C : Type*) [Category C] {ι : Type*} (c : ComplexShape ι) [HasZeroMorphisms C]
-  [CategoryWithHomology C] [(HomologicalComplex.qis C c).HasLocalization]
+  [CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization]
 
 /-- The category of homological complexes up to quasi-isomorphisms. -/
-abbrev HomologicalComplexUpToQis := (HomologicalComplex.qis C c).Localization'
+abbrev HomologicalComplexUpToQuasiIso := (HomologicalComplex.quasiIso C c).Localization'
 
 variable {C c}
 
-/-- The localization functor `HomologicalComplex C c ⥤ HomologicalComplexUpToQis C c`. -/
-abbrev HomologicalComplexUpToQis.Q :
-    HomologicalComplex C c ⥤ HomologicalComplexUpToQis C c :=
-  (HomologicalComplex.qis C c).Q'
+/-- The localization functor `HomologicalComplex C c ⥤ HomologicalComplexUpToQuasiIso C c`. -/
+abbrev HomologicalComplexUpToQuasiIso.Q :
+    HomologicalComplex C c ⥤ HomologicalComplexUpToQuasiIso C c :=
+  (HomologicalComplex.quasiIso C c).Q'
 
 variable (C c)
 
-lemma HomologicalComplex.homologyFunctor_inverts_qis (i : ι) :
-    (qis C c).IsInvertedBy (homologyFunctor C c i) := fun _ _ _ hf => by
-      rw [qis_iff] at hf
+lemma HomologicalComplex.homologyFunctor_inverts_quasiIso (i : ι) :
+    (quasiIso C c).IsInvertedBy (homologyFunctor C c i) := fun _ _ _ hf => by
+      rw [mem_quasiIso_iff] at hf
       dsimp
       infer_instance
 
-namespace HomologicalComplexUpToQis
+namespace HomologicalComplexUpToQuasiIso
 
-/-- The homology functor `HomologicalComplexUpToQis C c ⥤ C` for each `i : ι`. -/
-noncomputable def homologyFunctor (i : ι) : HomologicalComplexUpToQis C c ⥤ C :=
-  Localization.lift _ (HomologicalComplex.homologyFunctor_inverts_qis C c i) Q
+/-- The homology functor `HomologicalComplexUpToQuasiIso C c ⥤ C` for each `i : ι`. -/
+noncomputable def homologyFunctor (i : ι) : HomologicalComplexUpToQuasiIso C c ⥤ C :=
+  Localization.lift _ (HomologicalComplex.homologyFunctor_inverts_quasiIso C c i) Q
 
-/-- The homology functor on `HomologicalComplexUpToQis C c` is induced by
+/-- The homology functor on `HomologicalComplexUpToQuasiIso C c` is induced by
 the homology functor on `HomologicalComplex C c`. -/
 noncomputable def homologyFunctorFactors (i : ι) :
     Q ⋙ homologyFunctor C c i ≅ HomologicalComplex.homologyFunctor C c i :=
-  Localization.fac _ (HomologicalComplex.homologyFunctor_inverts_qis C c i) Q
+  Localization.fac _ (HomologicalComplex.homologyFunctor_inverts_quasiIso C c i) Q
+
+variable {C c}
+
+lemma isIso_Q_map_iff_mem_quasiIso {K L : HomologicalComplex C c} (f : K ⟶ L) :
+    IsIso (Q.map f) ↔ HomologicalComplex.quasiIso C c f := by
+  constructor
+  · intro h
+    rw [HomologicalComplex.mem_quasiIso_iff, quasiIso_iff]
+    intro i
+    rw [quasiIsoAt_iff_isIso_homologyMap]
+    refine' (NatIso.isIso_map_iff (homologyFunctorFactors C c i) f).1 _
+    dsimp
+    infer_instance
+  · intro h
+    exact Localization.inverts Q (HomologicalComplex.quasiIso C c) _ h
+
+end HomologicalComplexUpToQuasiIso
+
+end
+
+section
+
+variable (C : Type*) [Category C] {ι : Type*} (c : ComplexShape ι) [Preadditive C]
+  [CategoryWithHomology C] [(HomologicalComplex.quasiIso C c).HasLocalization]
+
+lemma HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences :
+    (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy
+      HomologicalComplexUpToQuasiIso.Q :=
+  MorphismProperty.IsInvertedBy.of_subset _ _ _
+    (Localization.inverts Q (HomologicalComplex.quasiIso C c))
+    (homotopyEquivalences_subset_quasiIso C c)
+
+namespace HomotopyCategory
+
+/-- The class of quasi-isomorphisms in the homotopy category. -/
+def quasiIso : MorphismProperty (HomotopyCategory C c) :=
+  fun _ _ f => ∀ (i : ι), IsIso ((homologyFunctor C c i).map f)
+
+variable {C c}
+
+lemma mem_quasiIso_iff {X Y : HomotopyCategory C c} (f : X ⟶ Y) :
+    quasiIso C c f ↔ ∀ (n : ι), IsIso ((homologyFunctor _ _ n).map f) := by
+  rfl
+
+lemma quotient_map_mem_quasiIso_iff {K L : HomologicalComplex C c} (f : K ⟶ L) :
+    quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f := by
+  have eq := fun (i : ι) => NatIso.isIso_map_iff (homologyFunctorFactors C c i) f
+  dsimp at eq
+  simp only [HomologicalComplex.mem_quasiIso_iff, mem_quasiIso_iff, quasiIso_iff,
+    quasiIsoAt_iff_isIso_homologyMap, eq]
+
+variable (C c)
 
-end HomologicalComplexUpToQis
+lemma respectsIso_quasiIso : (quasiIso C c).RespectsIso := by
+  apply MorphismProperty.RespectsIso.of_respects_arrow_iso
+  intro f g e hf i
+  exact ((MorphismProperty.RespectsIso.isomorphisms C).arrow_mk_iso_iff
+    ((homologyFunctor C c i).mapArrow.mapIso e)).1 (hf i)
+
+lemma homologyFunctor_inverts_quasiIso (i : ι) :
+    (quasiIso C c).IsInvertedBy (homologyFunctor C c i) := fun _ _ _ hf => hf i
+
+lemma quasiIso_eq_quasiIso_map_quotient :
+    quasiIso C c = (HomologicalComplex.quasiIso C c).map (quotient C c) := by
+  ext ⟨K⟩ ⟨L⟩ f
+  obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective f
+  constructor
+  · intro hf
+    rw [quotient_map_mem_quasiIso_iff] at hf
+    exact MorphismProperty.map_mem_map _ _ _ hf
+  · rintro ⟨K', L', g, h, ⟨e⟩⟩
+    rw [← quotient_map_mem_quasiIso_iff] at h
+    exact ((respectsIso_quasiIso C c).arrow_mk_iso_iff e).1 h
+
+end HomotopyCategory
+
+/-- The condition on a complex shape `c` saying that homotopic maps become equal in
+the localized category with respect to quasi-isomorphisms. -/
+class ComplexShape.QFactorsThroughHomotopy {ι : Type*} (c : ComplexShape ι)
+    (C : Type*) [Category C] [Preadditive C]
+    [CategoryWithHomology C] : Prop where
+  areEqualizedByLocalization {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g) :
+    AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g
+
+end

Mathlib/Algebra/Homology/QuasiIso.lean

@@ -468,13 +468,13 @@ end PreservesHomology
 variable (C c)
 
 /-- The morphism property on `HomologicalComplex C c` given by quasi-isomorphisms. -/
-def qis [CategoryWithHomology C] :
+def quasiIso [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
+lemma mem_quasiIso_iff [CategoryWithHomology C] (f : K ⟶ L) : quasiIso C c f ↔ QuasiIso f := by rfl
 
 end HomologicalComplex
 
@@ -497,8 +497,10 @@ instance : QuasiIso e.hom where
 
 instance : QuasiIso e.inv := (inferInstance : QuasiIso e.symm.hom)
 
-lemma homotopyEquivalences_subset_qis [CategoryWithHomology C] :
-    homotopyEquivalences C c ⊆ qis C c := by
+variable (C c)
+
+lemma homotopyEquivalences_subset_quasiIso [CategoryWithHomology C] :
+    homotopyEquivalences C c ⊆ quasiIso C c := by
   rintro K L _ ⟨e, rfl⟩
-  simp only [qis_iff]
+  simp only [HomologicalComplex.mem_quasiIso_iff]
   infer_instance

Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

@@ -291,7 +291,7 @@ lemma comp₀_rel {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction
   dsimp at fac
   have eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s := by
     rw [← reassoc_of% h₃, ← reassoc_of% h₃', fac]
-  obtain ⟨Y, t, ht, fac'⟩ := ext _ _ _ z₁.hs eq
+  obtain ⟨Y, t, ht, fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ z₁.hs eq
   simp only [assoc] at fac'
   refine' ⟨Y, z₄.f ≫ t, z₄.s ≫ t, _, _, _⟩
   · simp only [comp₀, assoc, reassoc_of% fac]
@@ -346,7 +346,7 @@ noncomputable def Hom.comp {X Y Z : C} (z₁ : Hom W X Y) (z₂ : Hom W Y Z) : H
     have eq : a.s ≫ z₁.f ≫ w₁.f ≫ u.f = a.s ≫ z₂.f ≫ w₂.f ≫ u.s := by
       rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
         reassoc_of% hft, fac₃]
-    obtain ⟨Z, p, hp, fac₄⟩ := ext _ _ _ a.hs eq
+    obtain ⟨Z, p, hp, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a.hs eq
     simp only [assoc] at fac₄
     rw [comp_eq _ _ z₁ fac₁, comp_eq _ _ z₂ fac₂]
     apply Quot.sound
@@ -376,7 +376,7 @@ noncomputable def Hom.comp {X Y Z : C} (z₁ : Hom W X Y) (z₂ : Hom W Y Z) : H
     apply Quot.sound
     refine' LeftFractionRel.trans _ ((_ : LeftFractionRel p₁ p₂).trans _)
     · have eq : a₁.s ≫ z₁.f ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f := by rw [← fac₁', reassoc_of% fac₁]
-      obtain ⟨Z, u, hu, fac₃⟩ := ext _ _ _ a₁.hs eq
+      obtain ⟨Z, u, hu, fac₃⟩ := HasLeftCalculusOfFractions.ext _ _ _ a₁.hs eq
       simp only [assoc] at fac₃
       refine' ⟨Z, w₁.s ≫ u, u, _, _, _⟩
       · dsimp
@@ -392,7 +392,7 @@ noncomputable def Hom.comp {X Y Z : C} (z₁ : Hom W X Y) (z₂ : Hom W Y Z) : H
       simp only [assoc] at fac₃
       have eq : a₁.s ≫ t₁ ≫ w₁.f ≫ q.f = a₁.s ≫ t₁ ≫ w₂.f ≫ q.s := by
         rw [← reassoc_of% fac₁', ← fac₃, reassoc_of% hst, reassoc_of% fac₂']
-      obtain ⟨Z, u, hu, fac₄⟩ := ext _ _ _ a₁.hs eq
+      obtain ⟨Z, u, hu, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a₁.hs eq
       simp only [assoc] at fac₄
       refine' ⟨Z, q.f ≫ u, q.s ≫ u, _, _, _⟩
       · simp only [assoc, reassoc_of% fac₃]
@@ -402,7 +402,7 @@ noncomputable def Hom.comp {X Y Z : C} (z₁ : Hom W X Y) (z₂ : Hom W Y Z) : H
           (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ q.hs hu)))
     · have eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f := by
         rw [← fac₂', reassoc_of% fac₂]
-      obtain ⟨Z, u, hu, fac₄⟩ := ext _ _ _ a₂.hs eq
+      obtain ⟨Z, u, hu, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a₂.hs eq
       simp only [assoc] at fac₄
       refine' ⟨Z, u, w₂.s ≫ u, _, _, _⟩
       · dsimp

Mathlib/CategoryTheory/Localization/Predicate.lean

@@ -483,4 +483,41 @@ def isoUniqFunctor (F : D₁ ⥤ D₂) (e : L₁ ⋙ F ≅ L₂) :
 
 end Localization
 
+section
+
+variable {X Y : C} (f g : X ⟶ Y)
+
+/-- The property that two morphisms become equal in the localized category. -/
+def AreEqualizedByLocalization : Prop := W.Q.map f = W.Q.map g
+
+lemma areEqualizedByLocalization_iff [L.IsLocalization W]:
+    AreEqualizedByLocalization W f g ↔ L.map f = L.map g := by
+  dsimp [AreEqualizedByLocalization]
+  constructor
+  · intro h
+    let e := Localization.compUniqFunctor W.Q L W
+    rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]
+    dsimp
+    rw [h]
+  · intro h
+    let e := Localization.compUniqFunctor L W.Q W
+    rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]
+    dsimp
+    rw [h]
+
+namespace AreEqualizedByLocalization
+
+lemma mk (L : C ⥤ D) [L.IsLocalization W] (h : L.map f = L.map g) :
+    AreEqualizedByLocalization W f g :=
+  (areEqualizedByLocalization_iff L W f g).2 h
+
+variable {W f g} (h : AreEqualizedByLocalization W f g)
+
+lemma map_eq (L : C ⥤ D) [L.IsLocalization W] : L.map f = L.map g :=
+  (areEqualizedByLocalization_iff L W f g).1 h
+
+end AreEqualizedByLocalization
+
+end
+
 end CategoryTheory

Mathlib/CategoryTheory/MorphismProperty.lean

@@ -55,6 +55,12 @@ variable {C}
 
 namespace MorphismProperty
 
+@[ext]
+lemma ext (W W' : MorphismProperty C) (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f) :
+    W = W' := by
+  funext X Y f
+  rw [h]
+
 lemma top_apply {X Y : C} (f : X ⟶ Y) : (⊤ : MorphismProperty C) f := by
   simp only [top_eq]
 

Mathlib/CategoryTheory/Preadditive/InjectiveResolution.lean

@@ -55,7 +55,7 @@ set_option linter.uppercaseLean3 false in
 #align category_theory.InjectiveResolution CategoryTheory.InjectiveResolution
 
 open InjectiveResolution in
-attribute [instance] injective quasiIso hasHomology
+attribute [instance] injective hasHomology InjectiveResolution.quasiIso
 
 /-- An object admits an injective resolution. -/
 class HasInjectiveResolution (Z : C) : Prop where

Mathlib/CategoryTheory/Preadditive/ProjectiveResolution.lean

@@ -50,7 +50,7 @@ set_option linter.uppercaseLean3 false in
 #align category_theory.ProjectiveResolution CategoryTheory.ProjectiveResolution
 
 open ProjectiveResolution in
-attribute [instance] projective quasiIso hasHomology
+attribute [instance] projective hasHomology ProjectiveResolution.quasiIso
 
 /-- An object admits a projective resolution.
 -/

Mathlib/CategoryTheory/Quotient.lean

@@ -199,6 +199,15 @@ theorem lift_unique (Φ : Quotient r ⥤ D) (hΦ : functor r ⋙ Φ = F) : Φ =
     congr
 #align category_theory.quotient.lift_unique CategoryTheory.Quotient.lift_unique
 
+lemma lift_unique' (F₁ F₂ : Quotient r ⥤ D) (h : functor r ⋙ F₁ = functor r ⋙ F₂) :
+    F₁ = F₂ := by
+  rw [lift_unique r (functor r ⋙ F₂) _ F₂ rfl]; swap
+  · rintro X Y f g h
+    dsimp
+    rw [Quotient.sound r h]
+  apply lift_unique
+  rw [h]
+
 /-- The original functor factors through the induced functor. -/
 def lift.isLift : functor r ⋙ lift r F H ≅ F :=
   NatIso.ofComponents fun X ↦ Iso.refl _