From c368c67d0d6dee42fbec7ae9c847f46ee1eb1cbe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 22 Jun 2026 11:08:34 +0200
Subject: [PATCH 1/9] feat(Algebra/Homology/Embedding): various results about
 truncations

---
 .../Homology/Embedding/CochainComplex.lean    | 57 +++++++++++++++++++
 .../Homology/Embedding/TruncGEHomology.lean   |  5 ++
 .../Homology/Embedding/TruncLEHomology.lean   |  5 ++
 3 files changed, 67 insertions(+)

diff --git a/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean b/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
index cd3908b34d4fc7..800a7708629da9 100644
--- a/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
+++ b/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
@@ -361,6 +361,63 @@ end
 
 end Preadditive
 
+section HasZeroMorphisms
+
+variable {C : Type*} [Category C] [HasZeroMorphisms C] [HasZeroObject C]
+  (K L : CochainComplex C ℤ) (φ : K ⟶ L) (e : K ≅ L)
+  [∀ (i : ℤ), K.HasHomology i] [∀ (i : ℤ), L.HasHomology i] (n : ℤ)
+
+set_option backward.defeqAttrib.useBackward true in
+/-- When `K` is a cochain complex indexed by `ℤ` and `n < i`, this is
+the isomorphism `(K.truncGE n).X i ≅ K.X i`. -/
+noncomputable def truncGEXIso (n i : ℤ) (hi : n < i := by lia) :
+    (K.truncGE n).X i ≅ K.X i :=
+  HomologicalComplex.truncGEXIso K (embeddingUpIntGE n) (i := (i - n).natAbs) (by
+      dsimp
+      rw [Int.natAbs_of_nonneg (by lia), add_sub_cancel])
+    (fun h ↦ by
+      rw [boundaryGE_embeddingUpIntGE_iff, Int.natAbs_eq_zero] at h
+      lia)
+
+set_option backward.defeqAttrib.useBackward true in
+/-- When `K` is a cochain complex indexed by `ℤ` and `i < n`, this is
+the isomorphism `(K.truncLE n).X i ≅ K.X i`. -/
+noncomputable def truncLEXIso (n i : ℤ) (hi : i < n := by lia) :
+    (K.truncLE n).X i ≅ K.X i :=
+  HomologicalComplex.truncLEXIso K (embeddingUpIntLE n) (i := (n - i).natAbs) (by
+      dsimp
+      rw [Int.natAbs_of_nonneg (by lia), sub_sub_cancel])
+    (fun h ↦ by
+      rw [boundaryLE_embeddingUpIntLE_iff, Int.natAbs_eq_zero] at h
+      lia)
+
+/-- When `K` is a cochain complex indexed by `ℤ`, this is the isomorphism
+`(K.truncGE n).X n ≅ K.opcycles n`. -/
+noncomputable def truncGEXIsoOpcycles (n : ℤ) :
+    (K.truncGE n).X n ≅ K.opcycles n :=
+  HomologicalComplex.truncGEXIsoOpcycles K (embeddingUpIntGE n) (i := 0) (by simp)
+    (by rw [boundaryGE_embeddingUpIntGE_iff])
+
+/-- When `K` is a cochain complex indexed by `ℤ`, this is the isomorphism
+`(K.truncLE n).X n ≅ K.cycles n`. -/
+noncomputable def truncLEXIsoCycles (n : ℤ) :
+    (K.truncLE n).X n ≅ K.cycles n :=
+  HomologicalComplex.truncLEXIsoCycles K (embeddingUpIntLE n) (i := 0) (by simp)
+    (by rw [boundaryLE_embeddingUpIntLE_iff])
+
+lemma acyclic_truncGE_iff (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁ := by lia) :
+    (K.truncGE n₁).Acyclic ↔ K.IsLE n₀ := by
+  dsimp [truncGE]
+  rw [acyclic_truncGE_iff_isSupportedOutside,
+    (Embedding.embeddingUpInt_areComplementary n₀ n₁ h).isSupportedOutside₂_iff]
+
+lemma acyclic_truncLE_iff (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁ := by lia) :
+    (K.truncLE n₀).Acyclic ↔ K.IsGE n₁ := by
+  dsimp [truncLE]
+  rw [acyclic_truncLE_iff_isSupportedOutside,
+    (Embedding.embeddingUpInt_areComplementary n₀ n₁ h).isSupportedOutside₁_iff]
+
+end HasZeroMorphisms
 
 section Abelian
 
diff --git a/Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean b/Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
index 4a3dfcb22871f7..bc11bec38b692a 100644
--- a/Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
+++ b/Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
@@ -226,6 +226,11 @@ lemma acyclic_truncGE_iff_isSupportedOutside :
 
 variable {K L}
 
+lemma Acyclic.truncGE (hK : K.Acyclic) (e : c.Embedding c') [e.IsTruncGE] :
+    (K.truncGE e).Acyclic := by
+  rw [acyclic_truncGE_iff_isSupportedOutside]
+  exact ⟨fun _ ↦ hK _⟩
+
 lemma quasiIso_truncGEMap_iff :
     QuasiIso (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι') (_ : e.f i = i'), QuasiIsoAt φ i' := by
   have : ∀ (i : ι) (i' : ι') (_ : e.f i = i'),
diff --git a/Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean b/Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean
index 4dce5e6f3311e7..d502131ca9842d 100644
--- a/Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean
+++ b/Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean
@@ -84,6 +84,11 @@ lemma acyclic_truncLE_iff_isSupportedOutside :
 
 variable {K L}
 
+lemma Acyclic.truncLE (hK : K.Acyclic) (e : c.Embedding c') [e.IsTruncLE] :
+    (K.truncLE e).Acyclic := by
+  rw [acyclic_truncLE_iff_isSupportedOutside]
+  exact ⟨fun _ ↦ hK _⟩
+
 lemma quasiIso_truncLEMap_iff :
     QuasiIso (truncLEMap φ e) ↔ ∀ (i : ι) (i' : ι') (_ : e.f i = i'), QuasiIsoAt φ i' := by
   rw [← quasiIso_opFunctor_map_iff]

From fdb8c9f7a4bc50f299ae1cf901219c058bf7d11f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 22 Jun 2026 11:34:16 +0200
Subject: [PATCH 2/9] feat(Algebra/Homology): injective resolution of a cochain
 complex

---
 .../Algebra/Homology/Factorizations/CM5a.lean | 50 ++++++++++++++++++-
 1 file changed, 48 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
index 30242a2ebf1749..bd9d835299c495 100644
--- a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
+++ b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
@@ -5,10 +5,9 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
+public import Mathlib.Algebra.Homology.DerivedCategory.TStructure
 public import Mathlib.Algebra.Homology.Factorizations.CM5b
 public import Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant
-public import Mathlib.Algebra.Homology.Refinements
 public import Mathlib.Algebra.Homology.SingleHomology
 public import Mathlib.CategoryTheory.Category.Factorisation
 public import Mathlib.CategoryTheory.Functor.OfSequence
@@ -652,4 +651,51 @@ public lemma cm5a (n : ℤ) [K.IsStrictlyGE (n + 1)] [L.IsStrictlyGE n] :
   exact ⟨K', inferInstance, ι, π ≫ p, inferInstance, inferInstance,
     MorphismProperty.comp_mem _ _ _ hπ hp, by simp⟩
 
+open ZeroObject
+
+variable (K)
+
+public lemma exists_injective_resolution' (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁ := by lia)
+    [K.IsStrictlyGE n₁] :
+    ∃ (L : CochainComplex C ℤ) (i : K ⟶ L) (_hi : Mono i) (_hi' : QuasiIso i)
+      (_ : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n₀ := by
+  have : K.IsStrictlyGE (n₀ + 1) := by rw [h]; infer_instance
+  obtain ⟨L, hL, i, p, hi, hi', hp, _⟩ := cm5a (0 : K ⟶ 0) n₀
+  exact ⟨L, i, hi, hi', (degreewiseEpiWithInjectiveKernel_iff_of_isZero p
+    (Limits.isZero_zero _)).1 hp, hL⟩
+
+public lemma exists_injective_resolution (n : ℤ) [K.IsStrictlyGE n] :
+    ∃ (L : CochainComplex C ℤ) (i : K ⟶ L) (_hi' : QuasiIso i)
+      (_hL : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n := by
+  have : HasDerivedCategory C := MorphismProperty.HasLocalization.standard _
+  obtain ⟨L, i, _, _, hL, _⟩ := exists_injective_resolution' K (n - 1) n (by simp)
+  have : L.IsGE n := by
+    have hK : K.IsGE n := inferInstance
+    rw [← DerivedCategory.isGE_Q_obj_iff] at hK ⊢
+    exact DerivedCategory.TStructure.t.isGE_of_iso (asIso (DerivedCategory.Q.map i)) n
+  have : QuasiIso (L.πTruncGE n) := by
+    rw [L.quasiIso_πTruncGE_iff n]
+    infer_instance
+  have : Injective (L.opcycles n) := by
+    let S : ShortComplex C := ShortComplex.mk (L.d (n - 1) n) (L.pOpcycles n) (by simp)
+    have : Mono S.f := by
+      let T := L.sc' (n - 2) (n - 1) n
+      have hT : T.Exact := by
+        rw [← L.exactAt_iff' (n - 2) (n - 1) n (by simp; lia) (by simp),
+          exactAt_iff_isZero_homology]
+        exact L.isZero_of_isGE n (n-1) (by linarith)
+      exact hT.mono_g ((L.isZero_of_isStrictlyGE (n - 1) _).eq_of_src ..)
+    have hS : S.ShortExact :=
+      { exact := S.exact_of_g_is_cokernel (L.opcyclesIsCokernel (n-1) n (by simp)) }
+    exact Retract.injective
+      { i := _, r := _, retract := (hS.splittingOfInjective).s_g }
+  -- note: this `i ≫ L.πTruncGE n` is a mono in degrees > n, but it may not be in degree n
+  refine ⟨L.truncGE n, i ≫ L.πTruncGE n, inferInstance, fun q ↦ ?_, inferInstance⟩
+  by_cases h : q < n
+  · exact (isZero_of_isStrictlyGE _ n _ h).injective
+  · simp only [not_lt] at h
+    obtain (hq | rfl) := h.lt_or_eq
+    · exact Injective.of_iso (L.truncGEXIso n q hq).symm (hL q)
+    · exact Injective.of_iso (L.truncGEXIsoOpcycles n).symm inferInstance
+
 end CochainComplex.Plus.modelCategoryQuillen

From b1db8b0e65d84972f831019b13622425adb74c36 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?=
 <37772949+joelriou@users.noreply.github.com>
Date: Mon, 22 Jun 2026 16:18:20 +0200
Subject: [PATCH 3/9] Update Mathlib/Algebra/Homology/Factorizations/CM5a.lean

Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>
---
 Mathlib/Algebra/Homology/Factorizations/CM5a.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
index bd9d835299c495..1e39c29d562b92 100644
--- a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
+++ b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
@@ -691,11 +691,9 @@ public lemma exists_injective_resolution (n : ℤ) [K.IsStrictlyGE n] :
       { i := _, r := _, retract := (hS.splittingOfInjective).s_g }
   -- note: this `i ≫ L.πTruncGE n` is a mono in degrees > n, but it may not be in degree n
   refine ⟨L.truncGE n, i ≫ L.πTruncGE n, inferInstance, fun q ↦ ?_, inferInstance⟩
-  by_cases h : q < n
+  rcases (lt_trichotomy q n) with h | rfl | h
   · exact (isZero_of_isStrictlyGE _ n _ h).injective
-  · simp only [not_lt] at h
-    obtain (hq | rfl) := h.lt_or_eq
-    · exact Injective.of_iso (L.truncGEXIso n q hq).symm (hL q)
-    · exact Injective.of_iso (L.truncGEXIsoOpcycles n).symm inferInstance
+  · exact Injective.of_iso (L.truncGEXIsoOpcycles q).symm inferInstance
+  · exact Injective.of_iso (L.truncGEXIso n q h).symm (hL q)
 
 end CochainComplex.Plus.modelCategoryQuillen

From 735a6332c9699c6964d21c2c1de31f5d168568cf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 22 Jun 2026 16:30:12 +0200
Subject: [PATCH 4/9] added docstring

---
 Mathlib/Algebra/Homology/Factorizations/CM5a.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
index 1e39c29d562b92..69022e9e045de7 100644
--- a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
+++ b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
@@ -667,6 +667,13 @@ public lemma exists_injective_resolution' (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁
 public lemma exists_injective_resolution (n : ℤ) [K.IsStrictlyGE n] :
     ∃ (L : CochainComplex C ℤ) (i : K ⟶ L) (_hi' : QuasiIso i)
       (_hL : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n := by
+  /- The proof proceeds by first applying `exists_injective_resolution'` in order to
+  obtain a monomorphism `K ⟶ L` that is also a quasi-isomorphism
+  with `L` consisting of injective objects and `L` lying in degrees `≥ n - 1`.
+  Then, as it is quasi-isomorphic to `K`, the cochain complex `L` is cohomologically
+  in degrees `≥ n`, so that the composition `K ⟶ L ⟶ L.truncGE n` is a quasi-isomorphism.
+  In order to conclude, one needs to show that `(L.truncGE n).X n` is injective,
+  i.e. that `L.opcycles n` is injective. -/
   have : HasDerivedCategory C := MorphismProperty.HasLocalization.standard _
   obtain ⟨L, i, _, _, hL, _⟩ := exists_injective_resolution' K (n - 1) n (by simp)
   have : L.IsGE n := by
@@ -691,7 +698,7 @@ public lemma exists_injective_resolution (n : ℤ) [K.IsStrictlyGE n] :
       { i := _, r := _, retract := (hS.splittingOfInjective).s_g }
   -- note: this `i ≫ L.πTruncGE n` is a mono in degrees > n, but it may not be in degree n
   refine ⟨L.truncGE n, i ≫ L.πTruncGE n, inferInstance, fun q ↦ ?_, inferInstance⟩
-  rcases (lt_trichotomy q n) with h | rfl | h
+  obtain h | rfl | h := lt_trichotomy q n
   · exact (isZero_of_isStrictlyGE _ n _ h).injective
   · exact Injective.of_iso (L.truncGEXIsoOpcycles q).symm inferInstance
   · exact Injective.of_iso (L.truncGEXIso n q h).symm (hL q)

From f843dcd493d5ad763ae1f7aeb1862546b47a2caf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?=
 <37772949+joelriou@users.noreply.github.com>
Date: Mon, 22 Jun 2026 16:30:40 +0200
Subject: [PATCH 5/9] Update Mathlib/Algebra/Homology/Factorizations/CM5a.lean

Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>
---
 Mathlib/Algebra/Homology/Factorizations/CM5a.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
index 69022e9e045de7..15d957dfcca73e 100644
--- a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
+++ b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
@@ -680,9 +680,7 @@ public lemma exists_injective_resolution (n : ℤ) [K.IsStrictlyGE n] :
     have hK : K.IsGE n := inferInstance
     rw [← DerivedCategory.isGE_Q_obj_iff] at hK ⊢
     exact DerivedCategory.TStructure.t.isGE_of_iso (asIso (DerivedCategory.Q.map i)) n
-  have : QuasiIso (L.πTruncGE n) := by
-    rw [L.quasiIso_πTruncGE_iff n]
-    infer_instance
+  have : QuasiIso (L.πTruncGE n) := (L.quasiIso_πTruncGE_iff n).mpr inferInstance
   have : Injective (L.opcycles n) := by
     let S : ShortComplex C := ShortComplex.mk (L.d (n - 1) n) (L.pOpcycles n) (by simp)
     have : Mono S.f := by

From f4738f0709cb6efb60ebaf9fc7c0e0872089d148 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Tue, 23 Jun 2026 10:28:44 +0200
Subject: [PATCH 6/9] added separate lemma

---
 .../Homology/DerivedCategory/TStructure.lean  |  2 +-
 .../Homology/Embedding/CochainComplex.lean    | 22 ++++++++++++++++---
 .../Algebra/Homology/Factorizations/CM5a.lean | 16 +++-----------
 3 files changed, 23 insertions(+), 17 deletions(-)

diff --git a/Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean b/Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean
index ae92cb4c519546..085d7772a0baca 100644
--- a/Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean
+++ b/Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean
@@ -76,7 +76,7 @@ noncomputable def TStructure.t : TStructure (DerivedCategory C) where
       rw [id_comp]
       rfl
     · dsimp
-      rw [← Q.map_comp, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE,
+      rw [← Q.map_comp, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE ..,
         Iso.hom_inv_id_assoc]
 
 /-- Given `X : DerivedCategory C` and `n : ℤ`, this property means
diff --git a/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean b/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
index 800a7708629da9..fd41039ee86f8b 100644
--- a/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
+++ b/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
@@ -431,19 +431,35 @@ lemma shortComplexTruncLE_shortExact (n : ℤ) :
     (K.shortComplexTruncLE n).ShortExact := by
   apply HomologicalComplex.shortComplexTruncLE_shortExact
 
-variable (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁)
+variable (n₀ n₁ : ℤ)
 
 /-- The canonical morphism `(K.shortComplexTruncLE n₀).X₃ ⟶ K.truncGE n₁`. -/
-noncomputable abbrev shortComplexTruncLEX₃ToTruncGE :
+noncomputable abbrev shortComplexTruncLEX₃ToTruncGE (h : n₀ + 1 = n₁ := by lia) :
     (K.shortComplexTruncLE n₀).X₃ ⟶ K.truncGE n₁ :=
   HomologicalComplex.shortComplexTruncLEX₃ToTruncGE K
     (Embedding.embeddingUpInt_areComplementary n₀ n₁ h)
 
 @[reassoc]
-lemma g_shortComplexTruncLEX₃ToTruncGE :
+lemma g_shortComplexTruncLEX₃ToTruncGE (h : n₀ + 1 = n₁ := by lia) :
     (K.shortComplexTruncLE n₀).g ≫ K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h = K.πTruncGE n₁ := by
   apply HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE
 
+lemma injective_opcycles [Injective (K.X n₀)] [Injective (K.X n₁)]
+    [K.IsStrictlyGE n₀] (hK : K.ExactAt n₀) (h : n₀ + 1 = n₁ := by lia) :
+    Injective (K.opcycles n₁) := by
+  let S : ShortComplex C := ShortComplex.mk (K.d n₀ n₁) (K.pOpcycles n₁) (by simp)
+  have : Mono S.f := by
+    let T := K.sc' (n₀ - 1) n₀ n₁
+    have hT : T.Exact := by
+      rw [← K.exactAt_iff' (n₀ - 1) n₀ n₁ (by simp) (by simpa),
+        exactAt_iff_isZero_homology]
+      exact hK.isZero_homology
+    exact hT.mono_g ((K.isZero_of_isStrictlyGE n₀ _).eq_of_src ..)
+  have hS : S.ShortExact :=
+    { exact := S.exact_of_g_is_cokernel (K.opcyclesIsCokernel n₀ n₁ (by simp [← h])) }
+  exact Retract.injective
+    { i := _, r := _, retract := (hS.splittingOfInjective).s_g }
+
 end Abelian
 
 end CochainComplex
diff --git a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
index 15d957dfcca73e..dd300497de5569 100644
--- a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
+++ b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
@@ -48,6 +48,7 @@ lemma `cm5a_cof`.
 
 -/
 
+
 open CategoryTheory Limits Opposite Abelian HomologicalComplex Pretriangulated
 
 variable {C : Type*} [Category* C] [Abelian C]
@@ -681,19 +682,8 @@ public lemma exists_injective_resolution (n : ℤ) [K.IsStrictlyGE n] :
     rw [← DerivedCategory.isGE_Q_obj_iff] at hK ⊢
     exact DerivedCategory.TStructure.t.isGE_of_iso (asIso (DerivedCategory.Q.map i)) n
   have : QuasiIso (L.πTruncGE n) := (L.quasiIso_πTruncGE_iff n).mpr inferInstance
-  have : Injective (L.opcycles n) := by
-    let S : ShortComplex C := ShortComplex.mk (L.d (n - 1) n) (L.pOpcycles n) (by simp)
-    have : Mono S.f := by
-      let T := L.sc' (n - 2) (n - 1) n
-      have hT : T.Exact := by
-        rw [← L.exactAt_iff' (n - 2) (n - 1) n (by simp; lia) (by simp),
-          exactAt_iff_isZero_homology]
-        exact L.isZero_of_isGE n (n-1) (by linarith)
-      exact hT.mono_g ((L.isZero_of_isStrictlyGE (n - 1) _).eq_of_src ..)
-    have hS : S.ShortExact :=
-      { exact := S.exact_of_g_is_cokernel (L.opcyclesIsCokernel (n-1) n (by simp)) }
-    exact Retract.injective
-      { i := _, r := _, retract := (hS.splittingOfInjective).s_g }
+  have : Injective (L.opcycles n) :=
+    L.injective_opcycles (n - 1) n (L.exactAt_of_isGE n (n - 1))
   -- note: this `i ≫ L.πTruncGE n` is a mono in degrees > n, but it may not be in degree n
   refine ⟨L.truncGE n, i ≫ L.πTruncGE n, inferInstance, fun q ↦ ?_, inferInstance⟩
   obtain h | rfl | h := lt_trichotomy q n

From df64ac04058a74a441c7dfa14a980d1c81828505 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Tue, 23 Jun 2026 10:33:57 +0200
Subject: [PATCH 7/9] better proof

---
 Mathlib/Algebra/Homology/Embedding/CochainComplex.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean b/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
index fd41039ee86f8b..ae06df80b4d34b 100644
--- a/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
+++ b/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
@@ -451,9 +451,7 @@ lemma injective_opcycles [Injective (K.X n₀)] [Injective (K.X n₁)]
   have : Mono S.f := by
     let T := K.sc' (n₀ - 1) n₀ n₁
     have hT : T.Exact := by
-      rw [← K.exactAt_iff' (n₀ - 1) n₀ n₁ (by simp) (by simpa),
-        exactAt_iff_isZero_homology]
-      exact hK.isZero_homology
+      rwa [← K.exactAt_iff' (n₀ - 1) n₀ n₁ (by simp) (by simpa)]
     exact hT.mono_g ((K.isZero_of_isStrictlyGE n₀ _).eq_of_src ..)
   have hS : S.ShortExact :=
     { exact := S.exact_of_g_is_cokernel (K.opcyclesIsCokernel n₀ n₁ (by simp [← h])) }

From 93ad52937596b52fcb091d2ba15425d9b4a1d4aa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Tue, 23 Jun 2026 10:58:39 +0200
Subject: [PATCH 8/9] better names

---
 Mathlib/Algebra/Homology/Factorizations/CM5a.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
index dd300497de5569..3cc419e1ca9cf3 100644
--- a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
+++ b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
@@ -656,7 +656,7 @@ open ZeroObject
 
 variable (K)
 
-public lemma exists_injective_resolution' (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁ := by lia)
+public lemma exists_mono_quasiIso_injective (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁ := by lia)
     [K.IsStrictlyGE n₁] :
     ∃ (L : CochainComplex C ℤ) (i : K ⟶ L) (_hi : Mono i) (_hi' : QuasiIso i)
       (_ : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n₀ := by
@@ -665,7 +665,7 @@ public lemma exists_injective_resolution' (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁
   exact ⟨L, i, hi, hi', (degreewiseEpiWithInjectiveKernel_iff_of_isZero p
     (Limits.isZero_zero _)).1 hp, hL⟩
 
-public lemma exists_injective_resolution (n : ℤ) [K.IsStrictlyGE n] :
+public lemma exists_quasiIso_injective (n : ℤ) [K.IsStrictlyGE n] :
     ∃ (L : CochainComplex C ℤ) (i : K ⟶ L) (_hi' : QuasiIso i)
       (_hL : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n := by
   /- The proof proceeds by first applying `exists_injective_resolution'` in order to
@@ -676,7 +676,7 @@ public lemma exists_injective_resolution (n : ℤ) [K.IsStrictlyGE n] :
   In order to conclude, one needs to show that `(L.truncGE n).X n` is injective,
   i.e. that `L.opcycles n` is injective. -/
   have : HasDerivedCategory C := MorphismProperty.HasLocalization.standard _
-  obtain ⟨L, i, _, _, hL, _⟩ := exists_injective_resolution' K (n - 1) n (by simp)
+  obtain ⟨L, i, _, _, hL, _⟩ := exists_mono_quasiIso_injective K (n - 1) n (by simp)
   have : L.IsGE n := by
     have hK : K.IsGE n := inferInstance
     rw [← DerivedCategory.isGE_Q_obj_iff] at hK ⊢

From a1ba43dedea97bb5411a087e70664ee09116339f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Tue, 23 Jun 2026 10:59:43 +0200
Subject: [PATCH 9/9] fix docstring

---
 Mathlib/Algebra/Homology/Factorizations/CM5a.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
index 3cc419e1ca9cf3..42fd1f3e186362 100644
--- a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
+++ b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
@@ -668,7 +668,7 @@ public lemma exists_mono_quasiIso_injective (n₀ n₁ : ℤ) (h : n₀ + 1 = n
 public lemma exists_quasiIso_injective (n : ℤ) [K.IsStrictlyGE n] :
     ∃ (L : CochainComplex C ℤ) (i : K ⟶ L) (_hi' : QuasiIso i)
       (_hL : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n := by
-  /- The proof proceeds by first applying `exists_injective_resolution'` in order to
+  /- The proof proceeds by first applying `exists_mono_quasiIso_injective` in order to
   obtain a monomorphism `K ⟶ L` that is also a quasi-isomorphism
   with `L` consisting of injective objects and `L` lying in degrees `≥ n - 1`.
   Then, as it is quasi-isomorphic to `K`, the cochain complex `L` is cohomologically