IndisputableMonolith.Foundation.LinkingVanishingHighDim
IndisputableMonolith/Foundation/LinkingVanishingHighDim.lean · 630 lines · 43 declarations
show as:
view math explainer →
1/-
2Linking vanishing in high dimension (D = 2 and D ≥ 4): the Mayer-Vietoris
3reduction to the arc-complement acyclicity frontier.
4
5## What this file proves (0 sorry, 0 new axioms)
6
7Campaign P-d3link, final phase. The binder predicate
8(`PublicSpine.DetectsNontrivialLinking D`, restated verbatim below) asks for
9an embedded circle in `S^D` whose complement has nonvanishing first singular
10homology. The full refutation for `D ≠ 3` is Alexander duality for
11arbitrary (possibly wild) embedded circles. This file carries out the
12classical Mayer-Vietoris reduction (Hatcher 2B.1, circle case):
13
14* **Two-point complement** (`twoPointComplHEquiv`, `isZero_h2_twoPointCompl`):
15 for any two distinct points `p ≠ q` of `Sⁿ` (`n ≥ 1`), the complement
16 `Sⁿ \ {p, q}` is homotopy equivalent to `Sⁿ⁻¹` (stereographic projection at
17 `p`, a translation, and polar coordinates); hence `H₂(Sⁿ \ {p,q}) = 0`
18 whenever `n ≠ 3`.
19* **Semicircle arcs** (`arcMap`, `range_arcPlus/Minus`, …): the closed upper
20 and lower semicircles of `S¹` are ranges of explicit embeddings of the
21 unit interval meeting exactly in the east and west points.
22* **The Mayer-Vietoris step** (`isZero_h1_inter`): if `U, V` are open, cover,
23 `H₂(X) = 0` and `H₁(U) = H₁(V) = 0`, then `H₁(U ∩ V) = 0` (exactness of
24 the banked MV sequence at `H₁(U ∩ V)`).
25* **The reduction** (`isZero_h1_complement_of_embedding`,
26 `not_detects_of_arcAcyclic`, `forces_D3_of_arcAcyclic`): granting the
27 single remaining frontier `ArcComplementsAcyclic D` (every embedded arc in
28 `S^D` has `H₁`-acyclic complement — true for every `D`, classically by the
29 compact-support bisection argument), every embedded circle in `S^D`
30 (`D ≠ 3`) has `H₁`-acyclic complement, so the binder's `forces_D3` holds.
31
32## The precise remaining frontier
33
34`ArcComplementsAcyclic D` (below): for every topological embedding
35`a : [0,1] → S^D`, `H₁(S^D \ range a; ℤ) = 0`. This is NOT an axiom and NOT
36a sorry: it is a hypothesis parameter, to be discharged by the
37compact-support bisection argument (Hatcher 2B.1, arc case) on top of the
38banked Mayer-Vietoris layer. Everything else in the `forces_D3` chain is
39proved unconditionally here.
40
41## Instance-diamond note (load-bearing, inherited from layers 4-5b)
42
43For `R = ℤ` every `ModuleCat ℤ` carrier has two `Module ℤ` instances,
44propositionally but not definitionally equal, and synthesis prefers the
45generic one. This file deprioritizes `AddCommGroup.toIntModule` and
46`SubNegMonoid.toZSMul` locally, matching layers 1-5b.
47-/
48import IndisputableMonolith.Foundation.SingularSphereGeometry
49import IndisputableMonolith.Foundation.LinkingVanishingLowDim
50
51namespace IndisputableMonolith
52namespace Foundation
53namespace LinkingVanishingHighDim
54
55open CategoryTheory Category Limits AlgebraicTopology Simplicial
56open SingularPrism SingularSubdivision SingularMayerVietoris SingularSphere
57open SingularSphereGeometry
58open Metric Set
59
60attribute [local instance 10] Classical.decEq
61
62/- See the instance-diamond note in the module header. -/
63attribute [local instance 0] AddCommGroup.toIntModule
64attribute [local instance 0] SubNegMonoid.toZSMul
65
66/-! ## The binder predicate, restated verbatim -/
67
68/-- Verbatim restatement of `PublicSpine.linkingComplementH1`. -/
69noncomputable def linkingComplementH1 (D : ℕ)
70 (f : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} D)) : ModuleCat ℤ :=
71 ((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
72 (ModuleCat.of ℤ ℤ)).obj
73 (TopCat.of {x : TopCat.sphere.{0} D // x ∉ Set.range f})
74
75/-- Verbatim restatement of `PublicSpine.DetectsNontrivialLinking`. -/
76def DetectsNontrivialLinking (D : ℕ) : Prop :=
77 ∃ f : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} D),
78 Topology.IsEmbedding f ∧
79 ¬ CategoryTheory.Limits.IsZero (linkingComplementH1 D f)
80
81/-! ## The frontier: arc complements are `H₁`-acyclic -/
82
83/-- **The precisely-stated remaining frontier** (Hatcher 2B.1, arc case):
84every topological embedding of the unit interval into `S^D` has
85`H₁`-acyclic complement. Classically true for every `D` (compact-support
86bisection); this file consumes it as a hypothesis parameter and reduces
87`forces_D3` to it. -/
88def ArcComplementsAcyclic (D : ℕ) : Prop :=
89 ∀ a : C(unitInterval, ↥(Sph D)), Topology.IsEmbedding a →
90 CategoryTheory.Limits.IsZero
91 (Hgrp (TopCat.of {y : ↥(Sph D) // y ∉ Set.range a}) 1)
92
93/-! ## Semicircle arcs of the circle -/
94
95/-- The point of the plane with coordinates `(a, b)`. -/
96noncomputable def pt2 (a b : ℝ) : Esp 1 :=
97 WithLp.toLp 2 ![a, b]
98
99@[simp] lemma pt2_zero (a b : ℝ) : pt2 a b 0 = a := rfl
100
101@[simp] lemma pt2_one (a b : ℝ) : pt2 a b 1 = b := rfl
102
103lemma pt2_norm (a b : ℝ) : ‖pt2 a b‖ = Real.sqrt (a ^ 2 + b ^ 2) := by
104 rw [EuclideanSpace.norm_eq, Fin.sum_univ_two]
105 show Real.sqrt (‖a‖ ^ 2 + ‖b‖ ^ 2) = Real.sqrt (a ^ 2 + b ^ 2)
106 rw [Real.norm_eq_abs, Real.norm_eq_abs, sq_abs, sq_abs]
107
108/-- Membership of `(a, b)` in the unit circle from `a² + b² = 1`. -/
109lemma pt2_mem_sphere {a b : ℝ} (h : a ^ 2 + b ^ 2 = 1) :
110 pt2 a b ∈ sphere (0 : Esp 1) 1 := by
111 rw [mem_sphere_zero_iff_norm, pt2_norm, h, Real.sqrt_one]
112
113/-- Coordinates of a circle point satisfy the circle equation. -/
114lemma coord_sq_add_sq (z : ↥(Sph 1)) : amb z 0 ^ 2 + amb z 1 ^ 2 = 1 := by
115 have hs := EuclideanSpace.norm_sq_eq (amb z)
116 rw [norm_amb, one_pow, Fin.sum_univ_two] at hs
117 simpa only [Real.norm_eq_abs, sq_abs] using hs.symm
118
119/-- The first coordinate of a circle point lies in `[-1, 1]` (squared form). -/
120lemma sq_coord0_le_one (z : ↥(Sph 1)) : amb z 0 ^ 2 ≤ 1 := by
121 nlinarith [coord_sq_add_sq z, sq_nonneg (amb z 1)]
122
123/-- The semicircle arc: `t ↦ (1 - 2t, s·√(1 - (1-2t)²))`, where `s = ±1`
124selects the upper or lower semicircle. -/
125noncomputable def arcFun (s : ℝ) (hs : s ^ 2 = 1) (t : unitInterval) :
126 ↥(Sph 1) :=
127 ⟨pt2 (1 - 2 * (t : ℝ)) (s * Real.sqrt (1 - (1 - 2 * (t : ℝ)) ^ 2)), by
128 apply pt2_mem_sphere
129 have ht0 : (0 : ℝ) ≤ (t : ℝ) := t.2.1
130 have ht1 : (t : ℝ) ≤ 1 := t.2.2
131 have hle : (1 - 2 * (t : ℝ)) ^ 2 ≤ 1 := by nlinarith
132 rw [mul_pow, hs, one_mul, Real.sq_sqrt (by linarith)]
133 ring⟩
134
135lemma arcFun_coord0 (s : ℝ) (hs : s ^ 2 = 1) (t : unitInterval) :
136 amb (arcFun s hs t) 0 = 1 - 2 * (t : ℝ) := rfl
137
138lemma arcFun_coord1 (s : ℝ) (hs : s ^ 2 = 1) (t : unitInterval) :
139 amb (arcFun s hs t) 1 = s * Real.sqrt (1 - (1 - 2 * (t : ℝ)) ^ 2) := rfl
140
141lemma continuous_arcFun (s : ℝ) (hs : s ^ 2 = 1) :
142 Continuous (arcFun s hs) := by
143 apply Continuous.subtype_mk
144 apply (PiLp.continuous_toLp 2 _).comp
145 refine continuous_pi ?_
146 intro i
147 fin_cases i
148 · show Continuous fun t : unitInterval => (1 - 2 * (t : ℝ))
149 fun_prop
150 · show Continuous fun t : unitInterval =>
151 s * Real.sqrt (1 - (1 - 2 * (t : ℝ)) ^ 2)
152 fun_prop
153
154/-- The semicircle arc as a continuous map. -/
155noncomputable def arcMap (s : ℝ) (hs : s ^ 2 = 1) :
156 C(unitInterval, ↥(Sph 1)) :=
157 ⟨arcFun s hs, continuous_arcFun s hs⟩
158
159lemma arcMap_injective (s : ℝ) (hs : s ^ 2 = 1) :
160 Function.Injective (arcMap s hs) := by
161 intro t t' h
162 have h0 : amb (arcFun s hs t) 0 = amb (arcFun s hs t') 0 := by
163 rw [show arcFun s hs t = arcFun s hs t' from h]
164 rw [arcFun_coord0, arcFun_coord0] at h0
165 exact Subtype.ext (by linarith)
166
167lemma isEmbedding_arcMap (s : ℝ) (hs : s ^ 2 = 1) :
168 Topology.IsEmbedding (arcMap s hs) := by
169 haveI : T2Space ↥(Sph 1) :=
170 inferInstanceAs (T2Space ↥(sphere (0 : Esp 1) 1))
171 exact ((continuous_arcFun s hs).isClosedEmbedding
172 (arcMap_injective s hs)).isEmbedding
173
174/-- The upper semicircle arc. -/
175noncomputable def arcPlus : C(unitInterval, ↥(Sph 1)) :=
176 arcMap 1 (one_pow 2)
177
178/-- The lower semicircle arc. -/
179noncomputable def arcMinus : C(unitInterval, ↥(Sph 1)) :=
180 arcMap (-1) (neg_one_sq)
181
182lemma isEmbedding_arcPlus : Topology.IsEmbedding arcPlus :=
183 isEmbedding_arcMap 1 (one_pow 2)
184
185lemma isEmbedding_arcMinus : Topology.IsEmbedding arcMinus :=
186 isEmbedding_arcMap (-1) (neg_one_sq)
187
188/-- Preimage parameter for a point of the circle: `t = (1 - z₀)/2 ∈ [0,1]`. -/
189noncomputable def arcParam (z : ↥(Sph 1)) : unitInterval :=
190 ⟨(1 - amb z 0) / 2, by
191 constructor
192 · have h := sq_coord0_le_one z
193 have : amb z 0 ≤ 1 := by nlinarith
194 linarith
195 · have h := sq_coord0_le_one z
196 have : -1 ≤ amb z 0 := by nlinarith
197 linarith⟩
198
199lemma arcFun_arcParam (s : ℝ) (hs : s ^ 2 = 1) (z : ↥(Sph 1))
200 (hz : s * amb z 1 = |amb z 1|) :
201 arcFun s hs (arcParam z) = z := by
202 apply amb_injective
203 apply esp1_ext
204 · rw [arcFun_coord0]
205 show 1 - 2 * ((1 - amb z 0) / 2) = amb z 0
206 ring
207 · rw [arcFun_coord1]
208 have hcoord : 1 - (1 - 2 * ((arcParam z : ℝ))) ^ 2 = amb z 1 ^ 2 := by
209 show 1 - (1 - 2 * ((1 - amb z 0) / 2)) ^ 2 = amb z 1 ^ 2
210 have := coord_sq_add_sq z
211 nlinarith [coord_sq_add_sq z]
212 rw [hcoord, Real.sqrt_sq_eq_abs, ← hz]
213 have hs' : s * s = 1 := by nlinarith [hs]
214 calc s * (s * amb z 1) = (s * s) * amb z 1 := by ring
215 _ = amb z 1 := by rw [hs', one_mul]
216
217/-- The upper semicircle is the range of `arcPlus`. -/
218lemma range_arcPlus :
219 Set.range arcPlus = {z : ↥(Sph 1) | 0 ≤ amb z 1} := by
220 ext z
221 constructor
222 · rintro ⟨t, rfl⟩
223 show (0 : ℝ) ≤ amb (arcFun 1 (one_pow 2) t) 1
224 rw [arcFun_coord1, one_mul]
225 exact Real.sqrt_nonneg _
226 · intro hz
227 exact ⟨arcParam z, arcFun_arcParam 1 (one_pow 2) z
228 (by rw [one_mul, abs_of_nonneg hz])⟩
229
230/-- The lower semicircle is the range of `arcMinus`. -/
231lemma range_arcMinus :
232 Set.range arcMinus = {z : ↥(Sph 1) | amb z 1 ≤ 0} := by
233 ext z
234 constructor
235 · rintro ⟨t, rfl⟩
236 show amb (arcFun (-1) neg_one_sq t) 1 ≤ 0
237 rw [arcFun_coord1]
238 have := Real.sqrt_nonneg (1 - (1 - 2 * (t : ℝ)) ^ 2)
239 nlinarith
240 · intro hz
241 exact ⟨arcParam z, arcFun_arcParam (-1) neg_one_sq z
242 (by rw [abs_of_nonpos hz]; ring)⟩
243
244/-- The two semicircles cover the circle. -/
245lemma range_arcPlus_union_arcMinus :
246 Set.range arcPlus ∪ Set.range arcMinus = Set.univ := by
247 rw [range_arcPlus, range_arcMinus]
248 ext z
249 simp only [Set.mem_union, Set.mem_setOf_eq, Set.mem_univ, iff_true]
250 exact le_total 0 (amb z 1)
251
252/-- The two semicircles meet exactly in the east and west points. -/
253lemma range_arcPlus_inter_arcMinus :
254 Set.range arcPlus ∩ Set.range arcMinus =
255 {(eastP : ↥(Sph 1)), (westP : ↥(Sph 1))} := by
256 rw [range_arcPlus, range_arcMinus]
257 ext z
258 simp only [Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_insert_iff,
259 Set.mem_singleton_iff]
260 constructor
261 · rintro ⟨h1, h2⟩
262 have hz1 : amb z 1 = 0 := le_antisymm h2 h1
263 have hz0 : amb z 0 ^ 2 = 1 := by
264 have := coord_sq_add_sq z
265 nlinarith
266 have habs : |amb z 0| = 1 := abs_eq_one_of_sq_eq_one hz0
267 rcases (abs_eq zero_le_one).mp habs with h | h
268 · left
269 apply amb_injective
270 apply esp1_ext
271 · rw [h, amb_eastP_zero]
272 · rw [hz1]
273 show (0 : ℝ) = EuclideanSpace.single (0 : Fin 2) (1 : ℝ) 1
274 rw [EuclideanSpace.single_apply, if_neg (by decide)]
275 · right
276 apply amb_injective
277 apply esp1_ext
278 · rw [h, amb_westP_zero]
279 · rw [hz1]
280 have hc : amb (westP : ↥(Sph 1)) =
281 -(EuclideanSpace.single (0 : Fin 2) (1 : ℝ)) := coe_neg_sphere eastP
282 rw [hc, show (-(EuclideanSpace.single (0 : Fin 2) (1 : ℝ))) 1 =
283 -(EuclideanSpace.single (0 : Fin 2) (1 : ℝ) 1) from rfl,
284 EuclideanSpace.single_apply, if_neg (by decide), neg_zero]
285 · rintro (rfl | rfl)
286 · constructor
287 · rw [show amb (eastP : ↥(Sph 1)) 1 =
288 EuclideanSpace.single (0 : Fin 2) (1 : ℝ) 1 from rfl,
289 EuclideanSpace.single_apply, if_neg (by decide)]
290 · rw [show amb (eastP : ↥(Sph 1)) 1 =
291 EuclideanSpace.single (0 : Fin 2) (1 : ℝ) 1 from rfl,
292 EuclideanSpace.single_apply, if_neg (by decide)]
293 · have hw : amb (westP : ↥(Sph 1)) 1 = 0 := by
294 have hc : amb (westP : ↥(Sph 1)) =
295 -(EuclideanSpace.single (0 : Fin 2) (1 : ℝ)) := coe_neg_sphere eastP
296 rw [hc, show (-(EuclideanSpace.single (0 : Fin 2) (1 : ℝ))) 1 =
297 -(EuclideanSpace.single (0 : Fin 2) (1 : ℝ) 1) from rfl,
298 EuclideanSpace.single_apply, if_neg (by decide), neg_zero]
299 exact ⟨le_of_eq hw.symm, le_of_eq hw⟩
300
301lemma eastP_ne_westP : (eastP : ↥(Sph 1)) ≠ westP := by
302 intro h
303 have := congrArg (fun z : ↥(Sph 1) => amb z 0) h
304 simp only [amb_eastP_zero, amb_westP_zero] at this
305 norm_num at this
306
307/-! ## The two-point complement: `Sⁿ \ {p, q} ≃ₕ Sⁿ⁻¹` for arbitrary points -/
308
309/-- The orthogonal hyperplane at an arbitrary sphere point `p` is isometric
310to the ambient space one dimension down (generalizing `hypIsometry`, which
311is the `p = northP` case). -/
312noncomputable def perpIsometry (n : ℕ) (p : ↥(Sph (n + 1))) :
313 ((ℝ ∙ (amb p))ᗮ : Submodule ℝ (Esp (n + 1))) ≃ₗᵢ[ℝ] Esp n :=
314 haveI : Fact (Module.finrank ℝ (Esp (n + 1)) = n + 1 + 1) :=
315 fact_finrank_esp n
316 (OrthonormalBasis.fromOrthogonalSpanSingleton (𝕜 := ℝ) (n + 1)
317 (fun h => one_ne_zero (by rw [← norm_amb p, h, norm_zero]))).repr
318
319/-- `p` as the base point of its own stereographic chart. -/
320lemma stereographic_source_pt (n : ℕ) (p : ↥(Sph n)) (x : ↥(Sph n))
321 (hx : x ≠ p) : x ∈ (stereographic (norm_amb p)).source := by
322 rw [stereographic_source]
323 intro hmem
324 exact hx (hmem.trans (Subtype.ext rfl))
325
326/-- Stereographic projection at `p` restricts to a homeomorphism from the
327doubly punctured sphere `Sⁿ \ {p, q}` onto the hyperplane minus the image
328of `q` (generalizing `interHomeoPunctured` to arbitrary points). -/
329noncomputable def twoPunctHomeo (n : ℕ) (p q : ↥(Sph n)) (hqp : q ≠ p) :
330 ↥(({p, q} : Set ↥(Sph n))ᶜ) ≃ₜ
331 ↥(({stereographic (norm_amb p) q}ᶜ :
332 Set ((ℝ ∙ (amb p))ᗮ : Submodule ℝ (Esp n)))) := by
333 set φ := stereographic (norm_amb p) with hφ
334 have hsrc : ∀ x : ↥(Sph n), x ≠ p → x ∈ φ.source :=
335 fun x hx => stereographic_source_pt n p x hx
336 have htgt : ∀ z : ((ℝ ∙ (amb p))ᗮ : Submodule ℝ (Esp n)), z ∈ φ.target :=
337 fun z => by rw [hφ, stereographic_target]; exact Set.mem_univ z
338 have hmem_compl : ∀ x : ↥(Sph n), x ∈ ({p, q} : Set ↥(Sph n))ᶜ ↔
339 x ≠ p ∧ x ≠ q := by
340 intro x
341 rw [Set.mem_compl_iff, Set.mem_insert_iff, Set.mem_singleton_iff]
342 push_neg
343 exact Iff.rfl
344 refine Homeomorph.mk (Equiv.mk ?_ ?_ ?_ ?_) ?_ ?_
345 · -- forward map
346 refine fun x => ⟨φ x.1, ?_⟩
347 obtain ⟨hxp, hxq⟩ := (hmem_compl x.1).mp x.2
348 intro h0
349 exact hxq (φ.injOn (hsrc x.1 hxp) (hsrc q hqp) h0)
350 · -- inverse map
351 refine fun y => ⟨φ.symm y.1, ?_⟩
352 have hmem : φ.symm y.1 ∈ φ.source := φ.map_target (htgt y.1)
353 refine (hmem_compl _).mpr ⟨?_, ?_⟩
354 · intro hp0
355 have : φ.symm y.1 ∈ ({⟨amb p, by
356 rw [mem_sphere_zero_iff_norm]; exact norm_amb p⟩}ᶜ :
357 Set (sphere (0 : Esp n) 1)) := by
358 rw [← stereographic_source (norm_amb p)]
359 exact hmem
360 exact this (by rw [hp0]; exact Set.mem_singleton_iff.mpr (Subtype.ext rfl))
361 · intro hq0
362 apply y.2
363 have hri := φ.right_inv (x := y.1) (htgt y.1)
364 rw [Set.mem_singleton_iff, ← hri, hq0]
365 · -- left inverse
366 intro x
367 obtain ⟨hxp, _⟩ := (hmem_compl x.1).mp x.2
368 exact Subtype.ext (φ.left_inv (hsrc x.1 hxp))
369 · -- right inverse
370 intro y
371 exact Subtype.ext (φ.right_inv (x := y.1) (htgt y.1))
372 · -- continuity, forward
373 refine Continuous.subtype_mk ?_ _
374 refine ContinuousOn.comp_continuous φ.continuousOn continuous_subtype_val ?_
375 intro x
376 exact hsrc x.1 ((hmem_compl x.1).mp x.2).1
377 · -- continuity, inverse
378 refine Continuous.subtype_mk ?_ _
379 refine ContinuousOn.comp_continuous φ.continuousOn_symm
380 continuous_subtype_val ?_
381 intro y
382 exact htgt y.1
383
384/-- Translating a puncture to the origin: `F \ {y₀} ≃ₜ F \ {0}`. -/
385noncomputable def punctTranslateHomeo {F : Type} [NormedAddCommGroup F]
386 (y₀ : F) : ↥(({y₀}ᶜ : Set F)) ≃ₜ ↥(({0}ᶜ : Set F)) :=
387 (Homeomorph.subRight y₀).subtype (fun x => by
388 rw [Set.mem_compl_iff, Set.mem_compl_iff, Set.mem_singleton_iff,
389 Set.mem_singleton_iff]
390 exact (not_congr sub_eq_zero).symm.trans Iff.rfl)
391
392/-- **The two-point complement is homotopy equivalent to the equator
393sphere**: `Sⁿ⁺¹ \ {p, q} ≃ₕ Sⁿ` for any distinct `p, q` (stereographic
394projection at `p`, translation of the image of `q` to the origin, polar
395coordinates, and collapse of the ray factor). -/
396noncomputable def twoPointComplHEquiv (n : ℕ) (p q : ↥(Sph (n + 1)))
397 (hqp : q ≠ p) :
398 ContinuousMap.HomotopyEquiv
399 ↥(({p, q} : Set ↥(Sph (n + 1)))ᶜ) ↥(Sph n) :=
400 (((twoPunctHomeo (n + 1) p q hqp).trans
401 ((punctTranslateHomeo (stereographic (norm_amb p) q)).trans
402 ((homeomorphUnitSphereProd _).trans
403 ((sphereHomeoOfLinearIsometryEquiv (perpIsometry n p)).prodCongr
404 (Homeomorph.refl ↥(Ioi (0 : ℝ))))))).toHomotopyEquiv).trans
405 (hequivProdContractible ↥(sphere (0 : Esp n) 1) ↥(Ioi (0 : ℝ)))
406
407/-- `H₂(Sⁿ \ {p, q}) = 0` for `n ≥ 1`, `n ≠ 3`, and any distinct points. -/
408theorem isZero_h2_twoPointCompl {n : ℕ} (hn : 1 ≤ n) (hn3 : n ≠ 3)
409 (p q : ↥(Sph n)) (hqp : q ≠ p) :
410 IsZero (Hgrp (TopCat.of ↥(({p, q} : Set ↥(Sph n))ᶜ)) 2) := by
411 obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (by omega : n ≠ 0)
412 exact (sphere_homology_vanish m 2 one_le_two (by omega)).of_iso
413 (hgrpIso (twoPointComplHEquiv m p q hqp) 2)
414
415/-! ## The Mayer-Vietoris step -/
416
417/-- **MV middle vanishing**: open cover `U ∪ V = X` with `H₂(X) = 0` and
418`H₁(U) = H₁(V) = 0` forces `H₁(U ∩ V) = 0` (exactness of the banked
419Mayer-Vietoris sequence at `H₁(U ∩ V)`). -/
420theorem isZero_h1_inter {X : TopCat.{0}} {U V : Set X}
421 (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
422 (hX2 : IsZero (Hgrp X 2))
423 (hU1 : IsZero (Hgrp (TopCat.of U) 1))
424 (hV1 : IsZero (Hgrp (TopCat.of V) 1)) :
425 IsZero (Hgrp (TopCat.of (U ∩ V : Set X)) 1) :=
426 (mv_exact₁ hU hV hUV 1).isZero_X₂
427 (hX2.eq_of_src _ _)
428 (((biprod_isZero_iff _ _).mpr ⟨hU1, hV1⟩).eq_of_tgt _ _)
429
430/-! ## Subtype flattening -/
431
432/-- Inside `W \ E`, the locus avoiding `K ⊇ E` is homeomorphic to the locus
433of `W` avoiding `K` (flattening a subtype of a subtype). -/
434noncomputable def flattenComplHomeo {W : TopCat.{0}} (E K : Set ↥W)
435 (hEK : E ⊆ K) :
436 ↥({x : ↥(TopCat.of (Eᶜ : Set ↥W)) | x.1 ∉ K}) ≃ₜ
437 {y : ↥W // y ∉ K} where
438 toFun x := ⟨x.1.1, x.2⟩
439 invFun y := ⟨⟨y.1, fun hE => y.2 (hEK hE)⟩, y.2⟩
440 left_inv _ := Subtype.ext (Subtype.ext rfl)
441 right_inv _ := rfl
442 continuous_toFun :=
443 Continuous.subtype_mk (continuous_subtype_val.comp continuous_subtype_val) _
444 continuous_invFun :=
445 Continuous.subtype_mk (Continuous.subtype_mk continuous_subtype_val _) _
446
447/-! ## The reduction: circle complements from arc complements -/
448
449/-- **Abstract two-arc Mayer-Vietoris**: two closed sets `KP, KM` in a space
450`W`, with `H₂(W \ (KP ∩ KM)) = 0` and `H₁`-acyclic complements, have
451`H₁`-acyclic union complement. -/
452theorem isZero_h1_unionCompl {W : TopCat.{0}} (KP KM : Set ↥W)
453 (hKPc : IsClosed KP) (hKMc : IsClosed KM)
454 (hX2 : IsZero (Hgrp (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) 2))
455 (hP1 : IsZero (Hgrp (TopCat.of {y : ↥W // y ∉ KP}) 1))
456 (hM1 : IsZero (Hgrp (TopCat.of {y : ↥W // y ∉ KM}) 1)) :
457 IsZero (Hgrp (TopCat.of {y : ↥W // y ∉ KP ∪ KM}) 1) := by
458 -- the MV cover of `W \ (KP ∩ KM)` by the complements of the two arcs
459 have hUopen : IsOpen
460 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KP} :
461 Set (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W))) :=
462 hKPc.isOpen_compl.preimage continuous_subtype_val
463 have hVopen : IsOpen
464 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KM} :
465 Set (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W))) :=
466 hKMc.isOpen_compl.preimage continuous_subtype_val
467 have hUVcover :
468 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KP} :
469 Set (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W))) ∪
470 {x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KM} = Set.univ := by
471 rw [Set.eq_univ_iff_forall]
472 intro x
473 by_cases hxP : x.1 ∈ KP
474 · right
475 intro hxM
476 exact x.2 ⟨hxP, hxM⟩
477 · left
478 exact hxP
479 -- H₁ of the pieces, flattened to the arc complements
480 have hU1 : IsZero (Hgrp (TopCat.of
481 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KP} :
482 Set (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)))) 1) :=
483 hP1.of_iso (hgrpIso
484 (flattenComplHomeo (KP ∩ KM) KP Set.inter_subset_left).toHomotopyEquiv 1)
485 have hV1 : IsZero (Hgrp (TopCat.of
486 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KM} :
487 Set (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)))) 1) :=
488 hM1.of_iso (hgrpIso
489 (flattenComplHomeo (KP ∩ KM) KM Set.inter_subset_right).toHomotopyEquiv 1)
490 -- MV middle vanishing, then flatten the intersection
491 have hmid := isZero_h1_inter hUopen hVopen hUVcover hX2 hU1 hV1
492 have hUVeq :
493 (({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KP} :
494 Set (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W))) ∩
495 {x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KM}) =
496 {x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KP ∪ KM} := by
497 ext x
498 rw [Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_setOf_eq,
499 Set.mem_setOf_eq]
500 constructor
501 · rintro ⟨h1, h2⟩ (h | h)
502 · exact h1 h
503 · exact h2 h
504 · intro h
505 exact ⟨fun hP => h (Set.mem_union_left _ hP),
506 fun hM => h (Set.mem_union_right _ hM)⟩
507 rw [hUVeq] at hmid
508 exact hmid.of_iso (hgrpIso
509 (flattenComplHomeo (KP ∩ KM) (KP ∪ KM)
510 (Set.inter_subset_left.trans
511 Set.subset_union_left)).symm.toHomotopyEquiv 1)
512
513/-- **The circle-complement reduction** (Hatcher 2B.1, circle case): if arc
514complements in `S^D` are `H₁`-acyclic, then for `D ≥ 1`, `D ≠ 3`, every
515embedded circle in `S^D` has `H₁`-acyclic complement. Mayer-Vietoris over
516the complements of the two semicircle images inside the complement of the
517two endpoint images. -/
518theorem isZero_h1_complement_of_embedding (D : ℕ) (hD : 1 ≤ D) (hD3 : D ≠ 3)
519 (harc : ArcComplementsAcyclic D)
520 (g : C(↥(Sph 1), ↥(Sph D))) (hg : Topology.IsEmbedding g) :
521 IsZero (Hgrp (TopCat.of {y : ↥(Sph D) // y ∉ Set.range g}) 1) := by
522 haveI : T2Space ↥(Sph D) :=
523 inferInstanceAs (T2Space ↥(sphere (0 : Esp D) 1))
524 -- the two semicircle images
525 have hgP : Topology.IsEmbedding (g.comp arcPlus) := by
526 rw [ContinuousMap.coe_comp]
527 exact hg.comp isEmbedding_arcPlus
528 have hgM : Topology.IsEmbedding (g.comp arcMinus) := by
529 rw [ContinuousMap.coe_comp]
530 exact hg.comp isEmbedding_arcMinus
531 have hKPg : Set.range (g.comp arcPlus) = ⇑g '' Set.range arcPlus := by
532 rw [ContinuousMap.coe_comp, Set.range_comp]
533 have hKMg : Set.range (g.comp arcMinus) = ⇑g '' Set.range arcMinus := by
534 rw [ContinuousMap.coe_comp, Set.range_comp]
535 -- the two endpoint images
536 have hinter : Set.range (g.comp arcPlus) ∩ Set.range (g.comp arcMinus) =
537 ({g eastP, g westP} : Set ↥(Sph D)) := by
538 rw [hKPg, hKMg, ← Set.image_inter hg.injective,
539 range_arcPlus_inter_arcMinus, Set.image_pair]
540 have hcover : Set.range (g.comp arcPlus) ∪ Set.range (g.comp arcMinus) =
541 Set.range g := by
542 rw [hKPg, hKMg, ← Set.image_union, range_arcPlus_union_arcMinus,
543 Set.image_univ]
544 -- H₂ of the two-point complement vanishes
545 have hgqp : g westP ≠ g eastP := fun h =>
546 eastP_ne_westP (hg.injective h).symm
547 have hX2 : IsZero (Hgrp (TopCat.of
548 ((Set.range (g.comp arcPlus) ∩ Set.range (g.comp arcMinus))ᶜ :
549 Set ↥(Sph D))) 2) := by
550 rw [hinter]
551 exact isZero_h2_twoPointCompl hD hD3 (g eastP) (g westP) hgqp
552 -- assemble
553 have hbig := isZero_h1_unionCompl
554 (Set.range (g.comp arcPlus)) (Set.range (g.comp arcMinus))
555 (isCompact_range (g.comp arcPlus).continuous).isClosed
556 (isCompact_range (g.comp arcMinus).continuous).isClosed
557 hX2 (harc _ hgP) (harc _ hgM)
558 rw [hcover] at hbig
559 exact hbig
560
561/-! ## Transport to the `TopCat.sphere` model of the binder -/
562
563/-- The `Sph`-model map underlying a circle map in the `TopCat.sphere`
564(`ULift`) model. -/
565noncomputable def toSphMap (D : ℕ)
566 (f : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} D)) :
567 C(↥(Sph 1), ↥(Sph D)) :=
568 ⟨fun x =>
569 (show ULift.{0} ↥(sphere (0 : Esp D) 1) from
570 f (show ↥(TopCat.sphere.{0} 1) from ULift.up x)).down,
571 continuous_uliftDown.comp (f.continuous.comp continuous_uliftUp)⟩
572
573lemma isEmbedding_toSphMap (D : ℕ)
574 (f : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} D))
575 (hf : Topology.IsEmbedding f) :
576 Topology.IsEmbedding (toSphMap D f) :=
577 (Homeomorph.ulift.isEmbedding.comp hf).comp
578 Homeomorph.ulift.symm.isEmbedding
579
580/-- The complement of an embedded circle in the `TopCat.sphere` model is
581homeomorphic to its complement in the `Sph` model. -/
582noncomputable def complDownHomeo (D : ℕ)
583 (f : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} D)) :
584 {x : ↥(TopCat.sphere.{0} D) // x ∉ Set.range f} ≃ₜ
585 {y : ↥(Sph D) // y ∉ Set.range (toSphMap D f)} where
586 toFun x := ⟨(show ULift.{0} ↥(sphere (0 : Esp D) 1) from x.1).down,
587 fun ⟨z, hz⟩ => x.2 ⟨show ↥(TopCat.sphere.{0} 1) from ULift.up z,
588 congrArg ULift.up hz⟩⟩
589 invFun y := ⟨show ↥(TopCat.sphere.{0} D) from ULift.up y.1,
590 fun ⟨w, hw⟩ => y.2
591 ⟨(show ULift.{0} ↥(sphere (0 : Esp 1) 1) from w).down,
592 congrArg ULift.down hw⟩⟩
593 left_inv _ := rfl
594 right_inv _ := rfl
595 continuous_toFun :=
596 Continuous.subtype_mk (continuous_uliftDown.comp continuous_subtype_val) _
597 continuous_invFun :=
598 Continuous.subtype_mk (continuous_uliftUp.comp continuous_subtype_val) _
599
600/-- **The high-dimensional (and `D = 2`) vanishing, conditional on the arc
601frontier**: granting `ArcComplementsAcyclic D`, no embedded circle in `S^D`
602(`D ≥ 1`, `D ≠ 3`) has homologically nontrivial complement. -/
603theorem not_detects_of_arcAcyclic (D : ℕ) (hD : 1 ≤ D) (hD3 : D ≠ 3)
604 (harc : ArcComplementsAcyclic D) : ¬ DetectsNontrivialLinking D := by
605 rintro ⟨f, hemb, hH⟩
606 apply hH
607 have hz := isZero_h1_complement_of_embedding D hD hD3 harc
608 (toSphMap D f) (isEmbedding_toSphMap D f hemb)
609 exact hz.of_iso (hgrpIso (complDownHomeo D f).toHomotopyEquiv 1)
610
611/-- **The bridge's uniqueness half, conditional on the arc frontier**:
612granting arc-complement acyclicity in every dimension `D ≥ 2`, `D ≠ 3`,
613nontrivial linking forces `D = 3`. Dimensions `0` and `1` are the banked
614unconditional results (`LinkingVanishingLowDim`). -/
615theorem forces_D3_of_arcAcyclic
616 (harc : ∀ D, 2 ≤ D → D ≠ 3 → ArcComplementsAcyclic D) :
617 ∀ D, DetectsNontrivialLinking D → D = 3 := by
618 intro D hdet
619 by_contra hne
620 match D, hne with
621 | 0, _ => exact LinkingVanishingLowDim.not_detects_zero hdet
622 | 1, _ => exact LinkingVanishingLowDim.not_detects_one hdet
623 | (n + 2), hne =>
624 exact not_detects_of_arcAcyclic (n + 2) (by omega) hne
625 (harc (n + 2) (by omega) hne) hdet
626
627end LinkingVanishingHighDim
628end Foundation
629end IndisputableMonolith
630