Skip to content

Commit e0f4e43

Browse files
joelrioujoelriou
committed
feat(Algebra/Homology): construction of the homotopy cofiber (#8969)
1 parent 7d3d6e4 commit e0f4e43

File tree

3 files changed

+243
-0
lines changed

3 files changed

+243
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -245,6 +245,7 @@ import Mathlib.Algebra.Homology.Homotopy
245245
import Mathlib.Algebra.Homology.HomotopyCategory
246246
import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
247247
import Mathlib.Algebra.Homology.HomotopyCategory.Shift
248+
import Mathlib.Algebra.Homology.HomotopyCofiber
248249
import Mathlib.Algebra.Homology.ImageToKernel
249250
import Mathlib.Algebra.Homology.LocalCohomology
250251
import Mathlib.Algebra.Homology.Localization

‎Mathlib/Algebra/Homology/Homotopy.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,11 @@ theorem dNext_eq (f : ∀ i j, C.X i ⟶ D.X j) {i i' : ι} (w : c.Rel i i') :
5656
rfl
5757
#align d_next_eq dNext_eq
5858

59+
lemma dNext_eq_zero (f : ∀ i j, C.X i ⟶ D.X j) (i : ι) (hi : ¬ c.Rel i (c.next i)) :
60+
dNext i f = 0 := by
61+
dsimp [dNext]
62+
rw [shape _ _ _ hi, zero_comp]
63+
5964
@[simp 1100]
6065
theorem dNext_comp_left (f : C ⟶ D) (g : ∀ i j, D.X i ⟶ E.X j) (i : ι) :
6166
(dNext i fun i j => f.f i ≫ g i j) = f.f i ≫ dNext i g :=
@@ -74,6 +79,11 @@ def prevD (j : ι) : (∀ i j, C.X i ⟶ D.X j) →+ (C.X j ⟶ D.X j) :=
7479
Preadditive.add_comp _ _ _ _ _ _
7580
#align prev_d prevD
7681

82+
lemma prevD_eq_zero (f : ∀ i j, C.X i ⟶ D.X j) (i : ι) (hi : ¬ c.Rel (c.prev i) i) :
83+
prevD i f = 0 := by
84+
dsimp [prevD]
85+
rw [shape _ _ _ hi, comp_zero]
86+
7787
/-- `f j (c.prev j)`. -/
7888
def toPrev (j : ι) : (∀ i j, C.X i ⟶ D.X j) →+ (C.X j ⟶ D.xPrev j) :=
7989
AddMonoidHom.mk' (fun f => f j (c.prev j)) fun _ _ => rfl

‎Mathlib/Algebra/Homology/HomotopyCofiber.lean‎

Lines changed: 232 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,232 @@
1+
/-
2+
Copyright (c) 2023 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.Homotopy
7+
8+
/-! The homotopy cofiber of a morphism of homological complexes
9+
10+
In this file, we construct the homotopy cofiber of a morphism `φ : F ⟶ G`
11+
between homological complexes in `HomologicalComplex C c`. In degree `i`,
12+
it is isomorphic to `(F.X j) ⊞ (G.X i)` if there is a `j` such that `c.Rel i j`,
13+
and `G.X i` otherwise. (This is also known as the mapping cone of `φ`. Under
14+
the name `CochainComplex.mappingCone`, a specific API shall be developed
15+
for the case of cochain complexes indexed by `ℤ` (TODO).)
16+
17+
When we assume `hc : ∀ j, ∃ i, c.Rel i j` (which holds in the case of chain complexes,
18+
or cochain complexes indexed by `ℤ`), then for any homological complex `K`,
19+
there is a bijection `HomologicalComplex.homotopyCofiber.descEquiv φ K hc`
20+
between `homotopyCofiber φ ⟶ K` and the tuples `(α, hα)` with
21+
`α : G ⟶ K` and `hα : Homotopy (φ ≫ α) 0` (TODO).
22+
23+
We shall also study the cylinder of a homological complex `K`: this is the
24+
homotopy cofiber of the morphism `biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K`.
25+
Then, a morphism `K.cylinder ⟶ M` is determined by the data of two
26+
morphisms `φ₀ φ₁ : K ⟶ M` and a homotopy `h : Homotopy φ₀ φ₁`,
27+
see `cylinder.desc`. There is also a homotopy equivalence
28+
`cylinder.homotopyEquiv K : HomotopyEquiv K.cylinder K`. From the construction of
29+
the cylinder, we deduce the lemma `Homotopy.map_eq_of_inverts_homotopyEquivalences`
30+
which assert that if a functor inverts homotopy equivalences, then the image of
31+
two homotopic maps are equal (TODO).
32+
33+
-/
34+
35+
36+
open CategoryTheory Category Limits Preadditive
37+
38+
variable {C : Type*} [Category C] [Preadditive C]
39+
40+
namespace HomologicalComplex
41+
42+
variable {ι : Type*} {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G)
43+
44+
/-- A morphism of homological complexes `φ : F ⟶ G` has a homotopy cofiber if for all
45+
indices `i` and `j` such that `c.Rel i j`, the binary biproduct `F.X j ⊞ G.X i` exists. -/
46+
class HasHomotopyCofiber (φ : F ⟶ G) : Prop where
47+
hasBinaryBiproduct (i j : ι) (hij : c.Rel i j) : HasBinaryBiproduct (F.X j) (G.X i)
48+
49+
instance [HasBinaryBiproducts C] : HasHomotopyCofiber φ where
50+
hasBinaryBiproduct _ _ _ := inferInstance
51+
52+
variable [HasHomotopyCofiber φ] [DecidableRel c.Rel]
53+
54+
namespace homotopyCofiber
55+
56+
/-- The `X` field of the homological complex `homotopyCofiber φ`. -/
57+
noncomputable def X (i : ι) : C :=
58+
if hi : c.Rel i (c.next i)
59+
then
60+
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hi
61+
(F.X (c.next i)) ⊞ (G.X i)
62+
else G.X i
63+
64+
/-- The canonical isomorphism `(homotopyCofiber φ).X i ≅ F.X j ⊞ G.X i` when `c.Rel i j`. -/
65+
noncomputable def XIsoBiprod (i j : ι) (hij : c.Rel i j) [HasBinaryBiproduct (F.X j) (G.X i)] :
66+
X φ i ≅ F.X j ⊞ G.X i :=
67+
eqToIso (by
68+
obtain rfl := c.next_eq' hij
69+
apply dif_pos hij)
70+
71+
/-- The canonical isomorphism `(homotopyCofiber φ).X i ≅ G.X i` when `¬ c.Rel i (c.next i)`. -/
72+
noncomputable def XIso (i : ι) (hi : ¬ c.Rel i (c.next i)) :
73+
X φ i ≅ G.X i :=
74+
eqToIso (dif_neg hi)
75+
76+
/-- The second projection `(homotopyCofiber φ).X i ⟶ G.X i`. -/
77+
noncomputable def sndX (i : ι) : X φ i ⟶ G.X i :=
78+
if hi : c.Rel i (c.next i)
79+
then
80+
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hi
81+
(XIsoBiprod φ _ _ hi).hom ≫ biprod.snd
82+
else
83+
(XIso φ i hi).hom
84+
85+
/-- The right inclusion `G.X i ⟶ (homotopyCofiber φ).X i`. -/
86+
noncomputable def inrX (i : ι) : G.X i ⟶ X φ i :=
87+
if hi : c.Rel i (c.next i)
88+
then
89+
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hi
90+
biprod.inr ≫ (XIsoBiprod φ _ _ hi).inv
91+
else
92+
(XIso φ i hi).inv
93+
94+
@[reassoc (attr := simp)]
95+
lemma inrX_sndX (i : ι) : inrX φ i ≫ sndX φ i = 𝟙 _ := by
96+
dsimp [sndX, inrX]
97+
split_ifs with hi <;> simp
98+
99+
@[reassoc]
100+
lemma sndX_inrX (i : ι) (hi : ¬ c.Rel i (c.next i)) :
101+
sndX φ i ≫ inrX φ i = 𝟙 _ := by
102+
dsimp [sndX, inrX]
103+
simp only [dif_neg hi, Iso.hom_inv_id]
104+
105+
/-- The first projection `(homotopyCofiber φ).X i ⟶ F.X j` when `c.Rel i j`. -/
106+
noncomputable def fstX (i j : ι) (hij : c.Rel i j) : X φ i ⟶ F.X j :=
107+
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
108+
(XIsoBiprod φ i j hij).hom ≫ biprod.fst
109+
110+
/-- The left inclusion `F.X i ⟶ (homotopyCofiber φ).X j` when `c.Rel j i`. -/
111+
noncomputable def inlX (i j : ι) (hij : c.Rel j i) : F.X i ⟶ X φ j :=
112+
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
113+
biprod.inl ≫ (XIsoBiprod φ j i hij).inv
114+
115+
@[reassoc (attr := simp)]
116+
lemma inlX_fstX (i j : ι ) (hij : c.Rel j i) :
117+
inlX φ i j hij ≫ fstX φ j i hij = 𝟙 _ := by
118+
simp [inlX, fstX]
119+
120+
@[reassoc (attr := simp)]
121+
lemma inlX_sndX (i j : ι) (hij : c.Rel j i) :
122+
inlX φ i j hij ≫ sndX φ j = 0 := by
123+
obtain rfl := c.next_eq' hij
124+
simp [inlX, sndX, dif_pos hij]
125+
126+
@[reassoc (attr := simp)]
127+
lemma inrX_fstX (i j : ι) (hij : c.Rel i j) :
128+
inrX φ i ≫ fstX φ i j hij = 0 := by
129+
obtain rfl := c.next_eq' hij
130+
simp [inrX, fstX, dif_pos hij]
131+
132+
/-- The `d` field of the homological complex `homotopyCofiber φ`. -/
133+
noncomputable def d (i j : ι) : X φ i ⟶ X φ j :=
134+
if hij : c.Rel i j
135+
then
136+
(if hj : c.Rel j (c.next j) then -fstX φ i j hij ≫ F.d _ _ ≫ inlX φ _ _ hj else 0) +
137+
fstX φ i j hij ≫ φ.f j ≫ inrX φ j + sndX φ i ≫ G.d i j ≫ inrX φ j
138+
else
139+
0
140+
141+
lemma ext_to_X (i j : ι) (hij : c.Rel i j) {A : C} {f g : A ⟶ X φ i}
142+
(h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij) (h₂ : f ≫ sndX φ i = g ≫ sndX φ i) :
143+
f = g := by
144+
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
145+
rw [← cancel_mono (XIsoBiprod φ i j hij).hom]
146+
apply biprod.hom_ext
147+
· simpa using h₁
148+
· obtain rfl := c.next_eq' hij
149+
simpa [sndX, dif_pos hij] using h₂
150+
151+
lemma ext_to_X' (i : ι) (hi : ¬ c.Rel i (c.next i)) {A : C} {f g : A ⟶ X φ i}
152+
(h : f ≫ sndX φ i = g ≫ sndX φ i) : f = g := by
153+
rw [← cancel_mono (XIso φ i hi).hom]
154+
simpa only [sndX, dif_neg hi] using h
155+
156+
lemma ext_from_X (i j : ι) (hij : c.Rel j i) {A : C} {f g : X φ j ⟶ A}
157+
(h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g) (h₂ : inrX φ j ≫ f = inrX φ j ≫ g) :
158+
f = g := by
159+
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
160+
rw [← cancel_epi (XIsoBiprod φ j i hij).inv]
161+
apply biprod.hom_ext'
162+
· simpa [inlX] using h₁
163+
· obtain rfl := c.next_eq' hij
164+
simpa [inrX, dif_pos hij] using h₂
165+
166+
lemma ext_from_X' (i : ι) (hi : ¬ c.Rel i (c.next i)) {A : C} {f g : X φ i ⟶ A}
167+
(h : inrX φ i ≫ f = inrX φ i ≫ g) : f = g := by
168+
rw [← cancel_epi (XIso φ i hi).inv]
169+
simpa only [inrX, dif_neg hi] using h
170+
171+
@[reassoc]
172+
lemma d_fstX (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) :
173+
d φ i j ≫ fstX φ j k hjk = -fstX φ i j hij ≫ F.d j k := by
174+
obtain rfl := c.next_eq' hjk
175+
simp [d, dif_pos hij, dif_pos hjk]
176+
177+
@[reassoc]
178+
lemma d_sndX (i j : ι) (hij : c.Rel i j) :
179+
d φ i j ≫ sndX φ j = fstX φ i j hij ≫ φ.f j + sndX φ i ≫ G.d i j := by
180+
dsimp [d]
181+
split_ifs with hij <;> simp
182+
183+
@[reassoc]
184+
lemma inlX_d (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) :
185+
inlX φ j i hij ≫ d φ i j = -F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j := by
186+
apply ext_to_X φ j k hjk
187+
· dsimp
188+
simp [d_fstX φ _ _ _ hij hjk]
189+
· simp [d_sndX φ _ _ hij]
190+
191+
@[reassoc]
192+
lemma inlX_d' (i j : ι) (hij : c.Rel i j) (hj : ¬ c.Rel j (c.next j)):
193+
inlX φ j i hij ≫ d φ i j = φ.f j ≫ inrX φ j := by
194+
apply ext_to_X' _ _ hj
195+
simp [d_sndX φ i j hij]
196+
197+
lemma shape (i j : ι) (hij : ¬ c.Rel i j) :
198+
d φ i j = 0 :=
199+
dif_neg hij
200+
201+
@[reassoc (attr := simp)]
202+
lemma inrX_d (i j : ι) :
203+
inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j := by
204+
by_cases hij : c.Rel i j
205+
· by_cases hj : c.Rel j (c.next j)
206+
· apply ext_to_X _ _ _ hj
207+
· simp [d_fstX φ _ _ _ hij]
208+
· simp [d_sndX φ _ _ hij]
209+
· apply ext_to_X' _ _ hj
210+
simp [d_sndX φ _ _ hij]
211+
· rw [shape φ _ _ hij, G.shape _ _ hij, zero_comp, comp_zero]
212+
213+
end homotopyCofiber
214+
215+
/-- The homotopy cofiber of a morphism of homological complexes,
216+
also known as the mapping cone. -/
217+
@[simps]
218+
noncomputable def homotopyCofiber : HomologicalComplex C c where
219+
X i := homotopyCofiber.X φ i
220+
d i j := homotopyCofiber.d φ i j
221+
shape i j hij := homotopyCofiber.shape φ i j hij
222+
d_comp_d' i j k hij hjk := by
223+
apply homotopyCofiber.ext_from_X φ j i hij
224+
· dsimp
225+
simp only [comp_zero, homotopyCofiber.inlX_d_assoc φ i j k hij hjk,
226+
add_comp, assoc, homotopyCofiber.inrX_d, Hom.comm_assoc, neg_comp]
227+
by_cases hk : c.Rel k (c.next k)
228+
· simp [homotopyCofiber.inlX_d φ j k _ hjk hk]
229+
· simp [homotopyCofiber.inlX_d' φ j k hjk hk]
230+
· simp
231+
232+
end HomologicalComplex

0 commit comments

Comments
 (0)