feat(Algebra/Homology): quasi-isomorphisms are stable under retracts and have the 2/3 property

Mathlib.lean

@@ -466,6 +466,7 @@ import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
 import Mathlib.Algebra.Homology.ShortComplex.Preadditive
 import Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
 import Mathlib.Algebra.Homology.ShortComplex.QuasiIso
+import Mathlib.Algebra.Homology.ShortComplex.Retract
 import Mathlib.Algebra.Homology.ShortComplex.RightHomology
 import Mathlib.Algebra.Homology.ShortComplex.ShortExact
 import Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Mathlib/Algebra/Homology/QuasiIso.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Joël Riou
 -/
 import Mathlib.Algebra.Homology.Homotopy
+import Mathlib.Algebra.Homology.ShortComplex.Retract
+import Mathlib.CategoryTheory.MorphismProperty.Composition
 
 /-!
 # Quasi-isomorphisms
@@ -51,6 +53,15 @@ lemma quasiIsoAt_iff' (f : K ⟶ L) (i j k : ι) (hi : c.prev j = i) (hk : c.nex
   exact ShortComplex.quasiIso_iff_of_arrow_mk_iso _ _
     (Arrow.isoOfNatIso (natIsoSc' C c i j k hi hk) (Arrow.mk f))
 
+lemma quasiIsoAt_of_retract {f : K ⟶ L} {f' : K' ⟶ L'}
+    (h : RetractArrow f f') (i : ι) [K.HasHomology i] [L.HasHomology i]
+    [K'.HasHomology i] [L'.HasHomology i] [hf' : QuasiIsoAt f' i] :
+    QuasiIsoAt f i := by
+  rw [quasiIsoAt_iff] at hf' ⊢
+  have : RetractArrow ((shortComplexFunctor C c i).map f)
+    ((shortComplexFunctor C c i).map f') := h.map (shortComplexFunctor C c i).mapArrow
+  exact ShortComplex.quasiIso_of_retract this
+
 lemma quasiIsoAt_iff_isIso_homologyMap (f : K ⟶ L) (i : ι)
     [K.HasHomology i] [L.HasHomology i] :
     QuasiIsoAt f i ↔ IsIso (homologyMap f i) := by
@@ -219,6 +230,12 @@ lemma quasiIso_of_arrow_mk_iso (φ : K ⟶ L) (φ' : K' ⟶ L') (e : Arrow.mk φ
     [hφ : QuasiIso φ] : QuasiIso φ' := by
   simpa only [← quasiIso_iff_of_arrow_mk_iso φ φ' e]
 
+lemma quasiIso_of_retractArrow {f : K ⟶ L} {f' : K' ⟶ L'}
+    (h : RetractArrow f f') [∀ i, K.HasHomology i] [∀ i, L.HasHomology i]
+    [∀ i, K'.HasHomology i] [∀ i, L'.HasHomology i] [QuasiIso f'] :
+    QuasiIso f where
+  quasiIsoAt i := quasiIsoAt_of_retract h i
+
 namespace HomologicalComplex
 
 section PreservesHomology
@@ -270,10 +287,35 @@ variable (C c)
 def quasiIso [CategoryWithHomology C] :
     MorphismProperty (HomologicalComplex C c) := fun _ _ f => QuasiIso f
 
-variable {C c}
+variable {C c} [CategoryWithHomology C]
 
 @[simp]
-lemma mem_quasiIso_iff [CategoryWithHomology C] (f : K ⟶ L) : quasiIso C c f ↔ QuasiIso f := by rfl
+lemma mem_quasiIso_iff  (f : K ⟶ L) : quasiIso C c f ↔ QuasiIso f := by rfl
+
+instance : (quasiIso C c).IsMultiplicative where
+  id_mem _ := by
+    rw [mem_quasiIso_iff]
+    infer_instance
+  comp_mem _ _ hf hg := by
+    rw [mem_quasiIso_iff] at hf hg ⊢
+    infer_instance
+
+instance : (quasiIso C c).HasTwoOutOfThreeProperty where
+  of_postcomp f g hg hfg := by
+    rw [mem_quasiIso_iff] at hg hfg ⊢
+    rwa [← quasiIso_iff_comp_right f g]
+  of_precomp f g hf hfg := by
+    rw [mem_quasiIso_iff] at hf hfg ⊢
+    rwa [← quasiIso_iff_comp_left f g]
+
+instance : (quasiIso C c).IsStableUnderRetracts where
+  of_retract h hg := by
+    rw [mem_quasiIso_iff] at hg ⊢
+    exact quasiIso_of_retractArrow h
+
+instance : (quasiIso C c).RespectsIso :=
+  MorphismProperty.respectsIso_of_isStableUnderComposition
+    (fun _ _ _ (_ : IsIso _) ↦ by rw [mem_quasiIso_iff]; infer_instance)
 
 end HomologicalComplex
 

Mathlib/Algebra/Homology/ShortComplex/Retract.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2024 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.ShortComplex.QuasiIso
+import Mathlib.CategoryTheory.MorphismProperty.Retract
+
+/-!
+# Quasi-isomorphisms of short complexes are stable under retracts
+
+-/
+
+namespace CategoryTheory
+
+open Limits
+
+namespace ShortComplex
+
+variable {C : Type*} [Category C] [HasZeroMorphisms C]
+  {S₁ T₁ S₂ T₂ : ShortComplex C}
+  [S₁.HasHomology] [T₁.HasHomology] [S₂.HasHomology] [T₂.HasHomology]
+  {f₁ : S₁ ⟶ T₁} {f₂ : S₂ ⟶ T₂}
+
+lemma quasiIso_of_retract (h : RetractArrow f₁ f₂) [hf₂ : QuasiIso f₂] :
+    QuasiIso f₁ := by
+  rw [quasiIso_iff] at hf₂ ⊢
+  have h : RetractArrow (homologyMap f₁) (homologyMap f₂) :=
+    { i := Arrow.homMk (u := homologyMap (show S₁ ⟶ S₂ from h.i.left))
+        (v := homologyMap (show T₁ ⟶ T₂ from h.i.right)) (by simp [← homologyMap_comp])
+      r := Arrow.homMk (u := homologyMap (show S₂ ⟶ S₁ from h.r.left))
+        (v := homologyMap (show T₂ ⟶ T₁ from h.r.right)) (by simp [← homologyMap_comp])
+      retract := by ext <;> simp [← homologyMap_comp] }
+  exact (MorphismProperty.isomorphisms C).of_retract h hf₂
+
+end ShortComplex
+
+end CategoryTheory