[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

@@ -18,7 +18,7 @@ and `HomotopyCategory` namespaces.
 
 -/
 
-open CategoryTheory Category
+open CategoryTheory Category ComplexShape Limits
 
 variable (C : Type*) [Category C] [Preadditive C]
 
@@ -124,6 +124,34 @@ 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
+
+@[reassoc]
+lemma liftCycles_shift_homologyπ
+    (K : CochainComplex C ℤ) {A : C} {n i : ℤ} (f : A ⟶ (K⟦n⟧).X i) (j : ℤ)
+    (hj : (up ℤ).next i = j) (hf : f ≫ (K⟦n⟧).d i j = 0) (i' : ℤ) (hi' : n + i = i') (j' : ℤ)
+    (hj' : (up ℤ).next i' = j') :
+    (K⟦n⟧).liftCycles f j hj hf ≫ (K⟦n⟧).homologyπ i =
+      K.liftCycles (f ≫ (K.shiftFunctorObjXIso n i i' (by omega)).hom) j' hj' (by
+        simp only [next] at hj hj'
+        obtain rfl : i' = i + n := by omega
+        obtain rfl : j' = j + n := by omega
+        dsimp at hf ⊢
+        simp only [Linear.comp_units_smul] at hf
+        apply (one_smul (M := ℤˣ) _).symm.trans _
+        rw [← Int.units_mul_self n.negOnePow, mul_smul, comp_id, hf, smul_zero]) ≫
+        K.homologyπ i' ≫
+          ((HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftIso n i i' hi').inv.app K := by
+  simp only [liftCycles, homologyπ,
+    shiftFunctorObjXIso, Functor.shiftIso, Functor.ShiftSequence.shiftIso,
+    ShiftSequence.shiftIso_inv_app, ShortComplex.homologyπ_naturality,
+    ShortComplex.liftCycles_comp_cyclesMap_assoc, shiftShortComplexFunctorIso_inv_app_τ₂,
+    assoc, Iso.hom_inv_id, comp_id]
+  rfl
+
 end CochainComplex
 
 namespace HomotopyCategory
@@ -147,4 +175,14 @@ lemma homologyShiftIso_hom_app (n a a' : ℤ) (ha' : n + a = a') (K : CochainCom
       (homologyFunctorFactors _ _ a').inv.app K := by
   apply Functor.ShiftSequence.induced_shiftIso_hom_app_obj
 
+@[reassoc]
+lemma homologyFunctor_shiftMap
+    {K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ L⟦n⟧) (a a' : ℤ) (h : n + a = a') :
+    (homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap
+      ((quotient _ _).map f ≫ ((quotient _ _).commShiftIso n).hom.app _) a a' h =
+        (homologyFunctorFactors _ _ a).hom.app K ≫
+          (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
+            (homologyFunctorFactors _ _ a').inv.app L := by
+  apply Functor.ShiftSequence.induced_shiftMap
+
 end HomotopyCategory

Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean

@@ -0,0 +1,146 @@
+/-
+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
+distinguished 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
+
+@[reassoc]
+lemma homologySequenceδ_quotient_mapTriangle_obj
+    (T : Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :
+    (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
+  apply homologyFunctor_shiftMap
+
+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
+  /- We proceed by diagram chase. We test the identity on
+     cocycles `x' : A' ⟶ (mappingCone S.f).X n₀` -/
+  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]
+  apply yoneda.map_injective
+  ext ⟨A⟩ (x : A ⟶ _)
+  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 [comp_id, 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]
+  /- We decompose the cocycle `x'` into two morphisms `a : A' ⟶ S.X₁.X n₁`
+     and `b : A' ⟶ S.X₂.X n₀` satisfying certain relations. -/
+  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
+  /- We simplify the RHS. -/
+  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)]
+  /- We simplify the LHS. -/
+  dsimp [Functor.shiftMap, homologyFunctor_shift]
+  rw [HomologicalComplex.homologyπ_naturality_assoc,
+    HomologicalComplex.liftCycles_comp_cyclesMap_assoc,
+    S.X₁.liftCycles_shift_homologyπ_assoc _ _ _ _ n₁ (by omega) (n₁ + 1) (by simp),
+    Iso.inv_hom_id_app]
+  dsimp [homologyFunctor_shift]
+  simp only [hab, add_comp, assoc, inl_v_triangle_mor₃_f_assoc,
+    shiftFunctorObjXIso, neg_comp, Iso.inv_hom_id, comp_neg, comp_id,
+    inr_f_triangle_mor₃_f_assoc, zero_comp, comp_zero, add_zero]
+
+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,34 @@
+/-
+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
+
+/-!
+# Refinements
+
+This file contains lemmas about "refinements" that are specific to
+the study of the homology of `HomologicalComplex`. General
+lemmas about refinements and the case of `ShortComplex` appear
+in the file `CategoryTheory.Abelian.Refinements`.
+
+-/
+
+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/Shift/InducedShiftSequence.lean

@@ -119,6 +119,18 @@ lemma induced_shiftIso_hom_app_obj (n a a' : M) (ha' : n + a = a') (X : C) :
         (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X := by
   apply induced.shiftIso_hom_app_obj
 
+@[reassoc]
+lemma induced_shiftMap {n : M} {X Y : C} (f : X ⟶ Y⟦n⟧) (a a' : M) (h : n + a = a') :
+    letI := induced e M F' e'
+    F.shiftMap (L.map f ≫ (L.commShiftIso n).hom.app _) a a' h =
+      (e' a).hom.app X ≫ G.shiftMap f a a' h ≫ (e' a').inv.app Y := by
+  dsimp [shiftMap]
+  rw [Functor.map_comp, induced_shiftIso_hom_app_obj, assoc, assoc]
+  nth_rw 2 [← Functor.map_comp_assoc]
+  simp only [comp_obj, Iso.hom_inv_id_app, map_id, id_comp]
+  rw [← NatTrans.naturality_assoc]
+  rfl
+
 end ShiftSequence
 
 end Functor

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