Skip to content

Commit e78b025

Browse files
joelrioujoelriou
committed
feat(Algebra/Homology): the mapping cocone (#35929)
Given a morphism `φ : K ⟶ L` of cochain complexes, the mapping cone allows to obtain a triangle `K ⟶ L ⟶ mappingCone φ ⟶ ...`. In this PR, we define the mapping cocone, which fits in a rotated triangle: `mappingCocone φ ⟶ K ⟶ L ⟶ ...`.
1 parent 6fcaafd commit e78b025

File tree

2 files changed

+324
-0
lines changed

2 files changed

+324
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -618,6 +618,7 @@ public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
618618
public import Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
619619
public import Mathlib.Algebra.Homology.HomotopyCategory.KInjective
620620
public import Mathlib.Algebra.Homology.HomotopyCategory.KProjective
621+
public import Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
621622
public import Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
622623
public import Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
623624
public import Mathlib.Algebra.Homology.HomotopyCategory.Shift

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

Lines changed: 323 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,323 @@
1+
/-
2+
Copyright (c) 2026 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+
module
7+
8+
public import Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
9+
10+
/-!
11+
# The mapping cocone
12+
13+
Given a morphism `φ : K ⟶ L` of cochain complexes, the mapping cone
14+
allows to obtain a triangle `K ⟶ L ⟶ mappingCone φ ⟶ ...`. In this
15+
file, we define the mapping cocone, which fits in a rotated triangle:
16+
`mappingCocone φ ⟶ K ⟶ L ⟶ ...`.
17+
18+
-/
19+
20+
@[expose] public section
21+
22+
open CategoryTheory Limits HomologicalComplex Pretriangulated
23+
24+
namespace CochainComplex
25+
26+
open HomComplex
27+
28+
variable {C : Type*} [Category* C] [Preadditive C]
29+
{K L : CochainComplex C ℤ} (φ : K ⟶ L)
30+
31+
/-- The mapping cocone of a morphism `φ : K ⟶ L` of cochain complexes: it is
32+
`(mappingCone φ)⟦(-1 : ℤ)⟧`. -/
33+
noncomputable def mappingCocone [HasHomotopyCofiber φ] :
34+
CochainComplex C ℤ := (mappingCone φ)⟦(-1 : ℤ)⟧
35+
36+
namespace mappingCocone
37+
38+
section
39+
40+
variable [HasHomotopyCofiber φ]
41+
42+
/-- The first projection `mappingCocone φ ⟶ K`. -/
43+
noncomputable def fst : mappingCocone φ ⟶ K :=
44+
-((mappingCone.fst φ).leftShift (-1) 0 (add_neg_cancel 1)).homOf
45+
46+
/-- The second projection in `Cochain (mappingCocone φ) L (-1)`. -/
47+
noncomputable def snd : Cochain (mappingCocone φ) L (-1) :=
48+
(mappingCone.snd φ).leftShift (-1) (-1) (zero_add _)
49+
50+
/-- The left inclusion in `Cochain K (mappingCocone φ) 0`. -/
51+
noncomputable def inl : Cochain K (mappingCocone φ) 0 :=
52+
(mappingCone.inl φ).rightShift (-1) 0 (zero_add _)
53+
54+
/-- The right inclusion in `Cocycle L (mappingCocone φ) 1`. -/
55+
noncomputable def inr : Cocycle L (mappingCocone φ) 1 :=
56+
(Cocycle.ofHom (mappingCone.inr φ)).rightShift (-1) 1 (by lia)
57+
58+
set_option backward.isDefEq.respectTransparency false in
59+
@[reassoc (attr := simp)]
60+
lemma inl_v_fst_f (p : ℤ) :
61+
(inl φ).v p p (add_zero p) ≫ (fst φ).f p = 𝟙 _ := by
62+
simp [inl, fst, Cochain.rightShift_v (n := -1) _ _ _ _ p _ _ (p + -1) (by lia),
63+
Cochain.leftShift_v (n := 1) _ _ _ _ _ p _ (p + -1) (by lia)]
64+
65+
set_option backward.isDefEq.respectTransparency false in
66+
@[reassoc (attr := simp)]
67+
lemma inl_v_snd_v (p q : ℤ) (hpq : p + -1 = q) :
68+
(inl φ).v p p (add_zero p) ≫ (snd φ).v p q hpq = 0 := by
69+
obtain rfl : q = p + -1 := by lia
70+
simp [inl, snd, Cochain.rightShift_v (n := -1) _ _ _ _ p _ _ (p + -1) (by lia),
71+
Cochain.leftShift_v _ _ _ _ _ _ hpq]
72+
73+
set_option backward.isDefEq.respectTransparency false in
74+
@[reassoc (attr := simp)]
75+
lemma inr_v_fst_f (p q : ℤ) (hpq : p + 1 = q) :
76+
(inr φ).1.v p q hpq ≫ (fst φ).f q = 0 := by
77+
simp [inr, fst, Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero p),
78+
Cochain.leftShift_v _ _ _ _ _ _ _ _ hpq]
79+
80+
set_option backward.isDefEq.respectTransparency false in
81+
@[reassoc (attr := simp)]
82+
lemma inr_v_snd_v (p q : ℤ) (hpq : p + 1 = q) :
83+
(inr φ).1.v p q hpq ≫ (snd φ).v q p (by lia) = 𝟙 _ := by
84+
simp [inr, snd, Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero p),
85+
Cochain.leftShift_v _ _ _ _ _ _ _ _ (add_zero p),
86+
Int.negOnePow_even 2 ⟨1, rfl⟩]
87+
88+
set_option backward.isDefEq.respectTransparency false in
89+
lemma id_X (p q : ℤ) (hpq : p + -1 = q) :
90+
(fst φ).f p ≫ (inl φ).v p p (add_zero p) +
91+
(snd φ).v p q hpq ≫ (inr φ).1.v q p (by lia) = 𝟙 _ := by
92+
obtain rfl : q = p + -1 := by lia
93+
simp [fst, inl, snd, inr, mappingCocone,
94+
Cochain.leftShift_v (n := 1) _ _ _ _ _ p _ (p + -1) (by lia),
95+
Cochain.rightShift_v _ _ _ _ _ _ _ _ hpq,
96+
Cochain.leftShift_v _ _ _ _ _ _ _ _ (add_zero (p + -1)),
97+
Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero (p + -1)),
98+
Int.negOnePow_even 2 ⟨1, rfl⟩,
99+
mappingCone.id_X φ (p + -1) p (by lia)]
100+
101+
section
102+
103+
variable {M : CochainComplex C ℤ} {n m : ℤ}
104+
(α : Cochain K M m) (β : Cochain L M n) (h : m + 1 = n)
105+
106+
/-- Constructor for cochains from `mappingCocone`. -/
107+
noncomputable def descCochain : Cochain (mappingCocone φ) M m :=
108+
(-m + 1).negOnePow • (mappingCone.descCochain φ α β h).leftShift (-1) m (by lia)
109+
110+
set_option backward.isDefEq.respectTransparency false in
111+
@[reassoc (attr := simp)]
112+
lemma inl_v_descCochain_v (p q : ℤ) (hpq : p + m = q) :
113+
(inl φ).v p p (add_zero _) ≫ (descCochain φ α β h).v p q hpq = α.v p q hpq := by
114+
simp [inl, descCochain, mappingCocone,
115+
Cochain.rightShift_v (n := -1) _ _ _ _ p _ _ (p + -1) (by lia), smul_smul,
116+
Cochain.leftShift_v (n := n) _ (-1) m (by lia) _ _ hpq (p + -1) (by lia)]
117+
118+
set_option backward.isDefEq.respectTransparency false in
119+
@[reassoc (attr := simp)]
120+
lemma inr_v_descCochain_v (p q : ℤ) (hpq : p + 1 = q) (r : ℤ) (hr : q + m = r) :
121+
(inr φ).1.v p q hpq ≫ (descCochain φ α β h).v q r hr = β.v p r (by lia) := by
122+
obtain rfl : p = q + -1 := by lia
123+
simp [inr, descCochain, mappingCocone, smul_smul,
124+
Cochain.rightShift_v _ _ _ _ _ _ hpq _ (add_zero (q + -1)),
125+
Cochain.leftShift_v (n := n) _ _ _ _ _ r _ (q + -1) (by lia)]
126+
127+
@[simp]
128+
lemma inl_comp_descCochain :
129+
(inl φ).comp (descCochain φ α β h) (zero_add m) = α := by
130+
cat_disch
131+
132+
@[simp]
133+
lemma inr_comp_descCochain :
134+
(inr φ).1.comp (descCochain φ α β h) (by lia) = β := by
135+
ext p q hpq
136+
simp [Cochain.comp_v (n₂ := m) _ _ _ _ (p + 1) q rfl (by lia)]
137+
138+
set_option backward.isDefEq.respectTransparency false in
139+
lemma δ_descCochain (n' : ℤ) (hn' : n + 1 = n') :
140+
δ m n (descCochain φ α β h) =
141+
(Cochain.ofHom (fst φ)).comp
142+
(δ m n α + m.negOnePow • (Cochain.ofHom φ).comp β (zero_add n)) (zero_add n) +
143+
(snd φ).comp (δ n n' β) (by lia) := by
144+
dsimp [descCochain, fst, snd, mappingCocone]
145+
ext p q hpq
146+
subst h
147+
obtain rfl : n' = m + 2 := by lia
148+
simp [Cochain.δ_leftShift _ (-1) _ (m + 1) _ (m + 2) (by lia),
149+
mappingCone.δ_descCochain (m := m) (n := m + 1) _ _ _ _ (m + 2) (by lia),
150+
Cochain.leftShift_v (n := 1) _ _ _ _ p p _ (p + -1) (by lia),
151+
Cochain.leftShift_v (n := m + 2) _ (-1) _ _ _ q _ (p + -1) (by lia),
152+
Cochain.leftShift_v _ _ _ _ _ _ _ _ (add_zero (p + -1)),
153+
Cochain.comp_v (n₁ := 1) _ _ _ (p + -1) p _ (by lia) hpq,
154+
Cochain.comp_v (n₂ := m + 2) _ _ _ p (p + -1) q rfl (by lia),
155+
smul_smul, Int.negOnePow_add, Int.negOnePow_even 2 ⟨1, rfl⟩]
156+
grind
157+
158+
end
159+
160+
/-- Constructor for cocycles from `mappingCocone`. -/
161+
@[simps]
162+
noncomputable def descCocycle {M : CochainComplex C ℤ} {n m : ℤ}
163+
(α : Cochain K M m) (β : Cocycle L M n) (h : m + 1 = n)
164+
(hαβ : δ m n α + m.negOnePow • (Cochain.ofHom φ).comp β.1 (zero_add n) = 0) :
165+
Cocycle (mappingCocone φ) M m :=
166+
⟨descCochain φ α β h, by
167+
simp [Cocycle.mem_iff _ n h, δ_descCochain _ _ _ h (n + 1) (by lia), hαβ]⟩
168+
169+
section
170+
171+
variable {M : CochainComplex C ℤ} (α : Cochain K M 0) (β : Cocycle L M 1)
172+
(hαβ : δ 0 1 α + (Cochain.ofHom φ).comp β.1 (zero_add 1) = 0)
173+
174+
/-- Constructor for morphisms from `mappingCocone`. -/
175+
noncomputable def desc : mappingCocone φ ⟶ M :=
176+
(descCocycle φ α β (zero_add 1) (by simpa)).homOf
177+
178+
@[simp]
179+
lemma ofHom_desc :
180+
Cochain.ofHom (desc φ α β hαβ) = descCochain φ α β.1 (by lia) := by
181+
simp [desc]
182+
183+
@[reassoc (attr := simp)]
184+
lemma inl_v_desc_f (p : ℤ) :
185+
(inl φ).v p p (add_zero p) ≫ (desc φ α β hαβ).f p = α.v p p (add_zero p) := by
186+
simp [desc]
187+
188+
@[reassoc (attr := simp)]
189+
lemma inr_v_desc_f (p q : ℤ) (hpq : p + 1 = q) :
190+
(inr φ).1.v p q hpq ≫ (desc φ α β hαβ).f q = β.1.v p q hpq := by
191+
simp [desc]
192+
193+
end
194+
195+
section
196+
197+
variable {M : CochainComplex C ℤ} {n m : ℤ}
198+
(α : Cochain M K n) (β : Cochain M L m) (h : m + 1 = n)
199+
200+
/-- Constructor for cochains to `mappingCocone`. -/
201+
noncomputable def liftCochain : Cochain M (mappingCocone φ) n :=
202+
(mappingCone.liftCochain φ α β h).rightShift (-1) n (by lia)
203+
204+
set_option backward.isDefEq.respectTransparency false in
205+
@[reassoc (attr := simp)]
206+
lemma liftCochain_v_fst_f (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) :
207+
(liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (fst φ).f p₂ = α.v p₁ p₂ h₁₂ := by
208+
simp [liftCochain, mappingCocone, fst,
209+
Cochain.rightShift_v (n := m) _ _ _ _ p₁ _ _ (p₂ + -1) (by lia),
210+
Cochain.leftShift_v (n := 1) _ _ _ _ _ p₂ _ (p₂ + -1) (by lia)]
211+
212+
set_option backward.isDefEq.respectTransparency false in
213+
@[reassoc (attr := simp)]
214+
lemma liftCochain_v_snd_v (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + -1 = p₃) :
215+
(liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (snd φ).v p₂ p₃ h₂₃ = β.v p₁ p₃ (by lia) := by
216+
subst h₂₃
217+
simp [liftCochain, mappingCocone, snd,
218+
Cochain.rightShift_v (n := m) _ _ _ _ p₁ _ _ (p₂ + -1) (by lia),
219+
Cochain.leftShift_v (n := 0) _ _ _ _ _ _ _ _ (add_zero _),
220+
Int.negOnePow_even 2 ⟨1, rfl⟩]
221+
222+
@[simp]
223+
lemma liftCochain_comp_fst :
224+
(liftCochain φ α β h).comp (Cochain.ofHom (fst φ)) (add_zero _) = α := by
225+
cat_disch
226+
227+
@[simp]
228+
lemma liftCochain_comp_snd :
229+
(liftCochain φ α β h).comp (snd φ) (by lia) = β := by
230+
ext p q hpq
231+
simp [Cochain.comp_v (n₁ := n) (n₂ := -1) (n₁₂ := m) _ _ _ p _ _ (by lia)
232+
(Int.add_neg_cancel_right q 1)]
233+
234+
set_option backward.isDefEq.respectTransparency false in
235+
lemma δ_liftCochain (n' : ℤ) (hn' : n + 1 = n') :
236+
δ n n' (liftCochain φ α β h) =
237+
(δ n n' α).comp (inl φ) (add_zero _) -
238+
(δ m n β + α.comp (Cochain.ofHom φ) (add_zero n)).comp (inr φ).1 hn' := by
239+
dsimp [liftCochain, inl, inr]
240+
ext p q hpq
241+
simp [mappingCone.δ_liftCochain _ _ _ _ n' hn',
242+
Cochain.δ_rightShift _ (-1) _ n' _ n (by lia),
243+
Cochain.rightShift_v (n := n) _ _ _ _ p _ _ (q + -1) (by lia),
244+
Cochain.rightShift_v _ _ _ _ _ _ _ (q + -1) rfl,
245+
Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero (q + -1)),
246+
Cochain.comp_v _ _ _ p q _ hpq rfl,
247+
Cochain.comp_v (n₁ := n) (n₂ := 1) _ _ _ p (q + -1) q (by lia) (by lia)]
248+
grind
249+
250+
end
251+
252+
/-- Constructor for cocycles to `mappingCocone`. -/
253+
@[simps]
254+
noncomputable def liftCocycle {M : CochainComplex C ℤ} {n m : ℤ}
255+
(α : Cocycle M K n) (β : Cochain M L m) (h : m + 1 = n)
256+
(hαβ : δ m n β + α.1.comp (Cochain.ofHom φ) (add_zero n) = 0) :
257+
Cocycle M (mappingCocone φ) n :=
258+
⟨liftCochain φ α β h,
259+
by simp [Cocycle.mem_iff _ _ rfl, δ_liftCochain _ _ _ _ _ rfl, hαβ]⟩
260+
261+
section
262+
263+
variable {M : CochainComplex C ℤ} (α : M ⟶ K) (β : Cochain M L (-1))
264+
(hαβ : δ (-1) 0 β + Cochain.ofHom (α ≫ φ) = 0)
265+
266+
/-- Constructor for morphisms to `mappingCocone`. -/
267+
noncomputable def lift : M ⟶ mappingCocone φ :=
268+
Cocycle.homOf (liftCocycle φ (Cocycle.ofHom α) β (by simp) (by simpa [← Cochain.ofHom_comp]))
269+
270+
@[simp]
271+
lemma ofHom_lift :
272+
Cochain.ofHom (lift φ α β hαβ) = liftCochain φ (Cochain.ofHom α) β (by simp) := by
273+
simp [lift]
274+
275+
@[reassoc (attr := simp)]
276+
lemma lift_f_fst_f (p : ℤ) :
277+
(lift φ α β hαβ).f p ≫ (fst φ).f p = α.f p := by
278+
simp [lift]
279+
280+
@[reassoc (attr := simp)]
281+
lemma lift_fst :
282+
lift φ α β hαβ ≫ fst φ = α := by
283+
cat_disch
284+
285+
@[reassoc (attr := simp)]
286+
lemma lift_f_snd_v (p q : ℤ) (hpq : p + (-1) = q) :
287+
(lift φ α β hαβ).f p ≫ (snd φ).v p q hpq = β.v p q hpq := by
288+
simp [lift]
289+
290+
end
291+
292+
end
293+
294+
section
295+
296+
variable [HasBinaryBiproducts C]
297+
298+
/-- Given a morphism `φ : K ⟶ L` of cochain complexes, this is the triangle
299+
`mappingCocone φ ⟶ K ⟶ L ⟶ ...`. -/
300+
@[simps! obj₁ obj₂ obj₃ mor₁ mor₂]
301+
noncomputable def triangle : Triangle (CochainComplex C ℤ) :=
302+
Triangle.mk (fst φ) φ
303+
((mappingCone.triangle φ).mor₂ ≫ (shiftFunctorCompIsoId _ (-1 : ℤ) 1 (by lia)).inv.app _)
304+
305+
set_option backward.isDefEq.respectTransparency false in
306+
/-- Rotating the triangle `mappingCocone.triangle φ` gives a triangle that is
307+
isomorphic to `mappingCone.triangle φ`. -/
308+
noncomputable def rotateTriangleIso :
309+
(triangle φ).rotate ≅ mappingCone.triangle φ := by
310+
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
311+
((shiftFunctorCompIsoId _ (-1 : ℤ) 1 (by lia)).app _)
312+
(by simp) (by simp [triangle]) ?_
313+
dsimp
314+
ext n
315+
simp [fst, mappingCone.triangle, Cochain.leftShift_v _ _ _ _ _ _ _ _ rfl,
316+
Cochain.rightShift_v _ _ _ _ _ _ _ _ rfl,
317+
shiftFunctorCompIsoId, shiftFunctorAdd'_inv_app_f', shiftFunctorZero_hom_app_f]
318+
319+
end
320+
321+
end mappingCocone
322+
323+
end CochainComplex

0 commit comments

Comments
 (0)