Skip to content

Commit dabb74d

Browse files
joelrioudagurtomas
joelriou
authored and
dagurtomas
committed
feat: the mapping cone of a monomorphism, up to a quasi-isomorphism (#13675)
In this PR, given a short exact sequence `S` in the category of cochain complexes in an abelian category, we compare the homology sequence of `S`, and the homology sequence of the homological functor on the homotopy category applied to the distinguished triangle of the mapping cone of the monomorphism `S.f`. In particular, up to a quasi-isomorphism, the mapping cone of `S.f` identifies to `S.X₃`. In future PRs, this shall be used in order to attach a distinguished triangle in the derived category to `S` (#13742), and compare the homology sequence of `S` and the homology sequence attached to this distinguished triangle. Co-authored-by: Joël Riou <[email protected]>
1 parent 64b5bd8 commit dabb74d

File tree

9 files changed

+270
-2
lines changed

9 files changed

+270
-2
lines changed

‎Mathlib.lean

+2
Original file line numberDiff line numberDiff line change
@@ -320,6 +320,7 @@ import Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
320320
import Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
321321
import Mathlib.Algebra.Homology.HomotopyCategory.Shift
322322
import Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
323+
import Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
323324
import Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
324325
import Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
325326
import Mathlib.Algebra.Homology.HomotopyCofiber
@@ -330,6 +331,7 @@ import Mathlib.Algebra.Homology.Localization
330331
import Mathlib.Algebra.Homology.ModuleCat
331332
import Mathlib.Algebra.Homology.Opposite
332333
import Mathlib.Algebra.Homology.QuasiIso
334+
import Mathlib.Algebra.Homology.Refinements
333335
import Mathlib.Algebra.Homology.ShortComplex.Ab
334336
import Mathlib.Algebra.Homology.ShortComplex.Abelian
335337
import Mathlib.Algebra.Homology.ShortComplex.Basic

‎Mathlib/Algebra/Homology/HomologySequenceLemmas.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ noncomputable def composableArrows₅ (i j : ι) (hij : c.Rel i j) : ComposableA
7272
mk₅ (homologyMap S₁.f i) (homologyMap S₁.g i) (hS₁.δ i j hij)
7373
(homologyMap S₁.f j) (homologyMap S₁.g j)
7474

75-
lemma composableArrows₅_exact (i j : ι) (hij : c.Rel i j):
75+
lemma composableArrows₅_exact (i j : ι) (hij : c.Rel i j) :
7676
(composableArrows₅ hS₁ i j hij).Exact :=
7777
exact_of_δ₀ (hS₁.homology_exact₂ i).exact_toComposableArrows
7878
(exact_of_δ₀ (hS₁.homology_exact₃ i j hij).exact_toComposableArrows

‎Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean

+11
Original file line numberDiff line numberDiff line change
@@ -174,6 +174,17 @@ lemma ext_from_iff (i j : ℤ) (hij : j + 1 = i) {A : C} (f g : (mappingCone φ)
174174
· rintro ⟨h₁, h₂⟩
175175
exact ext_from φ i j hij h₁ h₂
176176

177+
lemma decomp_to {i : ℤ} {A : C} (f : A ⟶ (mappingCone φ).X i) (j : ℤ) (hij : i + 1 = j) :
178+
∃ (a : A ⟶ F.X j) (b : A ⟶ G.X i), f = a ≫ (inl φ).v j i (by omega) + b ≫ (inr φ).f i :=
179+
⟨f ≫ (fst φ).1.v i j hij, f ≫ (snd φ).v i i (add_zero i),
180+
by apply ext_to φ i j hij <;> simp⟩
181+
182+
lemma decomp_from {j : ℤ} {A : C} (f : (mappingCone φ).X j ⟶ A) (i : ℤ) (hij : j + 1 = i) :
183+
∃ (a : F.X i ⟶ A) (b : G.X j ⟶ A),
184+
f = (fst φ).1.v j i hij ≫ a + (snd φ).v j j (add_zero j) ≫ b :=
185+
⟨(inl φ).v i j (by omega) ≫ f, (inr φ).f j ≫ f,
186+
by apply ext_from φ i j hij <;> simp⟩
187+
177188
lemma ext_cochain_to_iff (i j : ℤ) (hij : i + 1 = j)
178189
{K : CochainComplex C ℤ} {γ₁ γ₂ : Cochain K (mappingCone φ) i} :
179190
γ₁ = γ₂ ↔ γ₁.comp (fst φ).1 hij = γ₂.comp (fst φ).1 hij ∧

‎Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean

+39-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ and `HomotopyCategory` namespaces.
1818
1919
-/
2020

21-
open CategoryTheory Category
21+
open CategoryTheory Category ComplexShape Limits
2222

2323
variable (C : Type*) [Category C] [Preadditive C]
2424

@@ -124,6 +124,34 @@ instance {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) [QuasiIso φ] :
124124
change IsIso (homologyMap φ _)
125125
infer_instance
126126

127+
variable (C) in
128+
lemma homologyFunctor_shift (n : ℤ) :
129+
(homologyFunctor C (ComplexShape.up ℤ) 0).shift n =
130+
homologyFunctor C (ComplexShape.up ℤ) n := rfl
131+
132+
@[reassoc]
133+
lemma liftCycles_shift_homologyπ
134+
(K : CochainComplex C ℤ) {A : C} {n i : ℤ} (f : A ⟶ (K⟦n⟧).X i) (j : ℤ)
135+
(hj : (up ℤ).next i = j) (hf : f ≫ (K⟦n⟧).d i j = 0) (i' : ℤ) (hi' : n + i = i') (j' : ℤ)
136+
(hj' : (up ℤ).next i' = j') :
137+
(K⟦n⟧).liftCycles f j hj hf ≫ (K⟦n⟧).homologyπ i =
138+
K.liftCycles (f ≫ (K.shiftFunctorObjXIso n i i' (by omega)).hom) j' hj' (by
139+
simp only [next] at hj hj'
140+
obtain rfl : i' = i + n := by omega
141+
obtain rfl : j' = j + n := by omega
142+
dsimp at hf ⊢
143+
simp only [Linear.comp_units_smul] at hf
144+
apply (one_smul (M := ℤˣ) _).symm.trans _
145+
rw [← Int.units_mul_self n.negOnePow, mul_smul, comp_id, hf, smul_zero]) ≫
146+
K.homologyπ i' ≫
147+
((HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftIso n i i' hi').inv.app K := by
148+
simp only [liftCycles, homologyπ,
149+
shiftFunctorObjXIso, Functor.shiftIso, Functor.ShiftSequence.shiftIso,
150+
ShiftSequence.shiftIso_inv_app, ShortComplex.homologyπ_naturality,
151+
ShortComplex.liftCycles_comp_cyclesMap_assoc, shiftShortComplexFunctorIso_inv_app_τ₂,
152+
assoc, Iso.hom_inv_id, comp_id]
153+
rfl
154+
127155
end CochainComplex
128156

129157
namespace HomotopyCategory
@@ -147,4 +175,14 @@ lemma homologyShiftIso_hom_app (n a a' : ℤ) (ha' : n + a = a') (K : CochainCom
147175
(homologyFunctorFactors _ _ a').inv.app K := by
148176
apply Functor.ShiftSequence.induced_shiftIso_hom_app_obj
149177

178+
@[reassoc]
179+
lemma homologyFunctor_shiftMap
180+
{K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ L⟦n⟧) (a a' : ℤ) (h : n + a = a') :
181+
(homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap
182+
((quotient _ _).map f ≫ ((quotient _ _).commShiftIso n).hom.app _) a a' h =
183+
(homologyFunctorFactors _ _ a).hom.app K ≫
184+
(HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
185+
(homologyFunctorFactors _ _ a').inv.app L := by
186+
apply Functor.ShiftSequence.induced_shiftMap
187+
150188
end HomotopyCategory

‎Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean

+146
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
1+
/-
2+
Copyright (c) 2024 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
import Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
7+
import Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
8+
import Mathlib.Algebra.Homology.HomologySequenceLemmas
9+
import Mathlib.Algebra.Homology.Refinements
10+
11+
/-!
12+
# The mapping cone of a monomorphism, up to a quasi-isomophism
13+
14+
If `S` is a short exact short complex of cochain complexes in an abelian category,
15+
we construct a quasi-isomorphism `descShortComplex S : mappingCone S.f ⟶ S.X₃`.
16+
17+
We obtain this by comparing the homology sequence of `S` and the homology
18+
sequence of the homology functor on the homotopy category, applied to the
19+
distinguished triangle attached to the mapping cone of `S.f`.
20+
21+
-/
22+
23+
open CategoryTheory Category ComplexShape HomotopyCategory Limits
24+
HomologicalComplex.HomologySequence Pretriangulated Preadditive
25+
26+
variable {C : Type*} [Category C] [Abelian C]
27+
28+
namespace CochainComplex
29+
30+
@[reassoc]
31+
lemma homologySequenceδ_quotient_mapTriangle_obj
32+
(T : Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :
33+
(homologyFunctor C (up ℤ) 0).homologySequenceδ
34+
((quotient C (up ℤ)).mapTriangle.obj T) n₀ n₁ h =
35+
(homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫
36+
(HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap T.mor₃ n₀ n₁ (by omega) ≫
37+
(homologyFunctorFactors C (up ℤ) n₁).inv.app _ := by
38+
apply homologyFunctor_shiftMap
39+
40+
namespace mappingCone
41+
42+
variable (S : ShortComplex (CochainComplex C ℤ)) (hS : S.ShortExact)
43+
44+
/-- The canonical morphism `mappingCone S.f ⟶ S.X₃` when `S` is a short complex
45+
of cochain complexes. -/
46+
noncomputable def descShortComplex : mappingCone S.f ⟶ S.X₃ := desc S.f 0 S.g (by simp)
47+
48+
@[reassoc (attr := simp)]
49+
lemma inr_descShortComplex : inr S.f ≫ descShortComplex S = S.g := by
50+
simp [descShortComplex]
51+
52+
@[reassoc (attr := simp)]
53+
lemma inr_f_descShortComplex_f (n : ℤ) : (inr S.f).f n ≫ (descShortComplex S).f n = S.g.f n := by
54+
simp [descShortComplex]
55+
56+
@[reassoc (attr := simp)]
57+
lemma inl_v_descShortComplex_f (i j : ℤ) (h : i + (-1) = j) :
58+
(inl S.f).v i j h ≫ (descShortComplex S).f j = 0 := by
59+
simp [descShortComplex]
60+
61+
variable {S}
62+
63+
lemma homologySequenceδ_triangleh (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) :
64+
(homologyFunctor C (up ℤ) 0).homologySequenceδ (triangleh S.f) n₀ n₁ h =
65+
(homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫
66+
HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫
67+
(homologyFunctorFactors C (up ℤ) n₁).inv.app _ := by
68+
/- We proceed by diagram chase. We test the identity on
69+
cocycles `x' : A' ⟶ (mappingCone S.f).X n₀` -/
70+
dsimp
71+
rw [← cancel_mono ((homologyFunctorFactors C (up ℤ) n₁).hom.app _),
72+
assoc, assoc, assoc, Iso.inv_hom_id_app,
73+
← cancel_epi ((homologyFunctorFactors C (up ℤ) n₀).inv.app _), Iso.inv_hom_id_app_assoc]
74+
apply yoneda.map_injective
75+
ext ⟨A⟩ (x : A ⟶ _)
76+
obtain ⟨A', π, _, x', w, hx'⟩ :=
77+
(mappingCone S.f).eq_liftCycles_homologyπ_up_to_refinements x n₁ (by simpa using h)
78+
erw [homologySequenceδ_quotient_mapTriangle_obj_assoc _ _ _ h]
79+
dsimp
80+
rw [comp_id, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
81+
erw [comp_id]
82+
rw [← cancel_epi π, reassoc_of% hx', reassoc_of% hx',
83+
HomologicalComplex.homologyπ_naturality_assoc,
84+
HomologicalComplex.liftCycles_comp_cyclesMap_assoc]
85+
/- We decompose the cocycle `x'` into two morphisms `a : A' ⟶ S.X₁.X n₁`
86+
and `b : A' ⟶ S.X₂.X n₀` satisfying certain relations. -/
87+
obtain ⟨a, b, hab⟩ := decomp_to _ x' n₁ h
88+
rw [hab, ext_to_iff _ n₁ (n₁ + 1) rfl, add_comp, assoc, assoc, inr_f_d, add_comp, assoc,
89+
assoc, assoc, assoc, inr_f_fst_v, comp_zero, comp_zero, add_zero, zero_comp,
90+
d_fst_v _ _ _ _ h, comp_neg, inl_v_fst_v_assoc, comp_neg, neg_eq_zero,
91+
add_comp, assoc, assoc, assoc, assoc, inr_f_snd_v, comp_id, zero_comp,
92+
d_snd_v _ _ _ h, comp_add, inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, add_zero] at w
93+
/- We simplify the RHS. -/
94+
conv_rhs => simp only [hab, add_comp, assoc, inr_f_descShortComplex_f,
95+
inl_v_descShortComplex_f, comp_zero, zero_add]
96+
rw [hS.δ_eq n₀ n₁ (by simpa using h) (b ≫ S.g.f n₀) _ b rfl (-a)
97+
(by simp only [neg_comp, neg_eq_iff_add_eq_zero, w.2]) (n₁ + 1) (by simp)]
98+
/- We simplify the LHS. -/
99+
dsimp [Functor.shiftMap, homologyFunctor_shift]
100+
rw [HomologicalComplex.homologyπ_naturality_assoc,
101+
HomologicalComplex.liftCycles_comp_cyclesMap_assoc,
102+
S.X₁.liftCycles_shift_homologyπ_assoc _ _ _ _ n₁ (by omega) (n₁ + 1) (by simp),
103+
Iso.inv_hom_id_app]
104+
dsimp [homologyFunctor_shift]
105+
simp only [hab, add_comp, assoc, inl_v_triangle_mor₃_f_assoc,
106+
shiftFunctorObjXIso, neg_comp, Iso.inv_hom_id, comp_neg, comp_id,
107+
inr_f_triangle_mor₃_f_assoc, zero_comp, comp_zero, add_zero]
108+
109+
open ComposableArrows
110+
111+
set_option simprocs false
112+
113+
lemma quasiIso_descShortComplex : QuasiIso (descShortComplex S) where
114+
quasiIsoAt n := by
115+
rw [quasiIsoAt_iff_isIso_homologyMap]
116+
let φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅
117+
(triangleh S.f) n _ rfl).δlast ⟶ (composableArrows₅ hS n _ rfl).δlast :=
118+
homMk₄ ((homologyFunctorFactors C (up ℤ) _).hom.app _)
119+
((homologyFunctorFactors C (up ℤ) _).hom.app _)
120+
((homologyFunctorFactors C (up ℤ) _).hom.app _ ≫
121+
HomologicalComplex.homologyMap (descShortComplex S) n)
122+
((homologyFunctorFactors C (up ℤ) _).hom.app _)
123+
((homologyFunctorFactors C (up ℤ) _).hom.app _)
124+
((homologyFunctorFactors C (up ℤ) _).hom.naturality S.f)
125+
(by
126+
erw [(homologyFunctorFactors C (up ℤ) n).hom.naturality_assoc]
127+
dsimp
128+
rw [← HomologicalComplex.homologyMap_comp, inr_descShortComplex])
129+
(by
130+
dsimp
131+
erw [homologySequenceδ_triangleh hS]
132+
simp only [Functor.comp_obj, HomologicalComplex.homologyFunctor_obj, assoc,
133+
Iso.inv_hom_id_app, comp_id])
134+
((homologyFunctorFactors C (up ℤ) _).hom.naturality S.f)
135+
have : IsIso ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
136+
HomologicalComplex.homologyMap (descShortComplex S) n) := by
137+
apply Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
138+
((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅_exact _
139+
(mappingCone_triangleh_distinguished S.f) n _ rfl).δlast
140+
(composableArrows₅_exact hS n _ rfl).δlast φ
141+
all_goals dsimp [φ]; infer_instance
142+
apply IsIso.of_isIso_comp_left ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f))
143+
144+
end mappingCone
145+
146+
end CochainComplex

‎Mathlib/Algebra/Homology/Refinements.lean

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
/-
2+
Copyright (c) 2024 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
7+
import Mathlib.CategoryTheory.Abelian.Refinements
8+
import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
9+
10+
/-!
11+
# Refinements
12+
13+
This file contains lemmas about "refinements" that are specific to
14+
the study of the homology of `HomologicalComplex`. General
15+
lemmas about refinements and the case of `ShortComplex` appear
16+
in the file `CategoryTheory.Abelian.Refinements`.
17+
18+
-/
19+
20+
open CategoryTheory
21+
22+
variable {C ι : Type*} [Category C] [Abelian C] {c : ComplexShape ι}
23+
(K : HomologicalComplex C c)
24+
25+
namespace HomologicalComplex
26+
27+
lemma eq_liftCycles_homologyπ_up_to_refinements {A : C} {i : ι} (γ : A ⟶ K.homology i)
28+
(j : ι) (hj : c.next i = j) :
29+
∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ K.X i) (hz : z ≫ K.d i j = 0),
30+
π ≫ γ = K.liftCycles z j hj hz ≫ K.homologyπ i := by
31+
subst hj
32+
exact (K.sc i).eq_liftCycles_homologyπ_up_to_refinements γ
33+
34+
end HomologicalComplex

‎Mathlib/CategoryTheory/Abelian/Refinements.lean

+9
Original file line numberDiff line numberDiff line change
@@ -110,4 +110,13 @@ lemma ShortComplex.Exact.exact_up_to_refinements
110110
rw [ShortComplex.exact_iff_exact_up_to_refinements] at hS
111111
exact hS x₂ hx₂
112112

113+
lemma ShortComplex.eq_liftCycles_homologyπ_up_to_refinements {A : C} (γ : A ⟶ S.homology) :
114+
∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ S.X₂) (hz : z ≫ S.g = 0),
115+
π ≫ γ = S.liftCycles z hz ≫ S.homologyπ := by
116+
obtain ⟨A', π, hπ, z, hz⟩ := surjective_up_to_refinements_of_epi S.homologyπ γ
117+
refine ⟨A', π, hπ, z ≫ S.iCycles, by simp, ?_⟩
118+
rw [hz]
119+
congr 1
120+
rw [← cancel_mono S.iCycles, liftCycles_i]
121+
113122
end CategoryTheory

‎Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean

+12
Original file line numberDiff line numberDiff line change
@@ -119,6 +119,18 @@ lemma induced_shiftIso_hom_app_obj (n a a' : M) (ha' : n + a = a') (X : C) :
119119
(G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X := by
120120
apply induced.shiftIso_hom_app_obj
121121

122+
@[reassoc]
123+
lemma induced_shiftMap {n : M} {X Y : C} (f : X ⟶ Y⟦n⟧) (a a' : M) (h : n + a = a') :
124+
letI := induced e M F' e'
125+
F.shiftMap (L.map f ≫ (L.commShiftIso n).hom.app _) a a' h =
126+
(e' a).hom.app X ≫ G.shiftMap f a a' h ≫ (e' a').inv.app Y := by
127+
dsimp [shiftMap]
128+
rw [Functor.map_comp, induced_shiftIso_hom_app_obj, assoc, assoc]
129+
nth_rw 2 [← Functor.map_comp_assoc]
130+
simp only [comp_obj, Iso.hom_inv_id_app, map_id, id_comp]
131+
rw [← NatTrans.naturality_assoc]
132+
rfl
133+
122134
end ShiftSequence
123135

124136
end Functor

‎Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean

+16
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Homology.ShortComplex.Exact
77
import Mathlib.CategoryTheory.Shift.ShiftSequence
88
import Mathlib.CategoryTheory.Triangulated.Functor
99
import Mathlib.CategoryTheory.Triangulated.Subcategory
10+
import Mathlib.Algebra.Homology.ExactSequence
1011

1112
/-! # Homological functors
1213
@@ -249,6 +250,21 @@ lemma mem_homologicalKernel_W_iff {X Y : C} (f : X ⟶ Y) :
249250
· intros
250251
constructor <;> infer_instance
251252

253+
open ComposableArrows
254+
255+
/-- The exact sequence with six terms starting from `(F.shift n₀).obj T.obj₁` until
256+
`(F.shift n₁).obj T.obj₃` when `T` is a distinguished triangle and `F` a homological functor. -/
257+
@[simp] noncomputable def homologySequenceComposableArrows₅ : ComposableArrows A 5 :=
258+
mk₅ ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂)
259+
(F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ((F.shift n₁).map T.mor₂)
260+
261+
lemma homologySequenceComposableArrows₅_exact :
262+
(F.homologySequenceComposableArrows₅ T n₀ n₁ h).Exact :=
263+
exact_of_δ₀ (F.homologySequence_exact₂ T hT n₀).exact_toComposableArrows
264+
(exact_of_δ₀ (F.homologySequence_exact₃ T hT n₀ n₁ h).exact_toComposableArrows
265+
(exact_of_δ₀ (F.homologySequence_exact₁ T hT n₀ n₁ h).exact_toComposableArrows
266+
(F.homologySequence_exact₂ T hT n₁).exact_toComposableArrows))
267+
252268
end
253269

254270
end Functor

0 commit comments

Comments
 (0)