[Merged by Bors] - feat: the mapping cone of a monomorphism, up to a quasi-isomorphism

Mathlib.lean

@@ -312,6 +312,7 @@ import Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
 import Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
 import Mathlib.Algebra.Homology.HomotopyCategory.Shift
 import Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
+import Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
 import Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
 import Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
 import Mathlib.Algebra.Homology.HomotopyCofiber
@@ -322,6 +323,7 @@ import Mathlib.Algebra.Homology.Localization
 import Mathlib.Algebra.Homology.ModuleCat
 import Mathlib.Algebra.Homology.Opposite
 import Mathlib.Algebra.Homology.QuasiIso
+import Mathlib.Algebra.Homology.Refinements
 import Mathlib.Algebra.Homology.ShortComplex.Ab
 import Mathlib.Algebra.Homology.ShortComplex.Abelian
 import Mathlib.Algebra.Homology.ShortComplex.Basic

Mathlib/Algebra/Homology/HomologySequenceLemmas.lean

@@ -72,7 +72,7 @@ noncomputable def composableArrows₅ (i j : ι) (hij : c.Rel i j) : ComposableA
   mk₅ (homologyMap S₁.f i) (homologyMap S₁.g i) (hS₁.δ i j hij)
     (homologyMap S₁.f j) (homologyMap S₁.g j)
 
-lemma composableArrows₅_exact (i j : ι) (hij : c.Rel i j):
+lemma composableArrows₅_exact (i j : ι) (hij : c.Rel i j) :
     (composableArrows₅ hS₁ i j hij).Exact :=
   exact_of_δ₀ (hS₁.homology_exact₂ i).exact_toComposableArrows
     (exact_of_δ₀ (hS₁.homology_exact₃ i j hij).exact_toComposableArrows

Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean

@@ -174,6 +174,17 @@ lemma ext_from_iff (i j : ℤ) (hij : j + 1 = i) {A : C} (f g : (mappingCone φ)
   · rintro ⟨h₁, h₂⟩
     exact ext_from φ i j hij h₁ h₂
 
+lemma decomp_to {i : ℤ} {A : C} (f : A ⟶ (mappingCone φ).X i) (j : ℤ) (hij : i + 1 = j) :
+    ∃ (a : A ⟶ F.X j) (b : A ⟶ G.X i), f = a ≫ (inl φ).v j i (by omega) + b ≫ (inr φ).f i :=
+  ⟨f ≫ (fst φ).1.v i j hij, f ≫ (snd φ).v i i (add_zero i),
+    by apply ext_to φ i j hij <;> simp⟩
+
+lemma decomp_from {j : ℤ} {A : C} (f : (mappingCone φ).X j ⟶ A) (i : ℤ) (hij : j + 1 = i) :
+    ∃ (a : F.X i ⟶ A) (b : G.X j ⟶ A),
+      f = (fst φ).1.v j i hij ≫ a + (snd φ).v j j (add_zero j) ≫ b :=
+  ⟨(inl φ).v i j (by omega) ≫ f, (inr φ).f j ≫ f,
+    by apply ext_from φ i j hij <;> simp⟩
+
 lemma ext_cochain_to_iff (i j : ℤ) (hij : i + 1 = j)
     {K : CochainComplex C ℤ} {γ₁ γ₂ : Cochain K (mappingCone φ) i} :
     γ₁ = γ₂ ↔ γ₁.comp (fst φ).1 hij = γ₂.comp (fst φ).1 hij ∧

Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean

@@ -124,6 +124,11 @@ instance {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) [QuasiIso φ] :
     change IsIso (homologyMap φ _)
     infer_instance
 
+variable (C) in
+lemma homologyFunctor_shift (n : ℤ) :
+    (homologyFunctor C (ComplexShape.up ℤ) 0).shift n =
+      homologyFunctor C (ComplexShape.up ℤ) n := rfl
+
 end CochainComplex
 
 namespace HomotopyCategory

Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean

@@ -0,0 +1,143 @@
+/-
+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.HomotopyCategory.HomologicalFunctor
+import Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
+import Mathlib.Algebra.Homology.HomologySequenceLemmas
+import Mathlib.Algebra.Homology.Refinements
+
+/-!
+# The mapping cone of a monomorphism, up to a quasi-isomophism
+
+If `S` is a short exact short complex of cochain complexes in an abelian category,
+we construct a quasi-isomorphism `descShortComplex S : mappingCone S.f ⟶ S.X₃`.
+
+We obtain this by comparing the homology sequence of `S` and the homology
+sequence of the homology functor on the homotopy category, applied to the triangle
+attached to the mapping cone of `S.f`.
+
+-/
+
+open CategoryTheory Category ComplexShape HomotopyCategory Limits
+  HomologicalComplex.HomologySequence Pretriangulated Preadditive
+
+variable {C : Type*} [Category C] [Abelian C]
+
+namespace CochainComplex
+
+section
+
+variable (T : Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁)
+
+@[reassoc]
+lemma homologySequenceδ_quotient_mapTriangle_obj :
+    (homologyFunctor C (up ℤ) 0).homologySequenceδ
+        ((quotient C (up ℤ)).mapTriangle.obj T) n₀ n₁ h =
+      (homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫
+        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap T.mor₃ n₀ n₁ (by omega) ≫
+        (homologyFunctorFactors C (up ℤ) n₁).inv.app _ := by
+  sorry
+
+end
+
+namespace mappingCone
+
+variable (S : ShortComplex (CochainComplex C ℤ)) (hS : S.ShortExact)
+
+/-- The canonical morphism `mappingCone S.f ⟶ S.X₃` when `S` is a short complex
+of cochain complexes. -/
+noncomputable def descShortComplex : mappingCone S.f ⟶ S.X₃ := desc S.f 0 S.g (by simp)
+
+@[reassoc (attr := simp)]
+lemma inr_descShortComplex : inr S.f ≫ descShortComplex S = S.g := by
+  simp [descShortComplex]
+
+@[reassoc (attr := simp)]
+lemma inr_f_descShortComplex_f (n : ℤ) : (inr S.f).f n ≫ (descShortComplex S).f n = S.g.f n := by
+  simp [descShortComplex]
+
+@[reassoc (attr := simp)]
+lemma inl_v_descShortComplex_f (i j : ℤ) (h : i + (-1) = j) :
+    (inl S.f).v i j h ≫ (descShortComplex S).f j = 0 := by
+  simp [descShortComplex]
+
+variable {S}
+
+lemma homologySequenceδ_triangleh (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) :
+    (homologyFunctor C (up ℤ) 0).homologySequenceδ (triangleh S.f) n₀ n₁ h =
+      (homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫
+        HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫
+          (homologyFunctorFactors C (up ℤ) n₁).inv.app _ := by
+  dsimp
+  rw [← cancel_mono ((homologyFunctorFactors C (up ℤ) n₁).hom.app _),
+    assoc, assoc, assoc, Iso.inv_hom_id_app,
+    ← cancel_epi ((homologyFunctorFactors C (up ℤ) n₀).inv.app _), Iso.inv_hom_id_app_assoc]
+  dsimp
+  rw [comp_id]
+  apply yoneda.map_injective
+  ext ⟨A⟩ (x : A ⟶ _)
+  dsimp
+  obtain ⟨A', π, _, x', w, hx'⟩ :=
+    (mappingCone S.f).eq_liftCycles_homologyπ_up_to_refinements x n₁ (by simpa using h)
+  erw [homologySequenceδ_quotient_mapTriangle_obj_assoc _ _ _ h]
+  dsimp
+  rw [Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
+  erw [comp_id]
+  rw [← cancel_epi π, reassoc_of% hx', reassoc_of% hx',
+    HomologicalComplex.homologyπ_naturality_assoc,
+    HomologicalComplex.liftCycles_comp_cyclesMap_assoc]
+  obtain ⟨a, b, hab⟩ := decomp_to _ x' n₁ h
+  rw [hab, ext_to_iff _ n₁ (n₁ + 1) rfl, add_comp, assoc, assoc, inr_f_d, add_comp, assoc,
+    assoc, assoc, assoc, inr_f_fst_v, comp_zero, comp_zero, add_zero, zero_comp,
+    d_fst_v _ _ _ _ h, comp_neg, inl_v_fst_v_assoc, comp_neg, neg_eq_zero,
+    add_comp, assoc, assoc, assoc, assoc, inr_f_snd_v, comp_id, zero_comp,
+    d_snd_v _ _ _ h, comp_add, inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, add_zero] at w
+  conv_rhs => simp only [hab, add_comp, assoc, inr_f_descShortComplex_f,
+    inl_v_descShortComplex_f, comp_zero, zero_add]
+  rw [hS.δ_eq n₀ n₁ (by simpa using h) (b ≫ S.g.f n₀) _ b rfl (-a)
+    (by simp only [neg_comp, neg_eq_iff_add_eq_zero, w.2]) (n₁ + 1) (by simp)]
+  dsimp [Functor.shiftMap, homologyFunctor_shift]
+  rw [HomologicalComplex.homologyπ_naturality_assoc,
+    HomologicalComplex.liftCycles_comp_cyclesMap_assoc]
+  sorry
+
+open ComposableArrows
+
+set_option simprocs false
+
+lemma quasiIso_descShortComplex : QuasiIso (descShortComplex S) where
+  quasiIsoAt n := by
+    rw [quasiIsoAt_iff_isIso_homologyMap]
+    let φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅
+        (triangleh S.f) n _ rfl).δlast ⟶ (composableArrows₅ hS n _ rfl).δlast :=
+      homMk₄ ((homologyFunctorFactors C (up ℤ) _).hom.app _)
+        ((homologyFunctorFactors C (up ℤ) _).hom.app _)
+        ((homologyFunctorFactors C (up ℤ) _).hom.app _ ≫
+          HomologicalComplex.homologyMap (descShortComplex S) n)
+        ((homologyFunctorFactors C (up ℤ) _).hom.app _)
+        ((homologyFunctorFactors C (up ℤ) _).hom.app _)
+        ((homologyFunctorFactors C (up ℤ) _).hom.naturality S.f)
+        (by
+          erw [(homologyFunctorFactors C (up ℤ) n).hom.naturality_assoc]
+          dsimp
+          rw [← HomologicalComplex.homologyMap_comp, inr_descShortComplex])
+        (by
+          dsimp
+          erw [homologySequenceδ_triangleh hS]
+          simp only [Functor.comp_obj, HomologicalComplex.homologyFunctor_obj, assoc,
+            Iso.inv_hom_id_app, comp_id])
+        ((homologyFunctorFactors C (up ℤ) _).hom.naturality S.f)
+    have : IsIso ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
+        HomologicalComplex.homologyMap (descShortComplex S) n) := by
+      apply Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
+        ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅_exact _
+          (mappingCone_triangleh_distinguished S.f) n _ rfl).δlast
+        (composableArrows₅_exact hS n _ rfl).δlast φ
+      all_goals dsimp [φ]; infer_instance
+    apply IsIso.of_isIso_comp_left ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f))
+
+end mappingCone
+
+end CochainComplex

Mathlib/Algebra/Homology/Refinements.lean

@@ -0,0 +1,24 @@
+/-
+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.CategoryTheory.Abelian.Refinements
+import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
+
+open CategoryTheory
+
+variable {C ι : Type*} [Category C] [Abelian C] {c : ComplexShape ι}
+  (K : HomologicalComplex C c)
+
+namespace HomologicalComplex
+
+lemma eq_liftCycles_homologyπ_up_to_refinements {A : C} {i : ι} (γ : A ⟶ K.homology i)
+  (j : ι) (hj : c.next i = j) :
+    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ K.X i) (hz : z ≫ K.d i j = 0),
+      π ≫ γ = K.liftCycles z j hj hz ≫ K.homologyπ i := by
+  subst hj
+  exact (K.sc i).eq_liftCycles_homologyπ_up_to_refinements γ
+
+end HomologicalComplex

Mathlib/CategoryTheory/Abelian/Refinements.lean

@@ -110,4 +110,13 @@ lemma ShortComplex.Exact.exact_up_to_refinements
   rw [ShortComplex.exact_iff_exact_up_to_refinements] at hS
   exact hS x₂ hx₂
 
+lemma ShortComplex.eq_liftCycles_homologyπ_up_to_refinements {A : C} (γ : A ⟶ S.homology) :
+    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ S.X₂) (hz : z ≫ S.g = 0),
+      π ≫ γ = S.liftCycles z hz ≫ S.homologyπ := by
+  obtain ⟨A', π, hπ, z, hz⟩ := surjective_up_to_refinements_of_epi S.homologyπ γ
+  refine' ⟨A', π, hπ, z ≫ S.iCycles, by simp, _⟩
+  rw [hz]
+  congr 1
+  rw [← cancel_mono S.iCycles, liftCycles_i]
+
 end CategoryTheory

Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Homology.ShortComplex.Exact
 import Mathlib.CategoryTheory.Shift.ShiftSequence
 import Mathlib.CategoryTheory.Triangulated.Functor
 import Mathlib.CategoryTheory.Triangulated.Subcategory
+import Mathlib.Algebra.Homology.ExactSequence
 
 /-! # Homological functors
 
@@ -237,6 +238,21 @@ lemma mem_homologicalKernel_W_iff {X Y : C} (f : X ⟶ Y) :
   · intros
     constructor <;> infer_instance
 
+open ComposableArrows
+
+/-- The exact sequence with six terms starting from `(F.shift n₀).obj T.obj₁` until
+`(F.shift n₁).obj T.obj₃` when `T` is a distinguished triangle and `F` a homological functor. -/
+@[simp] noncomputable def homologySequenceComposableArrows₅ : ComposableArrows A 5 :=
+  mk₅ ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂)
+    (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ((F.shift n₁).map T.mor₂)
+
+lemma homologySequenceComposableArrows₅_exact :
+    (F.homologySequenceComposableArrows₅ T n₀ n₁ h).Exact :=
+  exact_of_δ₀ (F.homologySequence_exact₂ T hT n₀).exact_toComposableArrows
+    (exact_of_δ₀ (F.homologySequence_exact₃ T hT n₀ n₁ h).exact_toComposableArrows
+      (exact_of_δ₀ (F.homologySequence_exact₁ T hT n₀ n₁ h).exact_toComposableArrows
+        (F.homologySequence_exact₂ T hT n₁).exact_toComposableArrows))
+
 end
 
 end Functor