IndisputableMonolith.Foundation.SingularSphere
IndisputableMonolith/Foundation/SingularSphere.lean · 746 lines · 55 declarations
show as:
view math explainer →
1/-
2Sphere homology `H_*(Sⁿ; ℤ)` by Mayer-Vietoris induction.
3
4Layer 5 of the excision spine (layer 1: `SingularPrism`, homotopy invariance;
5layer 2: `SingularPair`, the LES of a pair; layer 3: `SingularSubdivision`,
6barycentric subdivision; layer 4: `SingularMayerVietoris`, the MV long exact
7sequence).
8
9## Contents (staged)
10
11* Stage A/B: homology of points and contractible spaces. Mathlib already
12 computes the singular homology of totally disconnected spaces
13 (`isZero_singularHomologyFunctor_of_totallyDisconnectedSpace`), which
14 covers both the one-point space and `S⁰`; combining with layer 1's
15 homotopy invariance gives `IsZero (H_m X)` for contractible `X`, `m ≠ 0`
16 (`isZero_homology_of_contractible`). For `H₀` we build the augmentation
17 apparatus: the class of a point (`ptH`), the augmentation against a
18 clopen set (`augH`), their pairing (`ptH_augH`), homotopy invariance of
19 the point class (`ptH_eq_of_joined`), and the computation
20 `IsIso (augH X univ)` for path-connected `X`
21 (`isIso_augH_of_pathConnected`), via layer 4's concrete homology-map
22 criterion.
23* Stage A/B exports: `h0_iso_int` (`H₀(X) ≅ ℤ`, path-connected `X`),
24 `h0_pt_iso_int`, `hn_pt_isZero`, `h0_contractible_iso_int`.
25* Stage C (abstract half, DONE): the Mayer-Vietoris consequences over
26 layer 4, for any open cover `U ∪ V = univ`:
27 - `isIso_mvδ` / `isIso_mvδ_of_contractible`: the suspension step,
28 `∂ : H_{n+2}(X) ≅ H_{n+1}(U ∩ V)` when `U, V` have vanishing homology
29 there (e.g. contractible);
30 - `isZero_of_isZero_inter`: vanishing transported across `∂`;
31 - `mono_mvPair_zero`: the degree-0 pair map is mono when `U ∩ V` is
32 path connected (split by the augmentation);
33 - `isZero_h1` / `isZero_h1_of_contractible`: `H₁(X) = 0` when `U, V`
34 kill `H₁` and `U ∩ V` is path connected.
35
36## FRONTIER (for the next worker; everything above builds green, 0 sorry)
37
38Stage C (geometric half) and Stage D remain. Recommended decomposition:
39
401. Sphere model: `Metric.sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1` as
41 `TopCat.of`. `U := {x | x ≠ south}`, `V := {x | x ≠ north}` are open
42 (complement of a singleton in a T1 space) and cover.
432. `ContractibleSpace ↥U`: `Mathlib.Geometry.Manifold.Instances.Sphere`
44 has `stereographic` (a `PartialHomeomorph` from the sphere with source
45 `{pole}ᶜ` onto the orthogonal complement); extract a `Homeomorph` from
46 `↥U` to a normed space via `PartialHomeomorph.toHomeomorphSourceTarget`
47 (mind the subtype-of-subtype plumbing: `↥U` here is a subtype of the
48 sphere subtype), then `Homeomorph.contractibleSpace` against the convex
49 target (`Convex.contractibleSpace` is imported).
503. `U ∩ V ≃ₕ Sⁿ⁻¹` (homotopy equivalence): the retraction normalizes the
51 first `n` coordinates; away from both poles the horizontal component is
52 nonzero, so the map is continuous; the straight-line homotopy stays in
53 `U ∩ V` after renormalization. This is the one genuinely geometric
54 proof. Combine with layer 1's `homotopyEquiv_homology_iso` to move
55 `Hgrp` across, then feed `isIso_mvδ_of_contractible` /
56 `isZero_h1_of_contractible` to run the induction
57 `H_{k+1}(Sⁿ) ≅ H_k(Sⁿ⁻¹)` (`k ≥ 1`) with `H₁(Sⁿ) = 0` for `n ≥ 2`.
584. `H₁(S¹) ≅ ℤ`: the degree-0 end. Use `mv_exact₂` at degree 0,
59 `mvSum_epi_zero`, `mono_mvPair_zero`-style splitting, and the `H₀`
60 computations (this file's `augH`/`ptH` toolkit: `ptH_augH` pairs point
61 classes against clopen augmentations, `ptH_eq_of_joined` merges joined
62 points; for `U ∩ V ≃ₕ S⁰`, two components give `H₀ ≅ ℤ ⊕ ℤ` via the
63 two clopen augmentations). Alternatively settle for
64 `¬ IsZero (H₁(S¹))` (enough for Stage D's corollary) by showing `mvδ 0`
65 is nonzero: the class `ptH a − ptH b` of the two-point difference in
66 `H₀(U ∩ V)` is in `ker (mvPair 0)` (the points join inside `U` and
67 inside `V`) but nonzero (pair against a clopen augmentation separating
68 the two arcs, using `ptH_augH`); exactness (`mv_exact₁`) lifts it
69 through `mvδ`.
705. Stage D: `sphere_homology_top` (`H_n(Sⁿ) ≠ 0`, i.e. `¬ IsZero`; the
71 `≅ ℤ` form needs the iso carried through the induction, harder),
72 `sphere_homology_vanish` (`IsZero (H_k(Sⁿ))`, `k ≠ 0, n`), and
73 `spheres_not_homotopy_equivalent` via layer 1's
74 `homotopyEquiv_homology_iso` (transport `IsZero` across the iso and
75 contradict). `S⁰` base: totally disconnected, so
76 `isZero_homology_of_totallyDisconnected` gives all positive degrees.
77
78## Instance-diamond note (load-bearing, inherited from layer 4)
79
80For `R = ℤ` every `ModuleCat ℤ` carrier has two `Module ℤ` instances
81(`isModule` and `AddCommGroup.toIntModule`), propositionally but not
82definitionally equal, and synthesis prefers the generic one. This file
83deprioritizes `AddCommGroup.toIntModule` and `SubNegMonoid.toZSMul`
84locally, matching layers 1-4.
85-/
86import Mathlib.Algebra.Homology.Single
87import Mathlib.Algebra.Homology.SingleHomology
88import Mathlib.Topology.Homotopy.Contractible
89import Mathlib.Topology.Homotopy.Path
90import Mathlib.Analysis.Convex.Contractible
91import Mathlib.Analysis.Normed.Module.Connected
92import Mathlib.Geometry.Manifold.Instances.Sphere
93import IndisputableMonolith.Foundation.SingularPrism
94import IndisputableMonolith.Foundation.SingularPair
95import IndisputableMonolith.Foundation.SingularSubdivision
96import IndisputableMonolith.Foundation.SingularMayerVietoris
97
98namespace IndisputableMonolith
99namespace Foundation
100namespace SingularSphere
101
102open CategoryTheory Category Limits AlgebraicTopology Simplicial Opposite
103open SingularPrism SingularSubdivision SingularMayerVietoris
104
105attribute [local instance 10] Classical.decEq
106
107/- See the instance-diamond note in the module header. -/
108attribute [local instance 0] AddCommGroup.toIntModule
109attribute [local instance 0] SubNegMonoid.toZSMul
110
111/-! ## Stage A toolkit: points, augmentations, and the class of a point -/
112
113/-- The degree-`n` singular homology of `X` with `ℤ` coefficients. -/
114noncomputable abbrev Hgrp (X : TopCat.{0}) (n : ℕ) : ModuleCat.{0} ℤ :=
115 (SC X).homology n
116
117/-- `ℤ` as a chain complex concentrated in degree `0`. -/
118noncomputable abbrev Zsingle : ChainComplex (ModuleCat.{0} ℤ) ℕ :=
119 (ChainComplex.single₀ (ModuleCat.{0} ℤ)).obj (ModuleCat.of ℤ ℤ)
120
121/-- The unique point of the standard `0`-simplex. -/
122noncomputable def v0 : stdSimplex ℝ (Fin 1) :=
123 ⟨Pi.single 0 1, single_mem_stdSimplex ℝ 0⟩
124
125instance : Subsingleton (stdSimplex ℝ (Fin (0 + 1))) :=
126 ⟨fun a b => Subtype.ext (funext fun i => by
127 have ha : a.1 0 = 1 := by
128 have h2 := a.2.2
129 rw [Fin.sum_univ_succ, Finset.univ_eq_empty, Finset.sum_empty,
130 add_zero] at h2
131 exact h2
132 have hb : b.1 0 = 1 := by
133 have h2 := b.2.2
134 rw [Fin.sum_univ_succ, Finset.univ_eq_empty, Finset.sum_empty,
135 add_zero] at h2
136 exact h2
137 have hi : i = 0 := Fin.ext (by omega)
138 rw [hi, ha, hb])⟩
139
140/-- The underlying point of a singular `0`-simplex. -/
141noncomputable def pointOf {X : TopCat.{0}} (s : Idx X 0) : X :=
142 simplexEquiv X 0 s v0
143
144/-- The singular `0`-simplex sitting at a point. -/
145noncomputable def constSimplex (X : TopCat.{0}) (x : X) : Idx X 0 :=
146 (simplexEquiv X 0).symm (ContinuousMap.const _ x)
147
148@[simp] lemma pointOf_constSimplex (X : TopCat.{0}) (x : X) :
149 pointOf (constSimplex X x) = x := by
150 unfold pointOf constSimplex
151 rw [Equiv.apply_symm_apply]
152 rfl
153
154/-- Singular `0`-simplices are determined by their underlying point. -/
155lemma idx0_ext {X : TopCat.{0}} {s t : Idx X 0} (h : pointOf s = pointOf t) :
156 s = t := by
157 apply (simplexEquiv X 0).injective
158 ext z
159 rw [Subsingleton.elim z v0]
160 exact h
161
162lemma constSimplex_pointOf {X : TopCat.{0}} (s : Idx X 0) :
163 constSimplex X (pointOf s) = s :=
164 idx0_ext (by rw [pointOf_constSimplex])
165
166/-- The point of a pushforward simplex is the image of the point. -/
167lemma pointOf_map {X Y : TopCat.{0}} (f : X ⟶ Y) (s : Idx X 0) :
168 pointOf ((TopCat.toSSet.map f).app (op ⦋0⦌) s) = f.hom (pointOf s) := by
169 unfold pointOf
170 rw [simplexEquiv_map]
171 rfl
172
173/-- The point of the `k`-th face of a singular `1`-simplex. -/
174lemma pointOf_δ {X : TopCat.{0}} (σ : Idx X 1) (k : Fin 2) :
175 pointOf ((TopCat.toSSet.obj X).δ k σ) =
176 simplexEquiv X 1 σ (SingularPrism.face k v0) := by
177 unfold pointOf
178 rw [simplexEquiv_δ]
179 rfl
180
181open Classical in
182/-- The partial augmentation against a set `A`: a `0`-simplex counts with
183coefficient `1` when its point lies in `A` and `0` otherwise. -/
184noncomputable def augFun (X : TopCat.{0}) (A : Set X) :
185 Cgrp X 0 ⟶ ModuleCat.of ℤ ℤ :=
186 Sigma.desc fun s => if pointOf s ∈ A then 𝟙 (ModuleCat.of ℤ ℤ) else 0
187
188open Classical in
189lemma gen_augFun {X : TopCat.{0}} {A : Set X} (s : Idx X 0) :
190 gen X 0 s ≫ augFun X A =
191 if pointOf s ∈ A then 𝟙 (ModuleCat.of ℤ ℤ) else 0 :=
192 Sigma.ι_desc _ _
193
194open Classical in
195lemma augFun_genUnit {X : TopCat.{0}} {A : Set X} (s : Idx X 0) :
196 augFun X A (genUnit X 0 s) = if pointOf s ∈ A then (1 : ℤ) else 0 := by
197 rw [genUnit_eq, ← ModuleCat.comp_apply, gen_augFun]
198 by_cases h : pointOf s ∈ A
199 · rw [if_pos h, if_pos h, ModuleCat.id_apply]
200 · rw [if_neg h, if_neg h, zeroApp]
201
202/-- Both endpoints of a singular `1`-simplex lie on the same side of a
203clopen set (the image of the connected `Δ¹` cannot cross it). -/
204lemma mem_iff_of_clopen_δ {X : TopCat.{0}} {A : Set X} (hA : IsClopen A)
205 (σ : Idx X 1) :
206 (pointOf ((TopCat.toSSet.obj X).δ (0 : Fin 2) σ) ∈ A ↔
207 pointOf ((TopCat.toSSet.obj X).δ (1 : Fin 2) σ) ∈ A) := by
208 rw [pointOf_δ, pointOf_δ]
209 set f := simplexEquiv X 1 σ with hf
210 have hS : IsClopen (⇑f ⁻¹' A) := hA.preimage f.continuous
211 rcases isClopen_iff.mp hS with h | h
212 · constructor
213 · intro hx
214 exact absurd (show SingularPrism.face (0 : Fin 2) v0 ∈ ⇑f ⁻¹' A from hx)
215 (by rw [h]; exact Set.notMem_empty _)
216 · intro hx
217 exact absurd (show SingularPrism.face (1 : Fin 2) v0 ∈ ⇑f ⁻¹' A from hx)
218 (by rw [h]; exact Set.notMem_empty _)
219 · constructor
220 · intro _
221 have : SingularPrism.face (1 : Fin 2) v0 ∈ ⇑f ⁻¹' A := by
222 rw [h]; trivial
223 exact this
224 · intro _
225 have : SingularPrism.face (0 : Fin 2) v0 ∈ ⇑f ⁻¹' A := by
226 rw [h]; trivial
227 exact this
228
229open Classical in
230/-- The partial augmentation against a clopen set kills boundaries. -/
231lemma bnd_augFun {X : TopCat.{0}} {A : Set X} (hA : IsClopen A) :
232 bnd X 0 ≫ augFun X A = 0 := by
233 apply Sigma.hom_ext
234 intro σ
235 rw [comp_zero, ← assoc]
236 rw [show Sigma.ι (fun _ : Idx X 1 => ModuleCat.of ℤ ℤ) σ ≫ bnd X 0 =
237 ∑ k : Fin 2, (-1 : ℤ) ^ (k : ℕ) •
238 gen X 0 ((TopCat.toSSet.obj X).δ k σ) from gen_d X 0 σ]
239 rw [Preadditive.sum_comp, Fin.sum_univ_two, Preadditive.zsmul_comp,
240 Preadditive.zsmul_comp, gen_augFun, gen_augFun]
241 by_cases h : pointOf ((TopCat.toSSet.obj X).δ (0 : Fin 2) σ) ∈ A
242 · rw [if_pos h, if_pos ((mem_iff_of_clopen_δ hA σ).mp h)]
243 simp only [Fin.val_zero, Fin.val_one, pow_zero, pow_one, one_smul, neg_smul,
244 one_smul]
245 exact add_neg_cancel _
246 · rw [if_neg h, if_neg (fun h1 => h ((mem_iff_of_clopen_δ hA σ).mpr h1))]
247 simp only [smul_zero, add_zero]
248
249open Classical in
250/-- The augmentation against a clopen set, as a chain map to `ℤ`
251concentrated in degree `0`. -/
252noncomputable def augTo (X : TopCat.{0}) (A : Set X) (hA : IsClopen A) :
253 SC X ⟶ Zsingle :=
254 HomologicalComplex.mkHomToSingle (augFun X A) (by
255 rintro i (hi : 0 + 1 = i)
256 obtain rfl : i = 1 := by omega
257 exact bnd_augFun hA)
258
259open Classical in
260lemma augTo_f_zero (X : TopCat.{0}) (A : Set X) (hA : IsClopen A) :
261 (augTo X A hA).f 0 = augFun X A := by
262 rw [augTo, HomologicalComplex.mkHomToSingle_f, ChainComplex.single₀ObjXSelf,
263 Iso.refl_inv]
264 exact comp_id _
265
266/-- The class of a point, as a chain map from `ℤ` concentrated in degree
267`0`. -/
268noncomputable def ptFrom (X : TopCat.{0}) (x : X) : Zsingle ⟶ SC X :=
269 HomologicalComplex.mkHomFromSingle (gen X 0 (constSimplex X x)) (by
270 rintro k (hk : k + 1 = 0)
271 exact absurd hk (by omega))
272
273lemma ptFrom_f_zero (X : TopCat.{0}) (x : X) :
274 (ptFrom X x).f 0 = gen X 0 (constSimplex X x) := by
275 rw [ptFrom, HomologicalComplex.mkHomFromSingle_f, ChainComplex.single₀ObjXSelf,
276 Iso.refl_hom, id_comp]
277
278open Classical in
279/-- Pairing the class of a point against a clopen augmentation. -/
280lemma ptFrom_augTo (X : TopCat.{0}) (x : X) (A : Set X) (hA : IsClopen A) :
281 ptFrom X x ≫ augTo X A hA =
282 if x ∈ A then 𝟙 Zsingle else 0 := by
283 apply HomologicalComplex.from_single_hom_ext
284 rw [HomologicalComplex.comp_f, ptFrom_f_zero, augTo_f_zero, gen_augFun,
285 pointOf_constSimplex]
286 by_cases h : x ∈ A
287 · rw [if_pos h, if_pos h, HomologicalComplex.id_f]
288 rfl
289 · rw [if_neg h, if_neg h]
290 rfl
291
292/-- The canonical identification `H₀(ℤ[0]) ≅ ℤ`. -/
293noncomputable abbrev ZsingleH0Iso : Zsingle.homology 0 ≅ ModuleCat.of ℤ ℤ :=
294 HomologicalComplex.singleObjHomologySelfIso (ComplexShape.down ℕ) 0 _
295
296/-- The degree-`0` homology augmentation against a clopen set. -/
297noncomputable def augH (X : TopCat.{0}) (A : Set X) (hA : IsClopen A) :
298 Hgrp X 0 ⟶ ModuleCat.of ℤ ℤ :=
299 HomologicalComplex.homologyMap (augTo X A hA) 0 ≫ ZsingleH0Iso.hom
300
301/-- The degree-`0` homology class of a point. -/
302noncomputable def ptH (X : TopCat.{0}) (x : X) :
303 ModuleCat.of ℤ ℤ ⟶ Hgrp X 0 :=
304 ZsingleH0Iso.inv ≫ HomologicalComplex.homologyMap (ptFrom X x) 0
305
306open Classical in
307/-- The pairing of the class of a point against a clopen augmentation. -/
308lemma ptH_augH (X : TopCat.{0}) (x : X) (A : Set X) (hA : IsClopen A) :
309 ptH X x ≫ augH X A hA =
310 if x ∈ A then 𝟙 (ModuleCat.of ℤ ℤ) else 0 := by
311 unfold ptH augH
312 rw [assoc, ← assoc (HomologicalComplex.homologyMap (ptFrom X x) 0),
313 ← HomologicalComplex.homologyMap_comp, ptFrom_augTo]
314 by_cases h : x ∈ A
315 · rw [if_pos h, if_pos h, HomologicalComplex.homologyMap_id, id_comp,
316 Iso.inv_hom_id]
317 · rw [if_neg h, if_neg h, HomologicalComplex.homologyMap_zero, zero_comp,
318 comp_zero]
319
320/-- The identity of `ℤ` is not the zero morphism (used to convert split
321monos out of `ℤ` into non-vanishing statements). -/
322lemma id_int_ne_zero : 𝟙 (ModuleCat.of ℤ ℤ) ≠ 0 := by
323 intro h
324 have h1 : (𝟙 (ModuleCat.of ℤ ℤ)) (1 : ℤ) = (0 : ModuleCat.of ℤ ℤ ⟶ _) (1 : ℤ) := by
325 rw [h]
326 rw [ModuleCat.id_apply, zeroApp] at h1
327 exact one_ne_zero h1
328
329/-! ## Stage A toolkit: path simplices -/
330
331/-- The homeomorphism `Δ¹ ≃ₜ I`, as a continuous map. -/
332noncomputable def simplexToI : C(stdSimplex ℝ (Fin 2), unitInterval) :=
333 ⟨stdSimplexHomeomorphUnitInterval, stdSimplexHomeomorphUnitInterval.continuous⟩
334
335/-- The singular `1`-simplex of a path. -/
336noncomputable def pathSimplex {X : TopCat.{0}} {x y : X} (γ : Path x y) :
337 Idx X 1 :=
338 (simplexEquiv X 1).symm (γ.toContinuousMap.comp simplexToI)
339
340lemma coord_face_v0 (k : Fin 2) :
341 (SingularPrism.face k v0).1 1 = if k = 0 then (1 : ℝ) else 0 := by
342 have h := SingularPrism.sum_filter_map_apply (a := Fin 1) (b := Fin 2)
343 k.succAbove (fun j => j = (1 : Fin 2)) v0
344 have hL : ∑ j with j = (1 : Fin 2), stdSimplex.map k.succAbove v0 j =
345 stdSimplex.map k.succAbove v0 1 := by
346 rw [Finset.filter_eq', if_pos (Finset.mem_univ _), Finset.sum_singleton]
347 have hcoord : ((k.succAbove 0 : Fin 2) : ℕ) = if k = 0 then 1 else 0 := by
348 rw [coe_succAbove]
349 fin_cases k <;> simp
350 have hR : ∑ m with k.succAbove m = (1 : Fin 2), v0.1 m =
351 if k = 0 then (1 : ℝ) else 0 := by
352 by_cases hk : k = 0
353 · subst hk
354 rw [if_pos rfl]
355 have hfil : ({m : Fin 1 | (0 : Fin 2).succAbove m = 1} : Finset (Fin 1)) =
356 {0} := by
357 apply Finset.ext
358 intro m
359 rw [Subsingleton.elim m (0 : Fin 1)]
360 constructor
361 · intro _
362 exact Finset.mem_singleton_self 0
363 · intro _
364 rw [Finset.mem_filter_univ]
365 decide
366 rw [hfil, Finset.sum_singleton]
367 show (Pi.single (0 : Fin 1) (1 : ℝ) : Fin 1 → ℝ) 0 = 1
368 rw [Pi.single_eq_same]
369 · rw [if_neg hk]
370 apply Finset.sum_eq_zero
371 intro m hm
372 exfalso
373 rw [Finset.mem_filter_univ] at hm
374 have h0 : ((k.succAbove m : Fin 2) : ℕ) = 1 := by rw [hm]; decide
375 rw [Subsingleton.elim m 0] at h0
376 rw [hcoord, if_neg hk] at h0
377 exact one_ne_zero h0.symm
378 show (stdSimplex.map k.succAbove v0).1 1 = _
379 calc (stdSimplex.map k.succAbove v0).1 1
380 = ∑ j with j = (1 : Fin 2), stdSimplex.map k.succAbove v0 j := hL.symm
381 _ = ∑ m with k.succAbove m = (1 : Fin 2), v0 m := h
382 _ = if k = 0 then (1 : ℝ) else 0 := hR
383
384lemma simplexToI_face_v0 (k : Fin 2) :
385 simplexToI (SingularPrism.face k v0) = if k = 0 then 1 else 0 := by
386 apply Subtype.ext
387 show ((SingularPrism.face k v0).1 1) = _
388 rw [coord_face_v0]
389 by_cases hk : k = 0
390 · rw [if_pos hk, if_pos hk]
391 rfl
392 · rw [if_neg hk, if_neg hk]
393 rfl
394
395lemma pointOf_δ_pathSimplex {X : TopCat.{0}} {x y : X} (γ : Path x y)
396 (k : Fin 2) :
397 pointOf ((TopCat.toSSet.obj X).δ k (pathSimplex γ)) =
398 if k = 0 then y else x := by
399 rw [pointOf_δ]
400 unfold pathSimplex
401 rw [Equiv.apply_symm_apply]
402 show γ (simplexToI (SingularPrism.face k v0)) = _
403 rw [simplexToI_face_v0]
404 by_cases hk : k = 0
405 · rw [if_pos hk, if_pos hk, Path.target]
406 · rw [if_neg hk, if_neg hk, Path.source]
407
408/-- The boundary of a path simplex: `∂[γ] = [target] − [source]`. -/
409lemma gen_pathSimplex_bnd {X : TopCat.{0}} {x y : X} (γ : Path x y) :
410 gen X 1 (pathSimplex γ) ≫ bnd X 0 =
411 gen X 0 (constSimplex X y) - gen X 0 (constSimplex X x) := by
412 rw [gen_d, Fin.sum_univ_two]
413 simp only [Fin.val_zero, Fin.val_one, pow_zero, pow_one]
414 rw [show (TopCat.toSSet.obj X).δ (0 : Fin 2) (pathSimplex γ) = constSimplex X y from
415 idx0_ext (by rw [pointOf_δ_pathSimplex, if_pos rfl, pointOf_constSimplex]),
416 show (TopCat.toSSet.obj X).δ (1 : Fin 2) (pathSimplex γ) = constSimplex X x from
417 idx0_ext (by rw [pointOf_δ_pathSimplex, if_neg (by decide), pointOf_constSimplex]),
418 one_zsmul, neg_one_zsmul, ← sub_eq_add_neg]
419
420lemma subApp {M N : ModuleCat.{0} ℤ} (f g : M ⟶ N) (z : M) :
421 (f - g) z = f z - g z := by
422 rw [sub_eq_add_neg, addApp, negApp, ← sub_eq_add_neg]
423
424/-- Elementwise boundary of a path simplex. -/
425lemma bnd_genUnit_pathSimplex {X : TopCat.{0}} {x y : X} (γ : Path x y) :
426 bnd X 0 (genUnit X 1 (pathSimplex γ)) =
427 genUnit X 0 (constSimplex X y) - genUnit X 0 (constSimplex X x) := by
428 rw [genUnit_eq, ← ModuleCat.comp_apply]
429 calc (gen X 1 (pathSimplex γ) ≫ bnd X 0) (1 : ℤ)
430 = (gen X 0 (constSimplex X y) - gen X 0 (constSimplex X x)) (1 : ℤ) := by
431 rw [gen_pathSimplex_bnd]
432 _ = genUnit X 0 (constSimplex X y) - genUnit X 0 (constSimplex X x) := by
433 rw [subApp, genUnit_eq, genUnit_eq]
434
435/-- Joined points have homologous point chains. -/
436lemma exists_bnd_eq_sub {X : TopCat.{0}} {x y : X} (h : Joined x y) :
437 ∃ w : ↥(Cgrp X 1),
438 bnd X 0 w = genUnit X 0 (constSimplex X y) -
439 genUnit X 0 (constSimplex X x) :=
440 ⟨genUnit X 1 (pathSimplex h.somePath), bnd_genUnit_pathSimplex h.somePath⟩
441
442/-! ## Stage A: `H₀` of a path-connected space -/
443
444open Classical in
445/-- In a path-connected space, every `0`-chain is homologous to its total
446augmentation times a base point. -/
447lemma exists_bnd_of_pathConnected {X : TopCat.{0}} [PathConnectedSpace X]
448 (x₀ : X) (z : ↥(Cgrp X 0)) :
449 ∃ v : ↥(Cgrp X 1),
450 bnd X 0 v =
451 z - gen X 0 (constSimplex X x₀) (augFun X Set.univ z) := by
452 induction z using freeInduction with
453 | unit s =>
454 obtain ⟨w, hw⟩ := exists_bnd_eq_sub
455 (PathConnectedSpace.joined x₀ (pointOf s))
456 refine ⟨w, ?_⟩
457 rw [hw, constSimplex_pointOf]
458 rw [show (unitOf s : ↥(Cgrp X 0)) = genUnit X 0 s from rfl,
459 augFun_genUnit, if_pos (Set.mem_univ _), ← genUnit_eq]
460 | zero =>
461 refine ⟨0, ?_⟩
462 rw [map_zero, map_zero, map_zero, sub_zero]
463 | add a b ha hb =>
464 obtain ⟨va, hva⟩ := ha
465 obtain ⟨vb, hvb⟩ := hb
466 refine ⟨va + vb, ?_⟩
467 rw [map_add, hva, hvb, map_add, map_add]
468 abel
469 | smulz c a ha =>
470 obtain ⟨v, hv⟩ := ha
471 refine ⟨c • v, ?_⟩
472 rw [mapSmul, hv, mapSmul, mapSmul, smul_sub]
473
474open Classical in
475/-- Elementwise form of `augTo_f_zero`, bridging the coercion at
476`Zsingle.X 0` against the coercion at `ModuleCat.of ℤ ℤ`. -/
477lemma augTo_f_zero_apply (X : TopCat.{0}) (A : Set X) (hA : IsClopen A)
478 (c : ↥(Cgrp X 0)) :
479 (ConcreteCategory.hom ((augTo X A hA).f 0)) c = augFun X A c :=
480 congrArg (fun ψ => (ConcreteCategory.hom ψ) c) (augTo_f_zero X A hA)
481
482/-- The differential out of degree `1` of the single complex vanishes. -/
483lemma Zsingle_d_one_zero : Zsingle.d 1 0 = 0 :=
484 (HomologicalComplex.isZero_single_obj_X (ComplexShape.down ℕ) 0
485 (ModuleCat.of ℤ ℤ) 1 one_ne_zero).eq_of_src _ _
486
487open Classical in
488/-- **`H₀` of a path-connected space.** The augmentation induces an
489isomorphism `H₀(X) ≅ ℤ` on homology. -/
490theorem isIso_homologyMap_augTo (X : TopCat.{0}) [PathConnectedSpace X] :
491 IsIso (HomologicalComplex.homologyMap
492 (augTo X Set.univ isClopen_univ) 0) := by
493 obtain ⟨x₀⟩ : Nonempty ↥X := PathConnectedSpace.nonempty
494 apply isIso_homologyMap_chain_zero
495 · intro y
496 refine ⟨gen X 0 (constSimplex X x₀) (show ℤ from y), 0, ?_⟩
497 rw [Zsingle_d_one_zero, zeroApp, add_zero, augTo_f_zero_apply,
498 ← ModuleCat.comp_apply, gen_augFun, if_pos (Set.mem_univ _)]
499 exact ModuleCat.id_apply _ _
500 · intro z hz
501 obtain ⟨w, hw⟩ := hz
502 have hz0 : augFun X Set.univ z = 0 := by
503 rw [augTo_f_zero_apply, Zsingle_d_one_zero, zeroApp] at hw
504 exact hw
505 obtain ⟨v, hv⟩ := exists_bnd_of_pathConnected x₀ z
506 rw [hz0, map_zero, sub_zero] at hv
507 exact ⟨v, hv.symm⟩
508
509/-- The homology augmentation `H₀(X) ⟶ ℤ` of a path-connected space is an
510isomorphism. -/
511theorem isIso_augH_of_pathConnected (X : TopCat.{0}) [PathConnectedSpace X] :
512 IsIso (augH X Set.univ isClopen_univ) := by
513 haveI := isIso_homologyMap_augTo X
514 unfold augH
515 infer_instance
516
517/-! ## Stage A/B: vanishing in positive degrees -/
518
519instance : TotallyDisconnectedSpace Unit :=
520 ⟨fun _ _ _ => Set.subsingleton_of_subsingleton⟩
521
522/-- Positive-degree singular homology of a totally disconnected space
523vanishes (Mathlib), retyped onto `Hgrp`. -/
524lemma isZero_homology_of_totallyDisconnected (X : TopCat.{0})
525 [TotallyDisconnectedSpace X] {m : ℕ} (hm : m ≠ 0) :
526 IsZero (Hgrp X m) :=
527 isZero_singularHomologyFunctor_of_totallyDisconnectedSpace
528 (ModuleCat.{0} ℤ) m (ModuleCat.of ℤ ℤ) X hm
529
530/-- **Stage B.** Positive-degree singular homology of a contractible space
531vanishes. -/
532theorem isZero_homology_of_contractible (X : TopCat.{0})
533 [ContractibleSpace X] {m : ℕ} (hm : m ≠ 0) :
534 IsZero (Hgrp X m) := by
535 obtain ⟨e⟩ := ContractibleSpace.hequiv_unit (X : Type)
536 have hzero : IsZero (Hgrp (TopCat.of Unit) m) :=
537 isZero_homology_of_totallyDisconnected (TopCat.of Unit) hm
538 exact hzero.of_iso
539 (homotopyEquiv_homology_iso (X := X) (Y := TopCat.of Unit) e m)
540
541/-! ## Stage A/B: naturality of augmentations and point classes -/
542
543open Classical in
544lemma sChainMap_augTo {X Y : TopCat.{0}} (f : X ⟶ Y) :
545 sChainMap f ≫ augTo Y Set.univ isClopen_univ =
546 augTo X Set.univ isClopen_univ := by
547 apply HomologicalComplex.to_single_hom_ext
548 rw [HomologicalComplex.comp_f, augTo_f_zero, augTo_f_zero]
549 show chainMap f 0 ≫ augFun Y Set.univ = augFun X Set.univ
550 apply Sigma.hom_ext
551 intro s
552 rw [← assoc]
553 rw [show Sigma.ι (fun _ : Idx X 0 => ModuleCat.of ℤ ℤ) s ≫ chainMap f 0 =
554 gen Y 0 ((TopCat.toSSet.map f).app (op ⦋0⦌) s) from gen_map f 0 s]
555 rw [gen_augFun, gen_augFun, if_pos (Set.mem_univ _), if_pos (Set.mem_univ _)]
556
557lemma homologyMap_augH {X Y : TopCat.{0}} (f : X ⟶ Y) :
558 HomologicalComplex.homologyMap (sChainMap f) 0 ≫
559 augH Y Set.univ isClopen_univ = augH X Set.univ isClopen_univ := by
560 unfold augH
561 rw [← assoc, ← HomologicalComplex.homologyMap_comp, sChainMap_augTo]
562
563lemma ptFrom_sChainMap {X Y : TopCat.{0}} (f : X ⟶ Y) (x : X) :
564 ptFrom X x ≫ sChainMap f = ptFrom Y (f.hom x) := by
565 apply HomologicalComplex.from_single_hom_ext
566 rw [HomologicalComplex.comp_f, ptFrom_f_zero, ptFrom_f_zero]
567 show gen X 0 (constSimplex X x) ≫ chainMap f 0 = gen Y 0 (constSimplex Y (f.hom x))
568 rw [gen_map,
569 show (TopCat.toSSet.map f).app (op ⦋0⦌) (constSimplex X x) =
570 constSimplex Y (f.hom x) from idx0_ext
571 (by rw [pointOf_map, pointOf_constSimplex, pointOf_constSimplex])]
572
573lemma ptH_natural {X Y : TopCat.{0}} (f : X ⟶ Y) (x : X) :
574 ptH X x ≫ HomologicalComplex.homologyMap (sChainMap f) 0 =
575 ptH Y (f.hom x) := by
576 unfold ptH
577 rw [assoc, ← HomologicalComplex.homologyMap_comp, ptFrom_sChainMap]
578
579/-- A path between points gives a chain homotopy between the point chain
580maps. -/
581noncomputable def ptFromHomotopy {X : TopCat.{0}} {x y : X} (γ : Path x y) :
582 Homotopy (ptFrom X x) (ptFrom X y) where
583 hom i j :=
584 if h : i = 0 ∧ j = 1 then
585 eqToHom (by rw [h.1]) ≫
586 ((HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0
587 (ModuleCat.of ℤ ℤ)).hom ≫ gen X 1 (pathSimplex γ.symm)) ≫
588 eqToHom (by rw [h.2]; rfl)
589 else 0
590 zero i j hij := by
591 rw [dif_neg]
592 rintro ⟨rfl, rfl⟩
593 exact hij rfl
594 comm i := by
595 match i with
596 | 0 =>
597 rw [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex]
598 rw [dif_pos ⟨rfl, rfl⟩, eqToHom_refl, eqToHom_refl, id_comp, comp_id]
599 rw [ptFrom, HomologicalComplex.mkHomFromSingle_f,
600 show (ptFrom X y).f 0 = (HomologicalComplex.singleObjXSelf
601 (ComplexShape.down ℕ) 0 (ModuleCat.of ℤ ℤ)).hom ≫
602 gen X 0 (constSimplex X y) from
603 HomologicalComplex.mkHomFromSingle_f _ _]
604 rw [assoc]
605 rw [show gen X 1 (pathSimplex γ.symm) ≫ (SC X).d 1 0 =
606 gen X 0 (constSimplex X x) - gen X 0 (constSimplex X y) from
607 gen_pathSimplex_bnd γ.symm]
608 rw [zero_add, ← Preadditive.comp_add]
609 congr 1
610 abel
611 | n + 1 =>
612 exact (HomologicalComplex.isZero_single_obj_X (ComplexShape.down ℕ) 0
613 (ModuleCat.of ℤ ℤ) (n + 1) (by omega)).eq_of_src _ _
614
615/-- Joined points have equal degree-`0` homology classes. -/
616lemma ptH_eq_of_joined {X : TopCat.{0}} {x y : X} (h : Joined x y) :
617 ptH X x = ptH X y := by
618 unfold ptH
619 rw [(ptFromHomotopy h.somePath).homologyMap_eq 0]
620
621/-! ## Stage A/B exports -/
622
623/-- **Stage A/B.** `H₀(X) ≅ ℤ` for a path-connected space, via the
624augmentation. -/
625noncomputable def h0_iso_int (X : TopCat.{0}) [PathConnectedSpace X] :
626 Hgrp X 0 ≅ ModuleCat.of ℤ ℤ :=
627 haveI := isIso_augH_of_pathConnected X
628 asIso (augH X Set.univ isClopen_univ)
629
630/-- **Stage A.** `H₀(pt) ≅ ℤ`. -/
631noncomputable def h0_pt_iso_int :
632 Hgrp (TopCat.of Unit) 0 ≅ ModuleCat.of ℤ ℤ :=
633 h0_iso_int (TopCat.of Unit)
634
635/-- **Stage A.** `H_m(pt) = 0` for `m ≠ 0`. -/
636lemma hn_pt_isZero {m : ℕ} (hm : m ≠ 0) : IsZero (Hgrp (TopCat.of Unit) m) :=
637 isZero_homology_of_totallyDisconnected (TopCat.of Unit) hm
638
639/-- **Stage B.** `H₀(X) ≅ ℤ` for a contractible space. -/
640noncomputable def h0_contractible_iso_int (X : TopCat.{0})
641 [ContractibleSpace X] : Hgrp X 0 ≅ ModuleCat.of ℤ ℤ :=
642 h0_iso_int X
643
644/-! ## Stage C (abstract): Mayer-Vietoris consequences -/
645
646section AbstractMV
647
648variable {X : TopCat.{0}} {U V : Set X}
649
650/-- **The suspension step.** If `H_{n+1}` and `H_n` of both `U` and `V`
651vanish, the Mayer-Vietoris connecting map `∂ : H_{n+1}(X) ⟶ H_n(U ∩ V)` is
652an isomorphism. -/
653theorem isIso_mvδ (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
654 (n : ℕ)
655 (hU1 : IsZero (Hgrp (TopCat.of U) (n + 1)))
656 (hV1 : IsZero (Hgrp (TopCat.of V) (n + 1)))
657 (hUn : IsZero (Hgrp (TopCat.of U) n))
658 (hVn : IsZero (Hgrp (TopCat.of V) n)) :
659 IsIso (mvδ hU hV hUV n) := by
660 haveI : Mono (mvδ hU hV hUV n) :=
661 (mv_exact₃ hU hV hUV n).mono_g
662 (((biprod_isZero_iff _ _).mpr ⟨hU1, hV1⟩).eq_of_src _ _)
663 haveI : Epi (mvδ hU hV hUV n) :=
664 (mv_exact₁ hU hV hUV n).epi_f
665 (((biprod_isZero_iff _ _).mpr ⟨hUn, hVn⟩).eq_of_tgt _ _)
666 exact isIso_of_mono_of_epi _
667
668/-- With contractible pieces the connecting map is an isomorphism
669`∂ : H_{n+2}(X) ≅ H_{n+1}(U ∩ V)` in all degrees `≥ 2`. -/
670theorem isIso_mvδ_of_contractible (hU : IsOpen U) (hV : IsOpen V)
671 (hUV : U ∪ V = Set.univ) (n : ℕ)
672 [ContractibleSpace ↥U] [ContractibleSpace ↥V] :
673 IsIso (mvδ hU hV hUV (n + 1)) :=
674 isIso_mvδ hU hV hUV (n + 1)
675 (isZero_homology_of_contractible _ (by omega))
676 (isZero_homology_of_contractible _ (by omega))
677 (isZero_homology_of_contractible _ (by omega))
678 (isZero_homology_of_contractible _ (by omega))
679
680/-- Vanishing transported across the connecting isomorphism:
681if `H_{n+1}(U ∩ V) = 0` then `H_{n+2}(X) = 0` (contractible pieces). -/
682theorem isZero_of_isZero_inter (hU : IsOpen U) (hV : IsOpen V)
683 (hUV : U ∪ V = Set.univ) (n : ℕ)
684 [ContractibleSpace ↥U] [ContractibleSpace ↥V]
685 (h : IsZero (Hgrp (TopCat.of (U ∩ V : Set X)) (n + 1))) :
686 IsZero (Hgrp X (n + 2)) := by
687 haveI := isIso_mvδ_of_contractible hU hV hUV n
688 exact h.of_iso (asIso (mvδ hU hV hUV (n + 1)))
689
690/-- The Mayer-Vietoris pair map is mono in degree `0` when `U ∩ V` is path
691connected (its first component is split by the augmentation). -/
692theorem mono_mvPair_zero (U V : Set X)
693 [PathConnectedSpace ↥(U ∩ V : Set X)] :
694 Mono (mvPair U V 0) := by
695 haveI : IsIso (augH (TopCat.of (U ∩ V : Set X)) Set.univ isClopen_univ) :=
696 isIso_augH_of_pathConnected _
697 haveI hm1 : Mono (HomologicalComplex.homologyMap
698 (sChainMap (mvInclU U V)) 0 ≫
699 augH (TopCat.of U) Set.univ isClopen_univ) := by
700 rw [homologyMap_augH]
701 infer_instance
702 haveI hm2 : Mono (HomologicalComplex.homologyMap
703 (sChainMap (mvInclU U V)) 0) :=
704 mono_of_mono _ (augH (TopCat.of U) Set.univ isClopen_univ)
705 have hfac : mvPair U V 0 ≫
706 (biprod.fst : _ ⟶ Hgrp (TopCat.of U) 0) =
707 HomologicalComplex.homologyMap (sChainMap (mvInclU U V)) 0 :=
708 biprod.lift_fst _ _
709 haveI : Mono (mvPair U V 0 ≫
710 (biprod.fst : _ ⟶ Hgrp (TopCat.of U) 0)) := by
711 rw [hfac]
712 exact hm2
713 exact mono_of_mono (mvPair U V 0) biprod.fst
714
715/-- **Low degree.** If `U, V` kill `H₁` and `U ∩ V` is path connected,
716then `H₁(X) = 0`. -/
717theorem isZero_h1 (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
718 [PathConnectedSpace ↥(U ∩ V : Set X)]
719 (hU1 : IsZero (Hgrp (TopCat.of U) 1))
720 (hV1 : IsZero (Hgrp (TopCat.of V) 1)) :
721 IsZero (Hgrp X 1) := by
722 haveI : Mono (mvδ hU hV hUV 0) :=
723 (mv_exact₃ hU hV hUV 0).mono_g
724 (((biprod_isZero_iff _ _).mpr ⟨hU1, hV1⟩).eq_of_src _ _)
725 haveI := mono_mvPair_zero U V
726 have h0 : mvδ hU hV hUV 0 = 0 :=
727 zero_of_comp_mono (mvPair U V 0) (mvδ_comp_mvPair hU hV hUV 0)
728 exact IsZero.of_mono_eq_zero _ h0
729
730/-- `H₁` vanishing with contractible pieces and path-connected
731intersection. -/
732theorem isZero_h1_of_contractible (hU : IsOpen U) (hV : IsOpen V)
733 (hUV : U ∪ V = Set.univ)
734 [ContractibleSpace ↥U] [ContractibleSpace ↥V]
735 [PathConnectedSpace ↥(U ∩ V : Set X)] :
736 IsZero (Hgrp X 1) :=
737 isZero_h1 hU hV hUV
738 (isZero_homology_of_contractible _ one_ne_zero)
739 (isZero_homology_of_contractible _ one_ne_zero)
740
741end AbstractMV
742
743end SingularSphere
744end Foundation
745end IndisputableMonolith
746