IndisputableMonolith.Foundation.SingularSphereGeometry
IndisputableMonolith/Foundation/SingularSphereGeometry.lean · 695 lines · 66 declarations
show as:
view math explainer →
1/-
2Sphere homology `H_*(Sⁿ; ℤ)`: the geometric half of Stage C, and Stage D.
3
4Layer 5b of the excision spine, continuing `SingularSphere.lean` (which
5holds Stages A/B and the abstract Mayer-Vietoris consequences).
6
7## Contents
8
9* Step 1 (concrete cover): `Sph n` is the unit sphere in
10 `EuclideanSpace ℝ (Fin (n+1))`; `coverU`/`coverV` remove the south/north
11 pole; both are open, cover, and are contractible via Mathlib's
12 stereographic projection (`contractibleSpace_compl_singleton_sphere`).
13* Step 2 (equator, homotopy type of the intersection): rather than the
14 hand-rolled normalization retraction sketched in the parent frontier
15 note, we compose the stereographic homeomorphism (punctured sphere ≅
16 orthogonal hyperplane, with the second pole going to `0`) with Mathlib's
17 polar-coordinates homeomorphism `homeomorphUnitSphereProd`
18 (`{0}ᶜ ≃ₜ sphere × (0,∞)`) and collapse the contractible factor:
19 `coverU ∩ coverV ≃ₕ Sⁿ⁻¹` (`interHomotopyEquiv`).
20* Step 3 (induction): the suspension isomorphism
21 `H_{k+2}(Sⁿ⁺¹) ≅ H_{k+1}(Sⁿ)` (`suspensionIso`), the base case `S⁰`
22 (finite, hence discrete and totally disconnected), `H₁(Sⁿ⁺²) = 0`
23 (path-connected intersection), and the non-vanishing of `H₁(S¹)`
24 (a point-difference class in the two-arc intersection is a nonzero
25 kernel element of the Mayer-Vietoris pair map, hence lifts through the
26 connecting map by exactness).
27* Step 4 (Stage D exports; all `#print axioms`-clean, only `propext`,
28 `Classical.choice`, `Quot.sound`):
29 - `sphere_top_ne_zero : ¬ IsZero (H_n(Sⁿ))` for `1 ≤ n`;
30 - `sphere_homology_vanish : IsZero (H_k(Sⁿ))` for `1 ≤ k`, `k ≠ n`;
31 - `spheres_not_homotopyEquivalent :
32 m ≠ n → IsEmpty (HomotopyEquiv Sᵐ Sⁿ)`;
33 - `sphere_dim_eq_of_homotopyEquiv` (the `Nonempty → m = n` form).
34
35## FRONTIER (for the next worker)
36
37Stages A-D of the excision spine are COMPLETE: this file builds green,
380 sorry, 0 new axioms, on top of `SingularSphere.lean` (Stages A/B/C).
39The sphere model is `Sph n := TopCat.of (Metric.sphere
40(0 : EuclideanSpace ℝ (Fin (n+1))) 1)` with homology `Hgrp (Sph n) k`.
41
42Next: the campaign consumers.
431. The `D = 2` and `D ≥ 4` linking-vanishing argument consuming Stage D:
44 spheres `S¹`/`S^{D-2}` can be unlinked in dimension `D ≠ 3` because the
45 relevant homology/homotopy obstruction vanishes there; the Stage D
46 exports supply the dimension-detection facts
47 (`sphere_dim_eq_of_homotopyEquiv`, `sphere_homology_vanish`,
48 `sphere_top_ne_zero`).
492. `AlexanderLinkingBridge` assembly in `PublicSpine.lean`, replacing the
50 S¹-cohomology axiom of `Foundation/DimensionForcing.lean`
51 (`linking_requires_D3`).
52
53Load-bearing tricks documented for reuse: the `amb` ambient-coordinate
54abbrev (subtype-of-`TopCat.of` coercion bridge; plain `↑` coercions fail
55to elaborate on `↥(Sph n)`), the `esp0_ext`/`esp1_ext` coordinatewise
56extensionality helpers (raw `PiLp.ext` + `fin_cases` produces
57un-rewritable `⟨0, ⋯⟩` indices), and the polar-coordinates route to the
58equator homotopy equivalence (no hand-rolled normalization homotopy:
59stereographic ∘ `homeomorphUnitSphereProd` ∘ collapse `Ioi 0`).
60
61## Instance-diamond note (load-bearing, inherited from layers 4-5)
62
63For `R = ℤ` every `ModuleCat ℤ` carrier has two `Module ℤ` instances
64(`isModule` and `AddCommGroup.toIntModule`), propositionally but not
65definitionally equal, and synthesis prefers the generic one. This file
66deprioritizes `AddCommGroup.toIntModule` and `SubNegMonoid.toZSMul`
67locally, matching layers 1-5.
68-/
69import Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
70import IndisputableMonolith.Foundation.SingularSphere
71
72namespace IndisputableMonolith
73namespace Foundation
74namespace SingularSphereGeometry
75
76open CategoryTheory Category Limits AlgebraicTopology Simplicial Opposite
77open SingularPrism SingularSubdivision SingularMayerVietoris SingularSphere
78open Metric Set
79
80attribute [local instance 10] Classical.decEq
81
82/- See the instance-diamond note in the module header. -/
83attribute [local instance 0] AddCommGroup.toIntModule
84attribute [local instance 0] SubNegMonoid.toZSMul
85
86/-! ## Step 1: the sphere model, poles, and the open cover -/
87
88/-- The ambient Euclidean space of `Sⁿ`. -/
89noncomputable abbrev Esp (n : ℕ) : Type := EuclideanSpace ℝ (Fin (n + 1))
90
91/-- The `n`-sphere as a topological space: the unit sphere in
92`EuclideanSpace ℝ (Fin (n+1))`. -/
93noncomputable def Sph (n : ℕ) : TopCat.{0} :=
94 TopCat.of (sphere (0 : Esp n) 1)
95
96/-- The north-pole vector: the last standard basis vector. -/
97noncomputable def northV (n : ℕ) : Esp n :=
98 EuclideanSpace.single (Fin.last n) 1
99
100lemma norm_northV (n : ℕ) : ‖northV n‖ = 1 := by
101 rw [northV, EuclideanSpace.norm_single, norm_one]
102
103/-- The north pole, as a point of the sphere. -/
104noncomputable def northP (n : ℕ) : sphere (0 : Esp n) 1 :=
105 ⟨northV n, by rw [mem_sphere_zero_iff_norm]; exact norm_northV n⟩
106
107/-- The south pole, as a point of the sphere. -/
108noncomputable def southP (n : ℕ) : sphere (0 : Esp n) 1 := -northP n
109
110lemma northP_ne_southP (n : ℕ) : northP n ≠ southP n := by
111 intro h
112 have h1 : (northP n : Esp n) = -(northP n : Esp n) := by
113 calc (northP n : Esp n) = (southP n : Esp n) := congrArg _ h
114 _ = -(northP n : Esp n) := coe_neg_sphere (northP n)
115 have h2 : (northP n : Esp n) = 0 := by
116 have hsum : (northP n : Esp n) + (northP n : Esp n) = 0 := by
117 nth_rewrite 2 [h1]
118 exact add_neg_cancel _
119 have h2' : (2 : ℝ) • (northP n : Esp n) = 0 := by
120 rw [two_smul]
121 exact hsum
122 rcases smul_eq_zero.mp h2' with h | h
123 · exact absurd h (by norm_num)
124 · exact h
125 have h3 : ‖(northP n : Esp n)‖ = 1 := norm_eq_of_mem_sphere (northP n)
126 rw [h2, norm_zero] at h3
127 exact zero_ne_one h3
128
129/-- The subtype topology of `Sph n` is the metric sphere topology
130(instance bridge across `TopCat.of`). -/
131instance (n : ℕ) : T1Space ↥(Sph n) :=
132 inferInstanceAs (T1Space (sphere (0 : Esp n) 1))
133
134/-- The sphere minus the south pole. -/
135noncomputable def coverU (n : ℕ) : Set ↥(Sph n) := {southP n}ᶜ
136
137/-- The sphere minus the north pole. -/
138noncomputable def coverV (n : ℕ) : Set ↥(Sph n) := {northP n}ᶜ
139
140lemma isOpen_coverU (n : ℕ) : IsOpen (coverU n) := isOpen_compl_singleton
141
142lemma isOpen_coverV (n : ℕ) : IsOpen (coverV n) := isOpen_compl_singleton
143
144lemma coverU_union_coverV (n : ℕ) : coverU n ∪ coverV n = Set.univ := by
145 rw [Set.eq_univ_iff_forall]
146 intro x
147 by_cases h : x = southP n
148 · right
149 intro hx
150 rw [Set.mem_singleton_iff] at hx
151 exact northP_ne_southP n (hx.symm.trans h)
152 · left
153 exact h
154
155/-! ## Step 1: contractibility of the punctured sphere -/
156
157/-- **The punctured sphere is contractible** (any sphere, any removed
158point): stereographic projection is a homeomorphism from the complement
159of a point onto the orthogonal hyperplane, which is a real topological
160vector space and hence contractible. -/
161theorem contractibleSpace_compl_singleton_sphere {E : Type}
162 [NormedAddCommGroup E] [InnerProductSpace ℝ E]
163 (p : sphere (0 : E) 1) :
164 ContractibleSpace ↥(({p}ᶜ : Set (sphere (0 : E) 1))) := by
165 have hp : ‖(p : E)‖ = 1 := norm_eq_of_mem_sphere p
166 have hsrc : ({p}ᶜ : Set (sphere (0 : E) 1)) = (stereographic hp).source := rfl
167 have e1 : ↥(({p}ᶜ : Set (sphere (0 : E) 1))) ≃ₜ ↥((stereographic hp).source) :=
168 Homeomorph.setCongr hsrc
169 have e2 : ↥((stereographic hp).source) ≃ₜ ↥((stereographic hp).target) :=
170 (stereographic hp).toHomeomorphSourceTarget
171 have e3 : ↥((stereographic hp).target) ≃ₜ (ℝ ∙ (p : E))ᗮ :=
172 (Homeomorph.setCongr (stereographic_target hp)).trans
173 (Homeomorph.Set.univ _)
174 exact ((e1.trans e2).trans e3).contractibleSpace
175
176instance contractible_coverU (n : ℕ) : ContractibleSpace ↥(coverU n) :=
177 contractibleSpace_compl_singleton_sphere (southP n)
178
179instance contractible_coverV (n : ℕ) : ContractibleSpace ↥(coverV n) :=
180 contractibleSpace_compl_singleton_sphere (northP n)
181
182/-! ## Step 2: the homotopy type of the intersection -/
183
184/-- The orthogonal hyperplane at the north pole. -/
185noncomputable abbrev Hyp (n : ℕ) : Type := ((ℝ ∙ (northV n))ᗮ : Submodule ℝ (Esp n))
186
187lemma mem_inter_iff (n : ℕ) (x : ↥(Sph n)) :
188 x ∈ coverU n ∩ coverV n ↔ x ≠ southP n ∧ x ≠ northP n := by
189 constructor
190 · rintro ⟨hU, hV⟩
191 exact ⟨hU, hV⟩
192 · rintro ⟨hS, hN⟩
193 exact ⟨hS, hN⟩
194
195/-- Stereographic projection at the north pole restricts to a homeomorphism
196from the doubly punctured sphere onto the punctured hyperplane (the south
197pole goes to the origin). -/
198noncomputable def interHomeoPunctured (n : ℕ) :
199 ↥(coverU n ∩ coverV n) ≃ₜ ↥(({0}ᶜ : Set (Hyp n))) := by
200 have hnv : ‖northV n‖ = 1 := norm_northV n
201 have hsource : ∀ y : ↥(Sph n), y ≠ northP n →
202 y ∈ (stereographic hnv).source := by
203 intro y hy
204 show y ∈ ({(⟨northV n, _⟩ : sphere (0 : Esp n) 1)}ᶜ : Set _)
205 exact hy
206 have hst_south : stereographic hnv (southP n) = 0 :=
207 stereographic_apply_neg (northP n)
208 refine Homeomorph.mk (Equiv.mk ?_ ?_ ?_ ?_) ?_ ?_
209 · -- forward map
210 refine fun x => ⟨stereographic hnv x.1, ?_⟩
211 obtain ⟨hS, hN⟩ := (mem_inter_iff n x.1).mp x.2
212 intro h0
213 apply hS
214 refine (stereographic hnv).injOn (hsource x.1 hN)
215 (hsource (southP n) (fun h => northP_ne_southP n h.symm)) ?_
216 rw [hst_south]
217 exact h0
218 · -- inverse map
219 refine fun y => ⟨(stereographic hnv).symm y.1, ?_⟩
220 have hmem : (stereographic hnv).symm y.1 ∈ (stereographic hnv).source :=
221 (stereographic hnv).map_target (by
222 rw [stereographic_target]; exact Set.mem_univ _)
223 refine (mem_inter_iff n _).mpr ⟨?_, hmem⟩
224 intro hS
225 apply y.2
226 have := (stereographic hnv).right_inv (x := y.1) (by
227 rw [stereographic_target]; exact Set.mem_univ _)
228 rw [← this, hS, hst_south]
229 rfl
230 · -- left inverse
231 intro x
232 obtain ⟨_, hN⟩ := (mem_inter_iff n x.1).mp x.2
233 exact Subtype.ext (Subtype.ext (congrArg Subtype.val
234 ((stereographic hnv).left_inv (hsource x.1 hN))))
235 · -- right inverse
236 intro y
237 exact Subtype.ext ((stereographic hnv).right_inv (x := y.1) (by
238 rw [stereographic_target]; exact Set.mem_univ _))
239 · -- continuity, forward
240 refine Continuous.subtype_mk ?_ _
241 refine ContinuousOn.comp_continuous
242 (stereographic hnv).continuousOn continuous_subtype_val ?_
243 intro x
244 exact hsource x.1 ((mem_inter_iff n x.1).mp x.2).2
245 · -- continuity, inverse
246 refine Continuous.subtype_mk ?_ _
247 refine ContinuousOn.comp_continuous
248 (stereographic hnv).continuousOn_symm continuous_subtype_val ?_
249 intro y
250 rw [stereographic_target]
251 exact Set.mem_univ _
252
253/-- The punctured hyperplane in polar coordinates:
254`Hyp n \ {0} ≃ₜ sphere(Hyp n) × (0, ∞)`. -/
255noncomputable def puncturedPolar (n : ℕ) :
256 ↥(({0}ᶜ : Set (Hyp n))) ≃ₜ
257 (↥(sphere (0 : Hyp n) 1) × ↥(Ioi (0 : ℝ))) :=
258 homeomorphUnitSphereProd (Hyp n)
259
260/-- A linear isometry equivalence restricts to a homeomorphism of unit
261spheres. -/
262noncomputable def sphereHomeoOfLinearIsometryEquiv {F G : Type}
263 [NormedAddCommGroup F] [NormedAddCommGroup G]
264 [NormedSpace ℝ F] [NormedSpace ℝ G] (e : F ≃ₗᵢ[ℝ] G) :
265 ↥(sphere (0 : F) 1) ≃ₜ ↥(sphere (0 : G) 1) :=
266 e.toHomeomorph.subtype (fun x => by
267 rw [mem_sphere_zero_iff_norm, mem_sphere_zero_iff_norm]
268 exact (congrArg (· = 1) (e.norm_map x)).symm.to_iff)
269
270/-- The finrank fact for the ambient space, in the shape
271`fromOrthogonalSpanSingleton` wants. -/
272lemma fact_finrank_esp (n : ℕ) :
273 Fact (Module.finrank ℝ (Esp (n + 1)) = n + 1 + 1) :=
274 ⟨finrank_euclideanSpace_fin⟩
275
276/-- The north-pole hyperplane of `Sⁿ⁺¹` is isometric to `EuclideanSpace ℝ
277(Fin (n+1))`, the ambient space of `Sⁿ`. -/
278noncomputable def hypIsometry (n : ℕ) : Hyp (n + 1) ≃ₗᵢ[ℝ] Esp n :=
279 haveI : Fact (Module.finrank ℝ (Esp (n + 1)) = n + 1 + 1) :=
280 fact_finrank_esp n
281 (OrthonormalBasis.fromOrthogonalSpanSingleton (𝕜 := ℝ) (n + 1)
282 (fun h => one_ne_zero (by rw [← norm_northV (n + 1), h, norm_zero]))).repr
283
284instance : ContractibleSpace ↥(Ioi (0 : ℝ)) :=
285 (convex_Ioi (0 : ℝ)).contractibleSpace ⟨1, Set.mem_Ioi.mpr one_pos⟩
286
287/-- Collapsing a contractible factor is a homotopy equivalence. -/
288noncomputable def hequivProdContractible (Z C : Type)
289 [TopologicalSpace Z] [TopologicalSpace C] [ContractibleSpace C] :
290 ContinuousMap.HomotopyEquiv (Z × C) Z :=
291 ((ContinuousMap.HomotopyEquiv.refl Z).prodCongr
292 (ContractibleSpace.hequiv_unit C).some).trans
293 (Homeomorph.prodUnique Z Unit).toHomotopyEquiv
294
295/-- **Step 2.** The intersection of the two punctured-sphere covers of
296`Sⁿ⁺¹` is homotopy equivalent to `Sⁿ`. -/
297noncomputable def interHomotopyEquiv (n : ℕ) :
298 ContinuousMap.HomotopyEquiv
299 ↥(coverU (n + 1) ∩ coverV (n + 1)) ↥(Sph n) :=
300 (((interHomeoPunctured (n + 1)).trans
301 ((puncturedPolar (n + 1)).trans
302 ((sphereHomeoOfLinearIsometryEquiv (hypIsometry n)).prodCongr
303 (Homeomorph.refl ↥(Ioi (0 : ℝ)))))).toHomotopyEquiv).trans
304 (hequivProdContractible ↥(sphere (0 : Esp n) 1) ↥(Ioi (0 : ℝ)))
305
306/-! ## Step 3: the suspension isomorphism -/
307
308/-- Homotopy-equivalence isomorphism on `Hgrp` (retyped from layer 1). -/
309noncomputable def hgrpIso {X Y : TopCat.{0}}
310 (h : ContinuousMap.HomotopyEquiv X Y) (k : ℕ) : Hgrp X k ≅ Hgrp Y k :=
311 homotopyEquiv_homology_iso h k
312
313/-- **The suspension isomorphism** `H_{k+2}(Sⁿ⁺¹) ≅ H_{k+1}(Sⁿ)`: the
314Mayer-Vietoris connecting map for the two-punctured-sphere cover, followed
315by the homotopy equivalence of the intersection with the equator sphere. -/
316noncomputable def suspensionIso (n k : ℕ) :
317 Hgrp (Sph (n + 1)) (k + 2) ≅ Hgrp (Sph n) (k + 1) :=
318 haveI : IsIso (mvδ (isOpen_coverU (n + 1)) (isOpen_coverV (n + 1))
319 (coverU_union_coverV (n + 1)) (k + 1)) :=
320 isIso_mvδ_of_contractible _ _ _ k
321 asIso (mvδ (isOpen_coverU (n + 1)) (isOpen_coverV (n + 1))
322 (coverU_union_coverV (n + 1)) (k + 1)) ≪≫
323 hgrpIso (interHomotopyEquiv n) (k + 1)
324
325/-! ## Step 3: the base case `S⁰` -/
326
327/-- The ambient coordinates of a sphere point (coercion helper across
328`TopCat.of`). -/
329noncomputable abbrev amb {n : ℕ} (x : ↥(Sph n)) : Esp n := x.1
330
331lemma norm_amb {n : ℕ} (x : ↥(Sph n)) : ‖amb x‖ = 1 :=
332 norm_eq_of_mem_sphere x
333
334lemma amb_injective {n : ℕ} : Function.Injective (amb (n := n)) :=
335 fun _ _ h => Subtype.ext h
336
337/-- Coordinatewise extensionality in `Esp 0`. -/
338lemma esp0_ext {a b : Esp 0} (h0 : a 0 = b 0) : a = b := by
339 apply PiLp.ext
340 intro i
341 have hi : i = 0 := Fin.ext (by omega)
342 rw [hi]
343 exact h0
344
345/-- Coordinatewise extensionality in `Esp 1`. -/
346lemma esp1_ext {a b : Esp 1} (h0 : a 0 = b 0) (h1 : a 1 = b 1) : a = b := by
347 apply PiLp.ext
348 intro i
349 refine Fin.cases h0 (fun j => ?_) i
350 have hj : j = 0 := Fin.ext (by omega)
351 rw [hj, show (0 : Fin 1).succ = (1 : Fin 2) from by decide]
352 exact h1
353
354lemma northV_ne_zero (n : ℕ) : northV n ≠ 0 := fun h =>
355 one_ne_zero (by rw [← norm_northV n, h, norm_zero])
356
357lemma abs_eq_one_of_sq_eq_one {t : ℝ} (h : t ^ 2 = 1) : |t| = 1 := by
358 have h3 : (|t| - 1) * (|t| + 1) = 0 := by
359 have : |t| ^ 2 = 1 := by rw [sq_abs]; exact h
360 nlinarith [this]
361 rcases mul_eq_zero.mp h3 with h4 | h4
362 · linarith
363 · have := abs_nonneg t
364 linarith
365
366lemma amb_southP (n : ℕ) : amb (southP n : sphere (0 : Esp n) 1) = -(northV n) :=
367 coe_neg_sphere (northP n)
368
369/-- A point of `S⁰` is one of the two poles. -/
370lemma sph0_eq_pole (x : ↥(Sph 0)) : x = northP 0 ∨ x = southP 0 := by
371 have hx : ‖amb x‖ = 1 := norm_amb x
372 have hsq : amb x 0 ^ 2 = 1 := by
373 have hs := EuclideanSpace.norm_sq_eq (amb x)
374 rw [hx, Fin.sum_univ_one, Real.norm_eq_abs, sq_abs] at hs
375 linarith [hs]
376 have habs : |amb x 0| = 1 := abs_eq_one_of_sq_eq_one hsq
377 have hlast : (0 : Fin 1) = Fin.last 0 := by decide
378 rcases (abs_eq zero_le_one).mp habs with h | h
379 · left
380 apply amb_injective
381 apply esp0_ext
382 rw [h]
383 show (1 : ℝ) = northV 0 0
384 rw [northV, EuclideanSpace.single_apply, if_pos hlast]
385 · right
386 apply amb_injective
387 rw [amb_southP 0]
388 apply esp0_ext
389 rw [h]
390 show (-1 : ℝ) = -(northV 0 0)
391 rw [northV, EuclideanSpace.single_apply, if_pos hlast]
392
393open Classical in
394instance : Finite ↥(Sph 0) := by
395 refine Finite.of_injective
396 (fun x : ↥(Sph 0) => decide (x = northP 0)) ?_
397 intro x y hxy
398 dsimp only at hxy
399 have hiff : (x = northP 0) ↔ (y = northP 0) := decide_eq_decide.mp hxy
400 rcases sph0_eq_pole x with hx | hx <;> rcases sph0_eq_pole y with hy | hy
401 · rw [hx, hy]
402 · exact absurd ((hiff.mp hx).symm.trans hy) (northP_ne_southP 0)
403 · exact absurd ((hiff.mpr hy).symm.trans hx) (northP_ne_southP 0)
404 · rw [hx, hy]
405
406instance : DiscreteTopology ↥(Sph 0) := Finite.instDiscreteTopology
407
408/-- **Base case.** All positive-degree homology of `S⁰` vanishes. -/
409lemma isZero_sph0 {k : ℕ} (hk : k ≠ 0) : IsZero (Hgrp (Sph 0) k) :=
410 isZero_homology_of_totallyDisconnected (Sph 0) hk
411
412/-! ## Step 3: path-connectedness of the intersection in dimension `≥ 2` -/
413
414lemma finrank_hyp (n : ℕ) : Module.finrank ℝ (Hyp (n + 1)) = n + 1 :=
415 haveI : Fact (Module.finrank ℝ (Esp (n + 1)) = n + 1 + 1) :=
416 fact_finrank_esp n
417 Submodule.finrank_orthogonal_span_singleton (northV_ne_zero (n + 1))
418
419lemma one_lt_rank_hyp (n : ℕ) : 1 < Module.rank ℝ (Hyp (n + 2)) := by
420 have hfr : Module.finrank ℝ (Hyp (n + 2)) = n + 2 := finrank_hyp (n + 1)
421 rw [← Module.finrank_eq_rank, hfr]
422 exact_mod_cast (by omega : 1 < n + 2)
423
424instance pathConnected_inter (n : ℕ) :
425 PathConnectedSpace ↥(coverU (n + 2) ∩ coverV (n + 2)) := by
426 have h1 : IsPathConnected ({0}ᶜ : Set (Hyp (n + 2))) :=
427 isPathConnected_compl_singleton_of_one_lt_rank (one_lt_rank_hyp n) 0
428 haveI : PathConnectedSpace ↥(({0}ᶜ : Set (Hyp (n + 2)))) :=
429 isPathConnected_iff_pathConnectedSpace.mp h1
430 exact (interHomeoPunctured (n + 2)).symm.surjective.pathConnectedSpace
431 (interHomeoPunctured (n + 2)).symm.continuous
432
433/-! ## Step 3: the vanishing induction -/
434
435/-- **Stage D vanishing.** `H_k(Sⁿ) = 0` for `1 ≤ k`, `k ≠ n`. -/
436theorem sphere_homology_vanish :
437 ∀ n k : ℕ, 1 ≤ k → k ≠ n → IsZero (Hgrp (Sph n) k) := by
438 intro n
439 induction n with
440 | zero =>
441 intro k hk _
442 exact isZero_sph0 (by omega)
443 | succ n ih =>
444 intro k hk hkn
445 match k, hk with
446 | 1, _ =>
447 have hn : n ≠ 0 := by omega
448 obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
449 exact isZero_h1_of_contractible (isOpen_coverU (m + 2))
450 (isOpen_coverV (m + 2)) (coverU_union_coverV (m + 2))
451 | (k + 2), _ =>
452 exact (ih (k + 1) (by omega) (by omega)).of_iso (suspensionIso n k)
453
454/-! ## Step 3: non-vanishing of `H₁(S¹)` -/
455
456section CircleTop
457
458/-- The east point of the circle. -/
459noncomputable def eastP : sphere (0 : Esp 1) 1 :=
460 ⟨EuclideanSpace.single 0 1, by
461 rw [mem_sphere_zero_iff_norm, EuclideanSpace.norm_single, norm_one]⟩
462
463/-- The west point of the circle. -/
464noncomputable def westP : sphere (0 : Esp 1) 1 := -eastP
465
466lemma amb_eastP_zero : amb (eastP : ↥(Sph 1)) 0 = 1 := by
467 show EuclideanSpace.single (0 : Fin 2) (1 : ℝ) 0 = 1
468 rw [EuclideanSpace.single_apply, if_pos rfl]
469
470lemma amb_westP_zero : amb (westP : ↥(Sph 1)) 0 = -1 := by
471 have hc : amb (westP : ↥(Sph 1)) =
472 -(EuclideanSpace.single (0 : Fin 2) (1 : ℝ)) := coe_neg_sphere eastP
473 rw [hc, show (-(EuclideanSpace.single (0 : Fin 2) (1 : ℝ))) 0 =
474 -(EuclideanSpace.single (0 : Fin 2) (1 : ℝ) 0) from rfl,
475 EuclideanSpace.single_apply, if_pos rfl]
476
477lemma northV_zero : northV 1 0 = 0 := by
478 rw [northV, EuclideanSpace.single_apply, if_neg (by decide)]
479
480lemma amb_northP_zero : amb (northP 1 : ↥(Sph 1)) 0 = 0 := northV_zero
481
482lemma amb_southP_zero : amb (southP 1 : ↥(Sph 1)) 0 = 0 := by
483 rw [show amb (southP 1 : ↥(Sph 1)) = -(northV 1) from amb_southP 1,
484 show (-(northV 1)) 0 = -(northV 1 0) from rfl, northV_zero]
485 exact neg_zero
486
487/-- On the doubly punctured circle, the first coordinate never vanishes. -/
488lemma coord_zero_ne_zero (x : ↥(Sph 1)) (hS : x ≠ southP 1)
489 (hN : x ≠ northP 1) : amb x 0 ≠ 0 := by
490 intro h0
491 have hx : ‖amb x‖ = 1 := norm_amb x
492 have hsq : amb x 1 ^ 2 = 1 := by
493 have hs := EuclideanSpace.norm_sq_eq (amb x)
494 rw [hx, Fin.sum_univ_two, h0] at hs
495 simp only [Real.norm_eq_abs, sq_abs] at hs
496 linarith [hs]
497 have habs : |amb x 1| = 1 := abs_eq_one_of_sq_eq_one hsq
498 have hlast : (1 : Fin 2) = Fin.last 1 := by decide
499 rcases (abs_eq zero_le_one).mp habs with h | h
500 · apply hN
501 apply amb_injective
502 apply esp1_ext
503 · rw [h0]
504 show (0 : ℝ) = northV 1 0
505 rw [northV_zero]
506 · rw [h]
507 show (1 : ℝ) = northV 1 1
508 rw [northV, EuclideanSpace.single_apply, if_pos hlast]
509 · apply hS
510 apply amb_injective
511 rw [amb_southP 1]
512 apply esp1_ext
513 · rw [h0]
514 show (0 : ℝ) = -(northV 1 0)
515 rw [northV_zero, neg_zero]
516 · rw [h]
517 show (-1 : ℝ) = -(northV 1 1)
518 rw [northV, EuclideanSpace.single_apply, if_pos hlast]
519
520lemma eastP_mem_inter : (eastP : ↥(Sph 1)) ∈ coverU 1 ∩ coverV 1 := by
521 refine (mem_inter_iff 1 eastP).mpr ⟨?_, ?_⟩
522 · intro h
523 have h2 := amb_eastP_zero
524 rw [show amb (eastP : ↥(Sph 1)) = amb (southP 1 : ↥(Sph 1)) from
525 congrArg amb h, amb_southP_zero] at h2
526 exact one_ne_zero h2.symm
527 · intro h
528 have h2 := amb_eastP_zero
529 rw [show amb (eastP : ↥(Sph 1)) = amb (northP 1 : ↥(Sph 1)) from
530 congrArg amb h, amb_northP_zero] at h2
531 exact one_ne_zero h2.symm
532
533lemma westP_mem_inter : (westP : ↥(Sph 1)) ∈ coverU 1 ∩ coverV 1 := by
534 refine (mem_inter_iff 1 westP).mpr ⟨?_, ?_⟩
535 · intro h
536 have h2 := amb_westP_zero
537 rw [show amb (westP : ↥(Sph 1)) = amb (southP 1 : ↥(Sph 1)) from
538 congrArg amb h, amb_southP_zero] at h2
539 norm_num at h2
540 · intro h
541 have h2 := amb_westP_zero
542 rw [show amb (westP : ↥(Sph 1)) = amb (northP 1 : ↥(Sph 1)) from
543 congrArg amb h, amb_northP_zero] at h2
544 norm_num at h2
545
546/-- The doubly punctured circle, as a space. -/
547noncomputable abbrev Wc : TopCat.{0} :=
548 TopCat.of (coverU 1 ∩ coverV 1 : Set ↥(Sph 1))
549
550/-- The east point in the intersection. -/
551noncomputable def aW : ↥Wc := ⟨eastP, eastP_mem_inter⟩
552
553/-- The west point in the intersection. -/
554noncomputable def bW : ↥Wc := ⟨westP, westP_mem_inter⟩
555
556/-- The coordinate function on the doubly punctured circle. -/
557noncomputable def coordW (w : ↥Wc) : ℝ := amb (w.1 : ↥(Sph 1)) 0
558
559/-- The right (east) arc of the doubly punctured circle. -/
560noncomputable def arcA : Set ↥Wc := {w | 0 < coordW w}
561
562lemma continuous_coordW : Continuous coordW :=
563 (EuclideanSpace.proj (0 : Fin 2)).continuous.comp
564 (continuous_subtype_val.comp continuous_subtype_val)
565
566lemma isClopen_arcA : IsClopen arcA := by
567 constructor
568 · -- closed: on `Wc` the coordinate never vanishes, so `< 0`/`> 0` split
569 have heq : arcA = coordW ⁻¹' (Ici (0 : ℝ)) := by
570 apply Set.ext
571 intro w
572 obtain ⟨hS, hN⟩ := (mem_inter_iff 1 w.1).mp w.2
573 constructor
574 · intro hw
575 have hw' : (0 : ℝ) < coordW w := hw
576 exact le_of_lt hw'
577 · intro hw
578 have hw' : (0 : ℝ) ≤ coordW w := hw
579 show (0 : ℝ) < coordW w
580 exact lt_of_le_of_ne hw'
581 (fun h => coord_zero_ne_zero w.1 hS hN h.symm)
582 rw [heq]
583 exact isClosed_Ici.preimage continuous_coordW
584 · have heq : arcA = coordW ⁻¹' (Ioi (0 : ℝ)) := rfl
585 rw [heq]
586 exact isOpen_Ioi.preimage continuous_coordW
587
588lemma aW_mem_arcA : aW ∈ arcA := by
589 show (0 : ℝ) < coordW aW
590 rw [show coordW aW = amb (eastP : ↥(Sph 1)) 0 from rfl, amb_eastP_zero]
591 exact one_pos
592
593lemma bW_notMem_arcA : bW ∉ arcA := by
594 show ¬ (0 : ℝ) < coordW bW
595 rw [show coordW bW = amb (westP : ↥(Sph 1)) 0 from rfl, amb_westP_zero]
596 norm_num
597
598/-- The point-difference class in `H₀` of the two-arc intersection. -/
599noncomputable def diffClass : ModuleCat.of ℤ ℤ ⟶ Hgrp Wc 0 :=
600 ptH Wc aW - ptH Wc bW
601
602/-- The point-difference class pairs to `1` against the east-arc
603augmentation (hence is nonzero). -/
604lemma diffClass_pairing :
605 diffClass ≫ augH Wc arcA isClopen_arcA = 𝟙 (ModuleCat.of ℤ ℤ) := by
606 rw [diffClass, Preadditive.sub_comp, ptH_augH, ptH_augH,
607 if_pos aW_mem_arcA, if_neg bW_notMem_arcA, sub_zero]
608
609/-- The point-difference class dies in `H₀(U) ⊞ H₀(V)` (both points join
610inside each punctured circle). -/
611lemma diffClass_mvPair :
612 diffClass ≫ mvPair (coverU 1) (coverV 1) 0 = 0 := by
613 have hjU : ptH (TopCat.of (coverU 1))
614 ((mvInclU (coverU 1) (coverV 1)).hom aW) =
615 ptH (TopCat.of (coverU 1))
616 ((mvInclU (coverU 1) (coverV 1)).hom bW) :=
617 ptH_eq_of_joined (PathConnectedSpace.joined _ _)
618 have hjV : ptH (TopCat.of (coverV 1))
619 ((mvInclV (coverU 1) (coverV 1)).hom aW) =
620 ptH (TopCat.of (coverV 1))
621 ((mvInclV (coverU 1) (coverV 1)).hom bW) :=
622 ptH_eq_of_joined (PathConnectedSpace.joined _ _)
623 apply biprod.hom_ext
624 · rw [assoc, zero_comp, mvPair, biprod.lift_fst, diffClass,
625 Preadditive.sub_comp, ptH_natural, ptH_natural, hjU, sub_self]
626 · rw [assoc, zero_comp, mvPair, biprod.lift_snd, Preadditive.comp_neg,
627 diffClass, Preadditive.sub_comp, ptH_natural, ptH_natural, hjV,
628 sub_self, neg_zero]
629
630/-- **`H₁(S¹) ≠ 0`.** If it vanished, the Mayer-Vietoris connecting map
631out of it would be zero, and exactness would kill the point-difference
632class, contradicting its nonzero pairing. -/
633theorem h1_s1_ne_zero : ¬ IsZero (Hgrp (Sph 1) 1) := by
634 intro hZ
635 have hδ : mvδ (isOpen_coverU 1) (isOpen_coverV 1)
636 (coverU_union_coverV 1) 0 = 0 :=
637 hZ.eq_of_src _ _
638 have hex := mv_exact₁ (isOpen_coverU 1) (isOpen_coverV 1)
639 (coverU_union_coverV 1) 0
640 rw [ShortComplex.moduleCat_exact_iff] at hex
641 have hker : mvPair (coverU 1) (coverV 1) 0 (diffClass (1 : ℤ)) = 0 := by
642 rw [← ModuleCat.comp_apply, diffClass_mvPair, zeroApp]
643 obtain ⟨w, hw⟩ := hex (diffClass (1 : ℤ)) hker
644 have hw' : mvδ (isOpen_coverU 1) (isOpen_coverV 1)
645 (coverU_union_coverV 1) 0 w = diffClass (1 : ℤ) := hw
646 rw [hδ, zeroApp] at hw'
647 have h1 : augH Wc arcA isClopen_arcA (diffClass (1 : ℤ)) = (1 : ℤ) := by
648 rw [← ModuleCat.comp_apply, diffClass_pairing, ModuleCat.id_apply]
649 rw [← hw', map_zero] at h1
650 exact one_ne_zero h1.symm
651
652end CircleTop
653
654/-! ## Step 4: Stage D exports -/
655
656/-- **Stage D.** The top homology of `Sⁿ` does not vanish (`1 ≤ n`). -/
657theorem sphere_top_ne_zero : ∀ n : ℕ, 1 ≤ n → ¬ IsZero (Hgrp (Sph n) n) := by
658 intro n
659 induction n with
660 | zero => omega
661 | succ n ih =>
662 intro _
663 match n, ih with
664 | 0, _ => exact h1_s1_ne_zero
665 | (m + 1), ih =>
666 intro hZ
667 exact (ih (by omega)) (hZ.of_iso (suspensionIso (m + 1) m).symm)
668
669/-- **Stage D.** Spheres of different dimension are not homotopy
670equivalent. -/
671theorem spheres_not_homotopyEquivalent {m n : ℕ} (hmn : m ≠ n) :
672 IsEmpty (ContinuousMap.HomotopyEquiv ↥(Sph m) ↥(Sph n)) := by
673 constructor
674 intro e
675 rcases Nat.lt_or_ge m n with h | h
676 · exact sphere_top_ne_zero n (by omega)
677 ((sphere_homology_vanish m n (by omega) (by omega)).of_iso
678 (hgrpIso e n).symm)
679 · have h' : n < m := lt_of_le_of_ne h (fun hh => hmn hh.symm)
680 exact sphere_top_ne_zero m (by omega)
681 ((sphere_homology_vanish n m (by omega) (by omega)).of_iso
682 (hgrpIso e.symm m).symm)
683
684/-- Stage D, `Nonempty` form: homotopy-equivalent spheres have equal
685dimension. -/
686theorem sphere_dim_eq_of_homotopyEquiv {m n : ℕ}
687 (h : Nonempty (ContinuousMap.HomotopyEquiv ↥(Sph m) ↥(Sph n))) :
688 m = n := by
689 by_contra hmn
690 exact (spheres_not_homotopyEquivalent hmn).false h.some
691
692end SingularSphereGeometry
693end Foundation
694end IndisputableMonolith
695