IndisputableMonolith.Foundation.SingularPrism
IndisputableMonolith/Foundation/SingularPrism.lean · 955 lines · 49 declarations
show as:
view math explainer →
1/-
2Homotopy invariance of singular homology: the prism operator.
3
4This file works toward the theorem that homotopic maps `f g : X ⟶ Y` of
5topological spaces induce the same map on singular homology (with `ℤ`
6coefficients), via the classical prism operator (Hatcher, Theorem 2.10).
7
8## Contents (staged; see the frontier note at the end of the file)
9
10* Stage 1: the prism decomposition maps `prism i : Δ^{n+1} → Δⁿ × I`
11 (affine maps onto the simplices of the standard triangulation of the
12 prism `Δⁿ × I`), as explicit continuous maps.
13* Stage 2: the face identities between the `prism i` and the topological
14 face inclusions `face j : Δⁿ → Δ^{n+1}` (the combinatorial heart of the
15 prism argument): top, bottom, cancellation of adjacent prisms, and the
16 two commutation identities with lower-dimensional faces.
17
18The model: `Δⁿ` is `stdSimplex ℝ (Fin (n+1))` (as used by
19`SimplexCategory.toTop` and hence by `TopCat.toSSet` and
20`AlgebraicTopology.singularHomologyFunctor`), and `I` is `unitInterval`.
21The vertices of the prism `Δⁿ × I` are `vⱼ = (eⱼ, 0)` and `wⱼ = (eⱼ, 1)`;
22`prism i` is the affine map `Δ^{n+1} → Δⁿ × I` sending the vertices
23`e₀, …, eₙ₊₁` of `Δ^{n+1}` to `v₀, …, vᵢ, wᵢ, …, wₙ`. Concretely, on
24barycentric coordinates the first component is induced by the vertex map
25`Fin.predAbove i` (which collapses `i, i+1` to `i`) and the second
26component is the sum of the coordinates strictly above `i`.
27-/
28import Mathlib.AlgebraicTopology.SingularHomology.Basic
29import Mathlib.Algebra.Category.ModuleCat.Colimits
30import Mathlib.Algebra.Category.ModuleCat.Abelian
31import Mathlib.Topology.Homotopy.Basic
32import Mathlib.Topology.Homotopy.Equiv
33
34namespace IndisputableMonolith
35namespace Foundation
36namespace SingularPrism
37
38open scoped unitInterval
39open CategoryTheory Limits AlgebraicTopology Simplicial Opposite
40
41/-! ## `Fin` coordinate arithmetic for `succAbove` / `predAbove` -/
42
43lemma coe_succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) :
44 ((p.succAbove i : Fin (n + 1)) : ℕ) =
45 if (i : ℕ) < (p : ℕ) then (i : ℕ) else (i : ℕ) + 1 := by
46 by_cases h : (i : ℕ) < (p : ℕ)
47 · rw [Fin.succAbove_of_castSucc_lt _ _ (by simpa [Fin.lt_def] using h)]
48 simp [h]
49 · rw [Fin.succAbove_of_le_castSucc _ _ (by simpa [Fin.le_def] using not_lt.mp h)]
50 simp [h]
51
52lemma coe_predAbove {n : ℕ} (p : Fin n) (i : Fin (n + 1)) :
53 ((p.predAbove i : Fin n) : ℕ) =
54 if (p : ℕ) < (i : ℕ) then (i : ℕ) - 1 else (i : ℕ) := by
55 by_cases h : (p : ℕ) < (i : ℕ)
56 · rw [Fin.predAbove_of_castSucc_lt _ _ (by simpa [Fin.lt_def] using h)]
57 simp [h]
58 · rw [Fin.predAbove_of_le_castSucc _ _ (by simpa [Fin.le_def] using not_lt.mp h)]
59 simp [h]
60
61/-! ## Stage 1: the prism decomposition maps -/
62
63variable {n : ℕ}
64
65/-- The second coordinate of the `i`-th prism map: the sum of the barycentric
66coordinates strictly above `i`. -/
67def prismSndFun (i : Fin (n + 1)) (x : stdSimplex ℝ (Fin (n + 2))) : ℝ :=
68 ∑ k with i.castSucc < k, x k
69
70lemma prismSndFun_nonneg (i : Fin (n + 1)) (x : stdSimplex ℝ (Fin (n + 2))) :
71 0 ≤ prismSndFun i x :=
72 Finset.sum_nonneg fun k _ => x.2.1 k
73
74lemma prismSndFun_le_one (i : Fin (n + 1)) (x : stdSimplex ℝ (Fin (n + 2))) :
75 prismSndFun i x ≤ 1 := by
76 calc prismSndFun i x ≤ ∑ k, x k :=
77 Finset.sum_le_sum_of_subset_of_nonneg (Finset.filter_subset _ _)
78 (fun k _ _ => x.2.1 k)
79 _ = 1 := x.2.2
80
81lemma prismSndFun_mem_unitInterval (i : Fin (n + 1)) (x : stdSimplex ℝ (Fin (n + 2))) :
82 prismSndFun i x ∈ I :=
83 Set.mem_Icc.mpr ⟨prismSndFun_nonneg i x, prismSndFun_le_one i x⟩
84
85lemma continuous_prismSndFun (i : Fin (n + 1)) :
86 Continuous (prismSndFun (n := n) i) :=
87 continuous_finset_sum _ fun k _ =>
88 (continuous_apply k).comp continuous_subtype_val
89
90/-- The `i`-th prism map `Δ^{n+1} → Δⁿ × I`: the affine map sending the
91vertices `e₀, …, eₙ₊₁` of `Δ^{n+1}` to `v₀, …, vᵢ, wᵢ, …, wₙ`, where
92`vⱼ = (eⱼ, 0)` and `wⱼ = (eⱼ, 1)` are the vertices of the prism. -/
93noncomputable def prism (i : Fin (n + 1)) :
94 C(stdSimplex ℝ (Fin (n + 2)), stdSimplex ℝ (Fin (n + 1)) × I) where
95 toFun x := (stdSimplex.map i.predAbove x,
96 ⟨prismSndFun i x, prismSndFun_mem_unitInterval i x⟩)
97 continuous_toFun :=
98 (stdSimplex.continuous_map _).prodMk
99 ((continuous_prismSndFun i).subtype_mk _)
100
101@[simp] lemma prism_apply_fst (i : Fin (n + 1)) (x : stdSimplex ℝ (Fin (n + 2))) :
102 (prism i x).1 = stdSimplex.map i.predAbove x := rfl
103
104@[simp] lemma prism_apply_snd (i : Fin (n + 1)) (x : stdSimplex ℝ (Fin (n + 2))) :
105 ((prism i x).2 : ℝ) = prismSndFun i x := rfl
106
107/-- The `j`-th topological face inclusion `Δⁿ → Δ^{n+1}`, induced by the
108vertex map `Fin.succAbove j` (skipping the vertex `j`). This is the
109topological realization of the simplicial face map `SimplexCategory.δ j`. -/
110noncomputable def face (j : Fin (n + 2)) :
111 C(stdSimplex ℝ (Fin (n + 1)), stdSimplex ℝ (Fin (n + 2))) :=
112 ⟨stdSimplex.map j.succAbove, stdSimplex.continuous_map _⟩
113
114@[simp] lemma face_apply (j : Fin (n + 2)) (x : stdSimplex ℝ (Fin (n + 1))) :
115 face j x = stdSimplex.map j.succAbove x := rfl
116
117/-! ## Stage 2: the face identities
118
119The composite of a prism map with a face inclusion is computed in the four
120classical cases (Hatcher, proof of Theorem 2.10):
121
122* `j = 0, i = 0`: the top of the prism, `x ↦ (x, 1)`;
123* `j = n+2, i = n+1` (last indices): the bottom of the prism, `x ↦ (x, 0)`;
124* `j = i+1` interior: consecutive prism maps agree on the shared face
125 (these are the cancelling terms in `∂P`);
126* `j ≤ i` or `j ≥ i+2`: the composite factors through a prism map in one
127 dimension lower, followed by a face inclusion of the prism (these match
128 the terms of `P∂`).
129-/
130
131/-- Composites of `stdSimplex.map` agree as soon as the underlying vertex
132maps agree pointwise. -/
133lemma map_map_eq_map_map {a b b' c : Type*}
134 [Fintype a] [Fintype b] [Fintype b'] [Fintype c]
135 (f : a → b) (g : b → c) (f' : a → b') (g' : b' → c)
136 (h : ∀ k, g (f k) = g' (f' k)) (x : stdSimplex ℝ a) :
137 stdSimplex.map g (stdSimplex.map f x) = stdSimplex.map g' (stdSimplex.map f' x) := by
138 rw [stdSimplex.map_comp_apply, stdSimplex.map_comp_apply,
139 show g ∘ f = g' ∘ f' from funext h]
140
141/-- Composite of `stdSimplex.map` with the identity vertex map. -/
142lemma map_map_eq_self {a b : Type*} [Fintype a] [Fintype b]
143 (f : a → b) (g : b → a) (h : ∀ k, g (f k) = k) (x : stdSimplex ℝ a) :
144 stdSimplex.map g (stdSimplex.map f x) = x := by
145 rw [stdSimplex.map_comp_apply, show g ∘ f = id from funext h,
146 stdSimplex.map_id_apply]
147
148/-- A filtered coordinate-sum of `stdSimplex.map f x` reindexes along `f`. -/
149lemma sum_filter_map_apply {a b : Type*} [Fintype a] [Fintype b] [DecidableEq b]
150 (f : a → b) (p : b → Prop) [DecidablePred p] (x : stdSimplex ℝ a) :
151 ∑ k with p k, stdSimplex.map f x k = ∑ m with p (f m), x m := by
152 classical
153 simp only [stdSimplex.map_coe, FunOnFinite.linearMap_apply_apply]
154 rw [Finset.sum_fiberwise_eq_sum_filter Finset.univ (Finset.univ.filter p) f (⇑x)]
155 exact Finset.sum_congr (by ext m; simp) fun _ _ => rfl
156
157lemma prismSndFun_map_succAbove (c : Fin (n + 1)) (j : Fin (n + 2))
158 (x : stdSimplex ℝ (Fin (n + 1))) :
159 prismSndFun c (stdSimplex.map j.succAbove x) =
160 ∑ m with c.castSucc < j.succAbove m, x m :=
161 sum_filter_map_apply j.succAbove (fun k => c.castSucc < k) x
162
163/-- Top of the prism: `prism 0 ∘ face 0 = (x ↦ (x, 1))`. -/
164theorem prism_comp_face_top :
165 (prism (0 : Fin (n + 1))).comp (face (0 : Fin (n + 2))) =
166 (ContinuousMap.id _).prodMk (ContinuousMap.const _ 1) := by
167 refine ContinuousMap.ext fun x => Prod.ext ?_ (Subtype.ext ?_)
168 · show stdSimplex.map (Fin.predAbove 0) (stdSimplex.map (Fin.succAbove 0) x) = x
169 refine map_map_eq_self _ _ (fun k => ?_) x
170 apply Fin.ext
171 simp only [coe_predAbove, coe_succAbove, Fin.val_zero]
172 split_ifs <;> omega
173 · show prismSndFun 0 (stdSimplex.map (Fin.succAbove 0) x) = 1
174 rw [prismSndFun_map_succAbove]
175 calc ∑ m with (0 : Fin (n + 1)).castSucc < (0 : Fin (n + 2)).succAbove m, x m
176 = ∑ m, x m := by
177 apply Finset.sum_congr _ fun _ _ => rfl
178 rw [Finset.filter_true_of_mem]
179 intro m _
180 simp only [Fin.lt_def, coe_succAbove, Fin.val_castSucc, Fin.val_zero]
181 split_ifs <;> omega
182 _ = 1 := x.2.2
183
184/-- Bottom of the prism: `prism (last) ∘ face (last) = (x ↦ (x, 0))`. -/
185theorem prism_comp_face_bot :
186 (prism (Fin.last n)).comp (face (Fin.last (n + 1))) =
187 (ContinuousMap.id _).prodMk (ContinuousMap.const _ 0) := by
188 refine ContinuousMap.ext fun x => Prod.ext ?_ (Subtype.ext ?_)
189 · show stdSimplex.map (Fin.predAbove (Fin.last n))
190 (stdSimplex.map (Fin.succAbove (Fin.last (n + 1))) x) = x
191 refine map_map_eq_self _ _ (fun k => ?_) x
192 apply Fin.ext
193 have hk := k.isLt
194 simp only [coe_predAbove, coe_succAbove, Fin.val_last]
195 split_ifs <;> omega
196 · show prismSndFun (Fin.last n) (stdSimplex.map (Fin.succAbove (Fin.last (n + 1))) x) = 0
197 rw [prismSndFun_map_succAbove]
198 apply Finset.sum_eq_zero
199 intro m hm
200 exfalso
201 rw [Finset.mem_filter] at hm
202 have hm' := hm.2
203 have hm2 := m.isLt
204 rw [Fin.lt_def] at hm'
205 revert hm'
206 simp only [coe_succAbove, Fin.val_castSucc, Fin.val_last]
207 split_ifs
208 all_goals omega
209
210/-- Adjacent prism maps agree on their shared face (the cancelling terms
211of `∂P`): `prism i ∘ face (i+1) = prism (i+1) ∘ face (i+1)`. -/
212theorem prism_comp_face_cancel (i : Fin (n + 1)) :
213 (prism i.castSucc).comp (face i.succ.castSucc) =
214 (prism i.succ).comp (face i.succ.castSucc) := by
215 refine ContinuousMap.ext fun x => Prod.ext ?_ (Subtype.ext ?_)
216 · show stdSimplex.map (Fin.predAbove i.castSucc)
217 (stdSimplex.map (Fin.succAbove i.succ.castSucc) x) =
218 stdSimplex.map (Fin.predAbove i.succ)
219 (stdSimplex.map (Fin.succAbove i.succ.castSucc) x)
220 refine map_map_eq_map_map _ _ _ _ (fun k => ?_) x
221 apply Fin.ext
222 have hk := k.isLt
223 simp only [coe_predAbove, coe_succAbove, Fin.val_castSucc, Fin.val_succ]
224 split_ifs <;> omega
225 · show prismSndFun i.castSucc (stdSimplex.map (Fin.succAbove i.succ.castSucc) x) =
226 prismSndFun i.succ (stdSimplex.map (Fin.succAbove i.succ.castSucc) x)
227 rw [prismSndFun_map_succAbove, prismSndFun_map_succAbove]
228 refine Finset.sum_congr (Finset.filter_congr fun m _ => ?_) fun _ _ => rfl
229 have hm := m.isLt
230 simp only [Fin.lt_def, coe_succAbove, Fin.val_castSucc, Fin.val_succ]
231 split_ifs <;> omega
232
233/-- Commutation with lower faces (`j ≤ i`): the composite of a prism map
234with a low face factors through the prism one dimension down. This matches
235the `(i, j)` terms of `∂P` with `j < i+1` against the terms of `P∂`. -/
236theorem prism_comp_face_of_le {i : Fin (n + 1)} {j : Fin (n + 2)}
237 (hij : j ≤ i.castSucc) :
238 (prism i.succ).comp (face j.castSucc) =
239 ((face j).prodMap (ContinuousMap.id I)).comp (prism i) := by
240 have hij' : (j : ℕ) ≤ (i : ℕ) := by simpa [Fin.le_def] using hij
241 refine ContinuousMap.ext fun x => Prod.ext ?_ (Subtype.ext ?_)
242 · show stdSimplex.map (Fin.predAbove i.succ)
243 (stdSimplex.map (Fin.succAbove j.castSucc) x) =
244 stdSimplex.map (Fin.succAbove j) (stdSimplex.map (Fin.predAbove i) x)
245 refine map_map_eq_map_map _ _ _ _ (fun k => ?_) x
246 apply Fin.ext
247 have hk := k.isLt
248 simp only [coe_predAbove, coe_succAbove, Fin.val_castSucc, Fin.val_succ]
249 split_ifs <;> omega
250 · show prismSndFun i.succ (stdSimplex.map (Fin.succAbove j.castSucc) x) =
251 prismSndFun i x
252 rw [prismSndFun_map_succAbove, prismSndFun]
253 refine Finset.sum_congr (Finset.filter_congr fun m _ => ?_) fun _ _ => rfl
254 have hm := m.isLt
255 simp only [Fin.lt_def, coe_succAbove, Fin.val_castSucc, Fin.val_succ]
256 split_ifs <;> omega
257
258/-- Commutation with high faces (`j > i`): the composite of a prism map
259with a high face factors through the prism one dimension down. This
260matches the `(i, j)` terms of `∂P` with `j > i+1` against the terms of
261`P∂`. -/
262theorem prism_comp_face_of_gt {i : Fin (n + 1)} {j : Fin (n + 2)}
263 (hij : i.castSucc < j) :
264 (prism i.castSucc).comp (face j.succ) =
265 ((face j).prodMap (ContinuousMap.id I)).comp (prism i) := by
266 have hij' : (i : ℕ) < (j : ℕ) := by simpa [Fin.lt_def] using hij
267 refine ContinuousMap.ext fun x => Prod.ext ?_ (Subtype.ext ?_)
268 · show stdSimplex.map (Fin.predAbove i.castSucc)
269 (stdSimplex.map (Fin.succAbove j.succ) x) =
270 stdSimplex.map (Fin.succAbove j) (stdSimplex.map (Fin.predAbove i) x)
271 refine map_map_eq_map_map _ _ _ _ (fun k => ?_) x
272 apply Fin.ext
273 have hk := k.isLt
274 simp only [coe_predAbove, coe_succAbove, Fin.val_castSucc, Fin.val_succ]
275 split_ifs <;> omega
276 · show prismSndFun i.castSucc (stdSimplex.map (Fin.succAbove j.succ) x) =
277 prismSndFun i x
278 rw [prismSndFun_map_succAbove, prismSndFun]
279 refine Finset.sum_congr (Finset.filter_congr fun m _ => ?_) fun _ _ => rfl
280 have hm := m.isLt
281 simp only [Fin.lt_def, coe_succAbove, Fin.val_castSucc, Fin.val_succ]
282 split_ifs <;> omega
283
284/-! ## Stage 3: the chain-level prism operator
285
286We now assemble the topological prism maps into a morphism of the singular
287chain groups. With `ℤ` coefficients, the singular chain group in degree `n`
288of a space `X` is the coproduct `∐_{σ} ℤ` indexed by the singular
289`n`-simplices of `X` (`Idx X n`); see `SSet.singularChainComplexFunctor`.
290-/
291
292/-- The type of singular `n`-simplices of `X` (the index set of the degree-`n`
293singular chain group). -/
294abbrev Idx (X : TopCat.{0}) (n : ℕ) : Type := (TopCat.toSSet.obj X).obj (op ⦋n⦌)
295
296/-- The degree-`n` singular chain group of `X` with `ℤ` coefficients:
297`∐_{σ ∈ Idx X n} ℤ`. -/
298noncomputable abbrev Cgrp (X : TopCat.{0}) (n : ℕ) : ModuleCat.{0} ℤ :=
299 ∐ fun _ : Idx X n => ModuleCat.of ℤ ℤ
300
301/-- The generator of the singular chain group attached to a singular
302simplex `a`. -/
303noncomputable abbrev gen (X : TopCat.{0}) (n : ℕ) (a : Idx X n) :
304 ModuleCat.of ℤ ℤ ⟶ Cgrp X n :=
305 Sigma.ι (fun _ : Idx X n => ModuleCat.of ℤ ℤ) a
306
307/-- Given a homotopy `H : I × X → Y`, a topological prism map
308`pr : Δ^{n+1} → Δⁿ × I`, and a singular `n`-simplex `σ : Δⁿ → X` of `X`, the
309associated singular `(n+1)`-simplex of `Y`: `t ↦ H(π₂(pr t), σ(π₁(pr t)))`. -/
310noncomputable def prismSimplex {X Y : TopCat.{0}} (H : C(I × X, Y)) (n : ℕ)
311 (pr : C(stdSimplex ℝ (Fin (n + 2)), stdSimplex ℝ (Fin (n + 1)) × I))
312 (s : Idx X n) : Idx Y (n + 1) :=
313 (Y.toSSetObjEquiv (op ⦋n + 1⦌)).symm
314 (H.comp (ContinuousMap.prodSwap.comp
315 (((X.toSSetObjEquiv (op ⦋n⦌) s).prodMap (ContinuousMap.id I)).comp pr)))
316
317/-- The prism operator on a generator: the signed sum
318`∑ᵢ (-1)ⁱ [prismSimplex i]` over the prism decomposition maps `prisms i`. -/
319noncomputable def Pgen {X Y : TopCat.{0}} (H : C(I × X, Y)) (n : ℕ)
320 (prisms : Fin (n + 1) →
321 C(stdSimplex ℝ (Fin (n + 2)), stdSimplex ℝ (Fin (n + 1)) × I))
322 (s : Idx X n) : ModuleCat.of ℤ ℤ ⟶ Cgrp Y (n + 1) :=
323 ∑ i : Fin (n + 1), (-1 : ℤ) ^ (i : ℕ) • gen Y (n + 1) (prismSimplex H n (prisms i) s)
324
325/-- The prism operator `P : C_n(X) → C_{n+1}(Y)`, extended from `Pgen` by the
326universal property of the coproduct. -/
327noncomputable def prismOp {X Y : TopCat.{0}} (H : C(I × X, Y)) (n : ℕ)
328 (prisms : Fin (n + 1) →
329 C(stdSimplex ℝ (Fin (n + 2)), stdSimplex ℝ (Fin (n + 1)) × I)) :
330 Cgrp X n ⟶ Cgrp Y (n + 1) :=
331 Sigma.desc (Pgen H n prisms)
332
333/-! ## Stage 4a: normal forms for the singular simplicial set
334
335The singular simplicial set `TopCat.toSSet.obj X` is the restricted Yoneda
336presheaf of `SimplexCategory.toTop`; through `TopCat.toSSetObjEquiv` its
337simplicial structure maps become precomposition with the topological face
338inclusions, and the functorial action of `TopCat.toSSet` becomes
339postcomposition.
340-/
341
342/-- Naturality of `TopCat.toSSetObjEquiv`: the simplicial face map `δ j` of
343the singular simplicial set is precomposition with the topological face
344inclusion `face j`. -/
345lemma toSSetObjEquiv_δ {X : TopCat.{0}} {n : ℕ} (j : Fin (n + 2)) (a : Idx X (n + 1)) :
346 X.toSSetObjEquiv (op ⦋n⦌) ((TopCat.toSSet.obj X).δ j a) =
347 (X.toSSetObjEquiv (op ⦋n + 1⦌) a).comp (face j) := by
348 ext x
349 rfl
350
351/-- Naturality of `TopCat.toSSetObjEquiv`: the functorial action of
352`TopCat.toSSet` on a continuous map `f` is postcomposition with `f`. -/
353lemma toSSetObjEquiv_map {X Y : TopCat.{0}} (f : X ⟶ Y) {n : ℕ} (a : Idx X n) :
354 Y.toSSetObjEquiv (op ⦋n⦌) ((TopCat.toSSet.map f).app (op ⦋n⦌) a) =
355 f.hom.comp (X.toSSetObjEquiv (op ⦋n⦌) a) := by
356 ext x
357 rfl
358
359/-! ## Stage 4b: generator normal forms for the singular chain complex -/
360
361/-- The singular chain complex of `X` with `ℤ` coefficients. -/
362noncomputable abbrev SC (X : TopCat.{0}) : ChainComplex (ModuleCat.{0} ℤ) ℕ :=
363 ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat.{0} ℤ)).obj
364 (ModuleCat.of ℤ ℤ)).obj X
365
366/-- The simplicial `ℤ`-module underlying the singular chain complex of `X`. -/
367noncomputable abbrev SOb (X : TopCat.{0}) : SimplicialObject (ModuleCat.{0} ℤ) :=
368 ((SimplicialObject.whiskering _ _).obj
369 (sigmaConst.obj (ModuleCat.of ℤ ℤ))).obj (TopCat.toSSet.obj X)
370
371lemma SC_eq (X : TopCat.{0}) : SC X = AlternatingFaceMapComplex.obj (SOb X) := rfl
372
373/-- The boundary out of degree `n+1` of the singular chain complex, typed on
374the coproduct presentation of the chain groups. -/
375noncomputable abbrev bnd (X : TopCat.{0}) (n : ℕ) : Cgrp X (n + 1) ⟶ Cgrp X n :=
376 (SC X).d (n + 1) n
377
378/-- The chain map induced by a continuous map, in degree `n`, typed on the
379coproduct presentation of the chain groups. -/
380noncomputable abbrev chainMap {X Y : TopCat.{0}} (f : X ⟶ Y) (n : ℕ) :
381 Cgrp X n ⟶ Cgrp Y n :=
382 (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat.{0} ℤ)).obj
383 (ModuleCat.of ℤ ℤ)).map f).f n
384
385/-- The boundary of a generator is the alternating sum of its faces. -/
386lemma gen_d (X : TopCat.{0}) (n : ℕ) (a : Idx X (n + 1)) :
387 gen X (n + 1) a ≫ bnd X n =
388 ∑ k : Fin (n + 2), (-1 : ℤ) ^ (k : ℕ) • gen X n ((TopCat.toSSet.obj X).δ k a) := by
389 show gen X (n + 1) a ≫ (AlternatingFaceMapComplex.obj (SOb X)).d (n + 1) n = _
390 rw [AlternatingFaceMapComplex.obj_d_eq, Preadditive.comp_sum]
391 refine Finset.sum_congr rfl fun k _ => ?_
392 rw [Preadditive.comp_zsmul]
393 congr 1
394 show gen X (n + 1) a ≫ Sigma.map' (f := fun _ : Idx X (n + 1) => ModuleCat.of ℤ ℤ)
395 (g := fun _ : Idx X n => ModuleCat.of ℤ ℤ)
396 ((TopCat.toSSet.obj X).δ k) (fun _ => 𝟙 _) = _
397 rw [Sigma.ι_comp_map', Category.id_comp]
398
399/-- The induced chain map sends a generator to the generator of the
400postcomposed simplex. -/
401lemma gen_map {X Y : TopCat.{0}} (f : X ⟶ Y) (n : ℕ) (a : Idx X n) :
402 gen X n a ≫ chainMap f n = gen Y n ((TopCat.toSSet.map f).app (op ⦋n⦌) a) := by
403 show gen X n a ≫ Sigma.map' (f := fun _ : Idx X n => ModuleCat.of ℤ ℤ)
404 (g := fun _ : Idx Y n => ModuleCat.of ℤ ℤ)
405 ((TopCat.toSSet.map f).app (op ⦋n⦌)) (fun _ => 𝟙 _) = _
406 rw [Sigma.ι_comp_map', Category.id_comp]
407
408/-- The prism operator sends a generator to the signed prism sum. -/
409lemma gen_prismOp {X Y : TopCat.{0}} (H : C(I × X, Y)) (n : ℕ)
410 (prisms : Fin (n + 1) →
411 C(stdSimplex ℝ (Fin (n + 2)), stdSimplex ℝ (Fin (n + 1)) × I))
412 (s : Idx X n) :
413 gen X n s ≫ prismOp H n prisms = Pgen H n prisms s :=
414 Sigma.ι_desc _ _
415
416/-! ## Stage 4c: the alternating double-sum cancellation (abstract form)
417
418The combinatorial heart of Hatcher's Theorem 2.10: given two doubly-indexed
419families related by the prism face identities (`hle`, `hgt` off the diagonal,
420`hcancel` on the two diagonals), the signed double sums collapse to the two
421end terms. Here `G i j` abstracts the `j`-th face of the `i`-th prism of a
422simplex (`∂P`), and `G' k i'` abstracts the `i'`-th prism of the `k`-th face
423(`P∂`).
424-/
425
426/-- Telescoping over `Fin`: if `S i.castSucc = D i.succ` then the sum of the
427differences `D i - S i` collapses to `D 0 - S last`. -/
428lemma sum_sub_telescope {M : Type*} [AddCommGroup M] :
429 ∀ (m : ℕ) (D S : Fin (m + 1) → M), (∀ i : Fin m, S i.castSucc = D i.succ) →
430 ∑ i, (D i - S i) = D 0 - S (Fin.last m)
431 | 0, D, S, _ => by simp
432 | m + 1, D, S, h => by
433 rw [Fin.sum_univ_succ,
434 sum_sub_telescope m (fun i => D i.succ) (fun i => S i.succ) (fun i => by
435 show S i.castSucc.succ = D i.succ.succ
436 rw [Fin.succ_castSucc]
437 exact h i.succ)]
438 have h0 : S 0 = D 1 := by simpa using h 0
439 have hlast : (Fin.last m).succ = Fin.last (m + 1) := rfl
440 rw [h0, hlast]
441 simp only [Fin.succ_zero_eq_one]
442 abel
443
444/-- The four-way partition of the `∂P` index set `Fin (n+2) × Fin (n+3)`:
445below the diagonal, the diagonal, the superdiagonal, above the
446superdiagonal. -/
447lemma sum_prod_partition {M : Type*} [AddCommGroup M] (n : ℕ)
448 (F : Fin (n + 2) × Fin (n + 3) → M) :
449 ∑ p, F p =
450 ((∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.2 : ℕ) < (p.1 : ℕ))}, F p) +
451 ∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.2 : ℕ) = (p.1 : ℕ))}, F p) +
452 ((∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.2 : ℕ) = (p.1 : ℕ) + 1)}, F p) +
453 ∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.1 : ℕ) + 1 < (p.2 : ℕ))}, F p) := by
454 classical
455 have h2 : (∑ p ∈ Finset.univ.filter (fun p : Fin (n + 2) × Fin (n + 3) =>
456 ¬ (p.2 : ℕ) < (p.1 : ℕ) ∧ ¬ (p.2 : ℕ) = (p.1 : ℕ)), F p) =
457 (∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.2 : ℕ) = (p.1 : ℕ) + 1)}, F p) +
458 ∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.1 : ℕ) + 1 < (p.2 : ℕ))}, F p := by
459 rw [← Finset.sum_filter_add_sum_filter_not
460 (Finset.univ.filter fun p : Fin (n + 2) × Fin (n + 3) =>
461 ¬ (p.2 : ℕ) < (p.1 : ℕ) ∧ ¬ (p.2 : ℕ) = (p.1 : ℕ))
462 (fun p => (p.2 : ℕ) = (p.1 : ℕ) + 1) F]
463 congr 1
464 · apply Finset.sum_congr _ fun _ _ => rfl
465 rw [Finset.filter_filter]
466 apply Finset.filter_congr
467 intro p _
468 omega
469 · apply Finset.sum_congr _ fun _ _ => rfl
470 rw [Finset.filter_filter]
471 apply Finset.filter_congr
472 intro p _
473 omega
474 have h1 : (∑ p ∈ Finset.univ.filter (fun p : Fin (n + 2) × Fin (n + 3) =>
475 ¬ (p.2 : ℕ) < (p.1 : ℕ)), F p) =
476 (∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.2 : ℕ) = (p.1 : ℕ))}, F p) +
477 ((∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.2 : ℕ) = (p.1 : ℕ) + 1)}, F p) +
478 ∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.1 : ℕ) + 1 < (p.2 : ℕ))}, F p) := by
479 rw [← Finset.sum_filter_add_sum_filter_not
480 (Finset.univ.filter fun p : Fin (n + 2) × Fin (n + 3) => ¬ (p.2 : ℕ) < (p.1 : ℕ))
481 (fun p => (p.2 : ℕ) = (p.1 : ℕ)) F]
482 congr 1
483 · apply Finset.sum_congr _ fun _ _ => rfl
484 rw [Finset.filter_filter]
485 apply Finset.filter_congr
486 intro p _
487 omega
488 · rw [← h2]
489 apply Finset.sum_congr _ fun _ _ => rfl
490 rw [Finset.filter_filter]
491 rw [← Finset.sum_filter_add_sum_filter_not Finset.univ
492 (fun p : Fin (n + 2) × Fin (n + 3) => (p.2 : ℕ) < (p.1 : ℕ)) F, h1]
493 abel
494
495/-- The two-way partition of the `P∂` index set `Fin (n+2) × Fin (n+1)`. -/
496lemma sum_prod_partition' {M : Type*} [AddCommGroup M] (n : ℕ)
497 (F : Fin (n + 2) × Fin (n + 1) → M) :
498 ∑ q, F q =
499 (∑ q ∈ {q : Fin (n + 2) × Fin (n + 1) | ((q.1 : ℕ) ≤ (q.2 : ℕ))}, F q) +
500 ∑ q ∈ {q : Fin (n + 2) × Fin (n + 1) | ((q.2 : ℕ) < (q.1 : ℕ))}, F q := by
501 classical
502 rw [← Finset.sum_filter_add_sum_filter_not Finset.univ
503 (fun q : Fin (n + 2) × Fin (n + 1) => (q.1 : ℕ) ≤ (q.2 : ℕ)) F]
504 congr 1
505 apply Finset.sum_congr _ fun _ _ => rfl
506 apply Finset.filter_congr
507 intro q _
508 omega
509
510/-- Hatcher's Theorem 2.10 alternating double-sum cancellation, abstractly:
511if `G` (the faces of the prisms, i.e. `∂P`) and `G'` (the prisms of the
512faces, i.e. `P∂`) satisfy the three prism face identities, the two signed
513double sums collapse to `G 0 0 - G last last` (i.e. `g♯ - f♯`). -/
514lemma prism_sum_cancellation {M : Type*} [AddCommGroup M] (n : ℕ)
515 (G : Fin (n + 2) → Fin (n + 3) → M) (G' : Fin (n + 2) → Fin (n + 1) → M)
516 (hle : ∀ (i : Fin (n + 1)) (j : Fin (n + 2)), (j : ℕ) ≤ (i : ℕ) →
517 G i.succ j.castSucc = G' j i)
518 (hgt : ∀ (i : Fin (n + 1)) (j : Fin (n + 2)), (i : ℕ) < (j : ℕ) →
519 G i.castSucc j.succ = G' j i)
520 (hcancel : ∀ i : Fin (n + 1),
521 G i.castSucc i.succ.castSucc = G i.succ i.succ.castSucc) :
522 ((∑ i : Fin (n + 2), ∑ j : Fin (n + 3), (-1 : ℤ) ^ ((i : ℕ) + (j : ℕ)) • G i j) +
523 ∑ k : Fin (n + 2), ∑ i' : Fin (n + 1), (-1 : ℤ) ^ ((k : ℕ) + (i' : ℕ)) • G' k i') =
524 G 0 0 - G (Fin.last (n + 1)) (Fin.last (n + 2)) := by
525 classical
526 have hB : (∑ i : Fin (n + 2), ∑ j : Fin (n + 3),
527 (-1 : ℤ) ^ ((i : ℕ) + (j : ℕ)) • G i j) =
528 ∑ p : Fin (n + 2) × Fin (n + 3), (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) • G p.1 p.2 := by
529 rw [← Finset.sum_product']
530 rfl
531 have hA : (∑ k : Fin (n + 2), ∑ i' : Fin (n + 1),
532 (-1 : ℤ) ^ ((k : ℕ) + (i' : ℕ)) • G' k i') =
533 ∑ q : Fin (n + 2) × Fin (n + 1), (-1 : ℤ) ^ ((q.1 : ℕ) + (q.2 : ℕ)) • G' q.1 q.2 := by
534 rw [← Finset.sum_product']
535 rfl
536 rw [hB, hA,
537 sum_prod_partition n (fun p => (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) • G p.1 p.2),
538 sum_prod_partition' n (fun q => (-1 : ℤ) ^ ((q.1 : ℕ) + (q.2 : ℕ)) • G' q.1 q.2)]
539 -- the below-diagonal `∂P` terms cancel the `k ≤ i'` half of `P∂`
540 have e1 : (∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.2 : ℕ) < (p.1 : ℕ))},
541 (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) • G p.1 p.2) =
542 -∑ q ∈ {q : Fin (n + 2) × Fin (n + 1) | ((q.1 : ℕ) ≤ (q.2 : ℕ))},
543 (-1 : ℤ) ^ ((q.1 : ℕ) + (q.2 : ℕ)) • G' q.1 q.2 := by
544 rw [← Finset.sum_neg_distrib]
545 refine Finset.sum_bij'
546 (i := fun p hp => ((⟨(p.2 : ℕ), by
547 simp only [Finset.mem_filter_univ] at hp; omega⟩ : Fin (n + 2)),
548 (⟨(p.1 : ℕ) - 1, by
549 simp only [Finset.mem_filter_univ] at hp; omega⟩ : Fin (n + 1))))
550 (j := fun q hq => (q.2.succ, q.1.castSucc)) ?_ ?_ ?_ ?_ ?_
551 · intro p hp
552 simp only [Finset.mem_filter_univ] at hp ⊢
553 omega
554 · intro q hq
555 simp only [Finset.mem_filter_univ] at hq ⊢
556 simp only [Fin.val_succ, Fin.val_castSucc]
557 omega
558 · intro p hp
559 simp only [Finset.mem_filter_univ] at hp
560 ext
561 · simp only [Fin.val_succ]; omega
562 · simp only [Fin.val_castSucc]
563 · intro q hq
564 simp only [Finset.mem_filter_univ] at hq
565 ext
566 · simp only [Fin.val_castSucc]
567 · simp only [Fin.val_succ]; omega
568 · intro p hp
569 simp only [Finset.mem_filter_univ] at hp
570 set k : Fin (n + 2) := ⟨(p.2 : ℕ), by omega⟩ with hk
571 set i' : Fin (n + 1) := ⟨(p.1 : ℕ) - 1, by omega⟩ with hi'
572 have hp1 : p.1 = i'.succ := by ext; simp only [Fin.val_succ, hi']; omega
573 have hp2 : p.2 = k.castSucc := by ext; simp only [Fin.val_castSucc, hk]
574 rw [hp1, hp2, hle i' k (by simp only [hk, hi']; omega)]
575 have hsign : ((i'.succ : ℕ) + (k.castSucc : ℕ)) = ((k : ℕ) + (i' : ℕ)) + 1 := by
576 simp only [Fin.val_succ, Fin.val_castSucc]; omega
577 rw [hsign, pow_succ, mul_neg_one, neg_smul]
578 -- the above-superdiagonal `∂P` terms cancel the `i' < k` half of `P∂`
579 have e2 : (∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.1 : ℕ) + 1 < (p.2 : ℕ))},
580 (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) • G p.1 p.2) =
581 -∑ q ∈ {q : Fin (n + 2) × Fin (n + 1) | ((q.2 : ℕ) < (q.1 : ℕ))},
582 (-1 : ℤ) ^ ((q.1 : ℕ) + (q.2 : ℕ)) • G' q.1 q.2 := by
583 rw [← Finset.sum_neg_distrib]
584 refine Finset.sum_bij'
585 (i := fun p hp => ((⟨(p.2 : ℕ) - 1, by
586 simp only [Finset.mem_filter_univ] at hp; omega⟩ : Fin (n + 2)),
587 (⟨(p.1 : ℕ), by
588 simp only [Finset.mem_filter_univ] at hp; omega⟩ : Fin (n + 1))))
589 (j := fun q hq => (q.2.castSucc, q.1.succ)) ?_ ?_ ?_ ?_ ?_
590 · intro p hp
591 simp only [Finset.mem_filter_univ] at hp ⊢
592 omega
593 · intro q hq
594 simp only [Finset.mem_filter_univ] at hq ⊢
595 simp only [Fin.val_succ, Fin.val_castSucc]
596 omega
597 · intro p hp
598 simp only [Finset.mem_filter_univ] at hp
599 ext
600 · simp only [Fin.val_castSucc]
601 · simp only [Fin.val_succ]; omega
602 · intro q hq
603 simp only [Finset.mem_filter_univ] at hq
604 ext
605 · simp only [Fin.val_succ]; omega
606 · simp only [Fin.val_castSucc]
607 · intro p hp
608 simp only [Finset.mem_filter_univ] at hp
609 set k : Fin (n + 2) := ⟨(p.2 : ℕ) - 1, by omega⟩ with hk
610 set i' : Fin (n + 1) := ⟨(p.1 : ℕ), by omega⟩ with hi'
611 have hp1 : p.1 = i'.castSucc := by ext; simp only [Fin.val_castSucc, hi']
612 have hp2 : p.2 = k.succ := by ext; simp only [Fin.val_succ, hk]; omega
613 rw [hp1, hp2, hgt i' k (by simp only [hk, hi']; omega)]
614 have hsign : ((i'.castSucc : ℕ) + (k.succ : ℕ)) = ((k : ℕ) + (i' : ℕ)) + 1 := by
615 simp only [Fin.val_succ, Fin.val_castSucc]; omega
616 rw [hsign, pow_succ, mul_neg_one, neg_smul]
617 -- the diagonal terms
618 have e3 : (∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.2 : ℕ) = (p.1 : ℕ))},
619 (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) • G p.1 p.2) =
620 ∑ i : Fin (n + 2), G i i.castSucc := by
621 refine Finset.sum_bij' (i := fun p _ => p.1)
622 (j := fun i _ => (i, i.castSucc)) ?_ ?_ ?_ ?_ ?_
623 · intro p _; exact Finset.mem_univ _
624 · intro i _
625 simp only [Finset.mem_filter_univ, Fin.val_castSucc]
626 · intro p hp
627 simp only [Finset.mem_filter_univ] at hp
628 ext
629 · rfl
630 · simp only [Fin.val_castSucc]; omega
631 · intro i _; rfl
632 · intro p hp
633 simp only [Finset.mem_filter_univ] at hp
634 have hp2 : p.2 = p.1.castSucc := by ext; simp only [Fin.val_castSucc]; omega
635 rw [hp2]
636 have : (-1 : ℤ) ^ ((p.1 : ℕ) + (p.1.castSucc : ℕ)) = 1 :=
637 Even.neg_one_pow (by simp only [Fin.val_castSucc]; exact ⟨(p.1 : ℕ), rfl⟩)
638 rw [this, one_smul]
639 -- the superdiagonal terms
640 have e4 : (∑ p ∈ {p : Fin (n + 2) × Fin (n + 3) | ((p.2 : ℕ) = (p.1 : ℕ) + 1)},
641 (-1 : ℤ) ^ ((p.1 : ℕ) + (p.2 : ℕ)) • G p.1 p.2) =
642 ∑ i : Fin (n + 2), -G i i.succ := by
643 refine Finset.sum_bij' (i := fun p _ => p.1)
644 (j := fun i _ => (i, i.succ)) ?_ ?_ ?_ ?_ ?_
645 · intro p _; exact Finset.mem_univ _
646 · intro i _
647 simp only [Finset.mem_filter_univ, Fin.val_succ]
648 · intro p hp
649 simp only [Finset.mem_filter_univ] at hp
650 ext
651 · rfl
652 · simp only [Fin.val_succ]; omega
653 · intro i _; rfl
654 · intro p hp
655 simp only [Finset.mem_filter_univ] at hp
656 have hp2 : p.2 = p.1.succ := by ext; simp only [Fin.val_succ]; omega
657 rw [hp2]
658 have : (-1 : ℤ) ^ ((p.1 : ℕ) + (p.1.succ : ℕ)) = -1 :=
659 Odd.neg_one_pow (by simp only [Fin.val_succ]; exact ⟨(p.1 : ℕ), by omega⟩)
660 rw [this, neg_one_smul]
661 -- the telescope
662 have e5 : (∑ i : Fin (n + 2), G i i.castSucc) + (∑ i : Fin (n + 2), -G i i.succ) =
663 G 0 0 - G (Fin.last (n + 1)) (Fin.last (n + 2)) := by
664 rw [← Finset.sum_add_distrib]
665 have := sum_sub_telescope (n + 1) (fun i : Fin (n + 2) => G i i.castSucc)
666 (fun i : Fin (n + 2) => G i i.succ) (fun i => by
667 show G i.castSucc i.castSucc.succ = G i.succ i.succ.castSucc
668 rw [Fin.succ_castSucc]
669 exact hcancel i)
670 simp only [sub_eq_add_neg] at this
671 rw [this, show ((Fin.last (n + 1)).succ : Fin (n + 3)) = Fin.last (n + 2) from rfl]
672 simp only [Fin.castSucc_zero, sub_eq_add_neg]
673 rw [e1, e2, e3, e4, ← e5]
674 abel
675
676/-! ## Stage 4d: transporting the face identities to singular simplices -/
677
678section FaceTransport
679
680variable {X Y : TopCat.{0}}
681
682/-- A face identity between prism maps transports to the corresponding
683identity of singular simplices: if `pr ∘ face j = (face j' × id) ∘ pr'`,
684then the `j`-th face of the prism simplex on `s` is the prism simplex of
685the `j'`-th face of `s`. -/
686lemma δ_prismSimplex_of_face (H : C(I × X, Y)) {n : ℕ}
687 (pr : C(stdSimplex ℝ (Fin (n + 3)), stdSimplex ℝ (Fin (n + 2)) × I))
688 (pr' : C(stdSimplex ℝ (Fin (n + 2)), stdSimplex ℝ (Fin (n + 1)) × I))
689 {j : Fin (n + 3)} {j' : Fin (n + 2)}
690 (hface : pr.comp (face j) = ((face j').prodMap (ContinuousMap.id I)).comp pr')
691 (s : Idx X (n + 1)) :
692 (TopCat.toSSet.obj Y).δ j (prismSimplex H (n + 1) pr s) =
693 prismSimplex H n pr' ((TopCat.toSSet.obj X).δ j' s) := by
694 apply (Y.toSSetObjEquiv (op ⦋n + 1⦌)).injective
695 rw [toSSetObjEquiv_δ, prismSimplex, Equiv.apply_symm_apply, prismSimplex,
696 Equiv.apply_symm_apply, toSSetObjEquiv_δ]
697 ext t
698 have h := ContinuousMap.congr_fun hface t
699 simp only [ContinuousMap.comp_apply] at h ⊢
700 exact (congrArg (fun z => H (ContinuousMap.prodSwap
701 (((X.toSSetObjEquiv (op ⦋n + 1⦌) s).prodMap (ContinuousMap.id I)) z))) h).trans rfl
702
703/-- Two prism maps agreeing on a face give equal faces of the prism
704simplices (the cancelling pairs of `∂P`). -/
705lemma δ_prismSimplex_congr (H : C(I × X, Y)) {n : ℕ}
706 (pr pr' : C(stdSimplex ℝ (Fin (n + 2)), stdSimplex ℝ (Fin (n + 1)) × I))
707 {j : Fin (n + 2)} (hface : pr.comp (face j) = pr'.comp (face j)) (s : Idx X n) :
708 (TopCat.toSSet.obj Y).δ j (prismSimplex H n pr s) =
709 (TopCat.toSSet.obj Y).δ j (prismSimplex H n pr' s) := by
710 apply (Y.toSSetObjEquiv (op ⦋n⦌)).injective
711 rw [toSSetObjEquiv_δ, toSSetObjEquiv_δ, prismSimplex, Equiv.apply_symm_apply,
712 prismSimplex, Equiv.apply_symm_apply]
713 ext t
714 have h := ContinuousMap.congr_fun hface t
715 simp only [ContinuousMap.comp_apply] at h ⊢
716 exact congrArg (fun z => H (ContinuousMap.prodSwap
717 (((X.toSSetObjEquiv (op ⦋n⦌) s).prodMap (ContinuousMap.id I)) z))) h
718
719/-- The `0`-th face of the `0`-th prism simplex is the pushforward of the
720simplex along the end `F₁` of the homotopy (the top of the prism). -/
721lemma δ_prismSimplex_top {F₀ F₁ : X ⟶ Y} (Ho : ContinuousMap.Homotopy F₀.hom F₁.hom)
722 (n : ℕ) (s : Idx X n) :
723 (TopCat.toSSet.obj Y).δ 0 (prismSimplex Ho.toContinuousMap n (prism 0) s) =
724 (TopCat.toSSet.map F₁).app (op ⦋n⦌) s := by
725 apply (Y.toSSetObjEquiv (op ⦋n⦌)).injective
726 rw [toSSetObjEquiv_δ, prismSimplex, Equiv.apply_symm_apply, toSSetObjEquiv_map]
727 ext t
728 have h := ContinuousMap.congr_fun (prism_comp_face_top (n := n)) t
729 simp only [ContinuousMap.comp_apply] at h ⊢
730 exact (congrArg (fun z => Ho.toContinuousMap (ContinuousMap.prodSwap
731 (((X.toSSetObjEquiv (op ⦋n⦌) s).prodMap (ContinuousMap.id I)) z))) h).trans
732 (Ho.apply_one _)
733
734/-- The last face of the last prism simplex is the pushforward of the
735simplex along the start `F₀` of the homotopy (the bottom of the prism). -/
736lemma δ_prismSimplex_bot {F₀ F₁ : X ⟶ Y} (Ho : ContinuousMap.Homotopy F₀.hom F₁.hom)
737 (n : ℕ) (s : Idx X n) :
738 (TopCat.toSSet.obj Y).δ (Fin.last (n + 1))
739 (prismSimplex Ho.toContinuousMap n (prism (Fin.last n)) s) =
740 (TopCat.toSSet.map F₀).app (op ⦋n⦌) s := by
741 apply (Y.toSSetObjEquiv (op ⦋n⦌)).injective
742 rw [toSSetObjEquiv_δ, prismSimplex, Equiv.apply_symm_apply, toSSetObjEquiv_map]
743 ext t
744 have h := ContinuousMap.congr_fun (prism_comp_face_bot (n := n)) t
745 simp only [ContinuousMap.comp_apply] at h ⊢
746 exact (congrArg (fun z => Ho.toContinuousMap (ContinuousMap.prodSwap
747 (((X.toSSetObjEquiv (op ⦋n⦌) s).prodMap (ContinuousMap.id I)) z))) h).trans
748 (Ho.apply_zero _)
749
750end FaceTransport
751
752/-! ## Stage 4e: the chain homotopy identity `∂P + P∂ = g♯ − f♯` -/
753
754section ChainHomotopyIdentity
755
756variable {X Y : TopCat.{0}} {F₀ F₁ : X ⟶ Y}
757
758/-- The chain homotopy identity in positive degrees:
759`∂ ∘ P + P ∘ ∂ = (F₁)♯ − (F₀)♯` on the degree-`(n+1)` chain group. -/
760lemma prism_chain_homotopy_succ (Ho : ContinuousMap.Homotopy F₀.hom F₁.hom) (n : ℕ) :
761 bnd X n ≫ prismOp Ho.toContinuousMap n prism +
762 prismOp Ho.toContinuousMap (n + 1) prism ≫ bnd Y (n + 1) =
763 chainMap F₁ (n + 1) - chainMap F₀ (n + 1) := by
764 apply Sigma.hom_ext
765 intro s
766 have hL1 : gen X (n + 1) s ≫ (bnd X n ≫ prismOp Ho.toContinuousMap n prism) =
767 ∑ k : Fin (n + 2), ∑ i' : Fin (n + 1), (-1 : ℤ) ^ ((k : ℕ) + (i' : ℕ)) •
768 gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
769 ((TopCat.toSSet.obj X).δ k s)) := by
770 rw [← Category.assoc, gen_d, Preadditive.sum_comp]
771 refine Finset.sum_congr rfl fun k _ => ?_
772 rw [Preadditive.zsmul_comp, gen_prismOp, Pgen, Finset.smul_sum]
773 refine Finset.sum_congr rfl fun i' _ => ?_
774 rw [smul_smul, ← pow_add]
775 have hL2 : gen X (n + 1) s ≫ (prismOp Ho.toContinuousMap (n + 1) prism ≫ bnd Y (n + 1)) =
776 ∑ i : Fin (n + 2), ∑ j : Fin (n + 3), (-1 : ℤ) ^ ((i : ℕ) + (j : ℕ)) •
777 gen Y (n + 1) ((TopCat.toSSet.obj Y).δ j
778 (prismSimplex Ho.toContinuousMap (n + 1) (prism i) s)) := by
779 rw [← Category.assoc, gen_prismOp, Pgen, Preadditive.sum_comp]
780 refine Finset.sum_congr rfl fun i _ => ?_
781 rw [Preadditive.zsmul_comp, gen_d, Finset.smul_sum]
782 refine Finset.sum_congr rfl fun j _ => ?_
783 rw [smul_smul, ← pow_add]
784 rw [Preadditive.comp_add, hL1, hL2, Preadditive.comp_sub, gen_map, gen_map,
785 add_comm (∑ k : Fin (n + 2), ∑ i' : Fin (n + 1), (-1 : ℤ) ^ ((k : ℕ) + (i' : ℕ)) •
786 gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
787 ((TopCat.toSSet.obj X).δ k s)))]
788 refine Eq.trans (prism_sum_cancellation n
789 (fun i j => gen Y (n + 1) ((TopCat.toSSet.obj Y).δ j
790 (prismSimplex Ho.toContinuousMap (n + 1) (prism i) s)))
791 (fun k i' => gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
792 ((TopCat.toSSet.obj X).δ k s)))
793 (fun i j hij => congrArg (gen Y (n + 1)) (δ_prismSimplex_of_face
794 Ho.toContinuousMap (prism i.succ) (prism i)
795 (prism_comp_face_of_le (Fin.le_def.mpr (by simpa using hij))) s))
796 (fun i j hij => congrArg (gen Y (n + 1)) (δ_prismSimplex_of_face
797 Ho.toContinuousMap (prism i.castSucc) (prism i)
798 (prism_comp_face_of_gt (Fin.lt_def.mpr (by simpa using hij))) s))
799 (fun i => congrArg (gen Y (n + 1)) (δ_prismSimplex_congr
800 Ho.toContinuousMap (prism i.castSucc) (prism i.succ)
801 (prism_comp_face_cancel i) s))) ?_
802 congr 1
803 · exact congrArg (gen Y (n + 1)) (δ_prismSimplex_top Ho (n + 1) s)
804 · exact congrArg (gen Y (n + 1)) (δ_prismSimplex_bot Ho (n + 1) s)
805
806/-- The chain homotopy identity in degree `0`:
807`∂ ∘ P = (F₁)♯ − (F₀)♯` on the degree-`0` chain group. -/
808lemma prism_chain_homotopy_zero (Ho : ContinuousMap.Homotopy F₀.hom F₁.hom) :
809 prismOp Ho.toContinuousMap 0 prism ≫ bnd Y 0 = chainMap F₁ 0 - chainMap F₀ 0 := by
810 apply Sigma.hom_ext
811 intro s
812 rw [← Category.assoc, gen_prismOp, Pgen, Fin.sum_univ_one, Preadditive.comp_sub,
813 gen_map, gen_map]
814 simp only [Fin.val_zero, pow_zero, one_smul]
815 rw [gen_d, Fin.sum_univ_two]
816 simp only [Fin.val_zero, Fin.val_one, pow_zero, pow_one, one_smul, neg_smul]
817 rw [congrArg (gen Y 0) (δ_prismSimplex_top Ho 0 s)]
818 rw [congrArg (gen Y 0) (show (TopCat.toSSet.obj Y).δ (1 : Fin 2)
819 (prismSimplex Ho.toContinuousMap 0 (prism (0 : Fin 1)) s) =
820 (TopCat.toSSet.map F₀).app (op ⦋0⦌) s from δ_prismSimplex_bot Ho 0 s)]
821 abel
822
823end ChainHomotopyIdentity
824
825/-! ## Stage 5: packaging and homotopy invariance of singular homology -/
826
827section Packaging
828
829variable {X Y : TopCat.{0}}
830
831/-- The singular chain map induced by a continuous map. -/
832noncomputable abbrev sChainMap (f : X ⟶ Y) : SC X ⟶ SC Y :=
833 ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat.{0} ℤ)).obj
834 (ModuleCat.of ℤ ℤ)).map f
835
836/-- A homotopy of continuous maps induces a chain homotopy of the induced
837maps of singular chain complexes, via the prism operator. -/
838noncomputable def prismHomotopy {F₀ F₁ : X ⟶ Y}
839 (Ho : ContinuousMap.Homotopy F₀.hom F₁.hom) :
840 Homotopy (sChainMap F₀) (sChainMap F₁) where
841 hom i j :=
842 if h : i + 1 = j then
843 (-prismOp Ho.toContinuousMap i prism) ≫ eqToHom (by subst h; rfl)
844 else 0
845 zero i j hij := by
846 rw [dif_neg]
847 intro h
848 exact hij (by simpa using h)
849 comm i := by
850 match i with
851 | 0 =>
852 rw [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex]
853 rw [dif_pos rfl, eqToHom_refl, Category.comp_id, Preadditive.neg_comp]
854 show chainMap F₀ 0 =
855 0 + -prismOp Ho.toContinuousMap 0 prism ≫ bnd Y 0 + chainMap F₁ 0
856 have h0 := prism_chain_homotopy_zero Ho
857 rw [eq_sub_iff_add_eq] at h0
858 rw [← h0]
859 abel
860 | n + 1 =>
861 rw [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex]
862 rw [dif_pos rfl, dif_pos rfl, eqToHom_refl, eqToHom_refl, Category.comp_id,
863 Category.comp_id, Preadditive.neg_comp, Preadditive.comp_neg]
864 show chainMap F₀ (n + 1) =
865 -bnd X n ≫ prismOp Ho.toContinuousMap n prism +
866 -prismOp Ho.toContinuousMap (n + 1) prism ≫ bnd Y (n + 1) +
867 chainMap F₁ (n + 1)
868 have h0 := prism_chain_homotopy_succ Ho n
869 rw [eq_sub_iff_add_eq] at h0
870 rw [← h0]
871 abel
872
873/-- **Homotopy invariance of singular homology**: homotopic continuous maps
874induce the same map on singular homology with `ℤ` coefficients
875(Hatcher, Theorem 2.10). -/
876theorem homotopic_maps_induce_same_homology
877 {f g : X ⟶ Y}
878 (h : ContinuousMap.Homotopy f.hom g.hom) (n : ℕ) :
879 ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj
880 (ModuleCat.of ℤ ℤ)).map f =
881 ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj
882 (ModuleCat.of ℤ ℤ)).map g :=
883 (prismHomotopy h).homologyMap_eq n
884
885/-- A homotopy equivalence of spaces induces a homotopy equivalence of
886singular chain complexes. -/
887noncomputable def chainHomotopyEquiv (h : ContinuousMap.HomotopyEquiv X Y) :
888 HomotopyEquiv (SC X) (SC Y) where
889 hom := sChainMap (TopCat.ofHom h.toFun)
890 inv := sChainMap (TopCat.ofHom h.invFun)
891 homotopyHomInvId :=
892 (Homotopy.ofEq ((CategoryTheory.Functor.map_comp _ _ _).symm)).trans
893 ((prismHomotopy (F₀ := TopCat.ofHom h.toFun ≫ TopCat.ofHom h.invFun)
894 (F₁ := 𝟙 X) h.left_inv.some).trans
895 (Homotopy.ofEq (CategoryTheory.Functor.map_id _ _)))
896 homotopyInvHomId :=
897 (Homotopy.ofEq ((CategoryTheory.Functor.map_comp _ _ _).symm)).trans
898 ((prismHomotopy (F₀ := TopCat.ofHom h.invFun ≫ TopCat.ofHom h.toFun)
899 (F₁ := 𝟙 Y) h.right_inv.some).trans
900 (Homotopy.ofEq (CategoryTheory.Functor.map_id _ _)))
901
902/-- A homotopy equivalence of spaces induces an isomorphism on singular
903homology with `ℤ` coefficients. -/
904noncomputable def homotopyEquiv_homology_iso
905 (h : ContinuousMap.HomotopyEquiv X Y) (n : ℕ) :
906 ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj
907 (ModuleCat.of ℤ ℤ)).obj X ≅
908 ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj
909 (ModuleCat.of ℤ ℤ)).obj Y :=
910 (chainHomotopyEquiv h).toHomologyIso n
911
912/-- The map on singular homology induced by (the forward map of) a homotopy
913equivalence is an isomorphism. -/
914theorem isIso_homology_map_of_homotopyEquiv
915 (h : ContinuousMap.HomotopyEquiv X Y) (n : ℕ) :
916 IsIso (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj
917 (ModuleCat.of ℤ ℤ)).map (TopCat.ofHom h.toFun)) :=
918 inferInstanceAs (IsIso ((homotopyEquiv_homology_iso h n).hom))
919
920end Packaging
921
922/-! ### Frontier note: CLOSED (all stages complete)
923
924All five stages are complete and axiom-clean (only `propext`, `Classical.choice`,
925`Quot.sound`); the module builds green with 0 `sorry`.
926
927* Stages 1–3: the topological prism maps (`prism`), the five face identities
928 (`prism_comp_face_top`, `prism_comp_face_bot`, `prism_comp_face_cancel`,
929 `prism_comp_face_of_le`, `prism_comp_face_of_gt`), and the chain-level
930 prism operator (`prismOp`).
931* Stage 4: generator normal forms (`gen_d`, `gen_map`, `gen_prismOp`), the
932 abstract alternating double-sum cancellation (`prism_sum_cancellation`,
933 built from `sum_sub_telescope`, `sum_prod_partition`,
934 `sum_prod_partition'`), the transported face identities
935 (`δ_prismSimplex_of_face`, `δ_prismSimplex_congr`, `δ_prismSimplex_top`,
936 `δ_prismSimplex_bot`), and the chain homotopy identity
937 `∂ ∘ P + P ∘ ∂ = (F₁)♯ − (F₀)♯` in every degree
938 (`prism_chain_homotopy_succ`, `prism_chain_homotopy_zero`).
939* Stage 5: `prismHomotopy : Homotopy (sChainMap F₀) (sChainMap F₁)`,
940 the main theorem `homotopic_maps_induce_same_homology` (homotopy
941 invariance of Mathlib singular homology with `ℤ` coefficients,
942 Hatcher Theorem 2.10), plus the homotopy-equivalence corollaries
943 `chainHomotopyEquiv`, `homotopyEquiv_homology_iso`, and
944 `isIso_homology_map_of_homotopyEquiv`.
945
946Nothing remains on this frontier. Possible follow-ups (new scope, not
947required here): coefficients in an arbitrary `R`-module (the whole argument
948is coefficient-independent; only the `ModuleCat ℤ` instances would change),
949and upstreaming to Mathlib.
950-/
951
952end SingularPrism
953end Foundation
954end IndisputableMonolith
955