IndisputableMonolith.Foundation.ArcComplementAcyclic
IndisputableMonolith/Foundation/ArcComplementAcyclic.lean · 871 lines · 60 declarations
show as:
view math explainer →
1/-
2Arc-complement acyclicity (Hatcher 2B.1, arc case): every topological
3embedding of the unit interval into `S^D` has `H₁`-acyclic complement.
4
5Campaign P-d3link, THE FINAL WALL. This file discharges the single
6remaining hypothesis parameter `ArcComplementsAcyclic D` of
7`LinkingVanishingHighDim`, unconditionally and for every `D`.
8
9## Proof (compact-support bisection over the banked Mayer-Vietoris layer)
10
11Suppose some 1-cycle `z` in the complement of the embedded arc `a([0,1])`
12is not a boundary.
13
14* **Elementwise class toolkit** (`classOf`, `classOf_eq_zero_iff`,
15 `exists_classOf`, `classOf_natural`): concrete homology classes of
16 cycles in a chain complex of `ℤ`-modules, built on Mathlib's
17 `moduleCatLeftHomologyData` and the banked `lhMapData` of layer 4;
18 a class vanishes iff its cycle bounds, and classes push forward along
19 chain maps.
20* **The bisection step** (`bounds_of_mv`, `bounds_of_halves`): the two
21 half-arc complements form an open cover of the midpoint complement
22 (contractible, so `H₂ = 0`); exactness of the banked Mayer-Vietoris
23 sequence at `H₁(U ∩ V)` makes the pair map injective, so a cycle whose
24 pushforwards bound in both half-arc complements already bounds in the
25 full arc complement. Hence `z` stays nonbounding in the complement of
26 one of the two halves; iterate.
27* **The limit step**: the nested intervals shrink to a point `t*`; the
28 complement of `a(t*)` is contractible (stereographic projection), so the
29 pushforward of `z` bounds there, via a 2-chain `w` with compact support
30 (`suppOf`, finitely many singular simplices with compact images). The
31 support misses `a(t*)`, so by continuity it misses `a(I_k)` for some
32 large `k`; the bounding chain lifts (`exists_chain_lift`), so `z`
33 already bounds in the complement of `a(I_k)` — contradiction.
34
35## Instance-diamond note (load-bearing, inherited from layers 4-5b)
36
37For `R = ℤ` every `ModuleCat ℤ` carrier has two `Module ℤ` instances,
38propositionally but not definitionally equal, and synthesis prefers the
39generic one. This file deprioritizes `AddCommGroup.toIntModule` and
40`SubNegMonoid.toZSMul` locally, matching layers 1-5b.
41-/
42import IndisputableMonolith.Foundation.LinkingVanishingHighDim
43
44namespace IndisputableMonolith
45namespace Foundation
46namespace ArcComplementAcyclic
47
48open CategoryTheory Category Limits AlgebraicTopology Simplicial Opposite
49open SingularPrism SingularSubdivision SingularMayerVietoris SingularSphere
50open SingularSphereGeometry LinkingVanishingHighDim
51open Metric Set
52
53attribute [local instance 10] Classical.decEq
54
55/- See the instance-diamond note in the module header. -/
56attribute [local instance 0] AddCommGroup.toIntModule
57attribute [local instance 0] SubNegMonoid.toZSMul
58
59set_option maxHeartbeats 800000
60
61/-! ## Elementwise helpers for isomorphisms of `ℤ`-modules -/
62
63section IsoElements
64
65variable {M N : ModuleCat.{0} ℤ}
66
67lemma inv_hom_apply (e : M ≅ N) (x : ↥M) : e.inv (e.hom x) = x := by
68 rw [← ModuleCat.comp_apply, e.hom_inv_id, ModuleCat.id_apply]
69
70lemma hom_inv_apply (e : M ≅ N) (x : ↥N) : e.hom (e.inv x) = x := by
71 rw [← ModuleCat.comp_apply, e.inv_hom_id, ModuleCat.id_apply]
72
73lemma hom_apply_eq_zero_iff (e : M ≅ N) (x : ↥M) : e.hom x = 0 ↔ x = 0 := by
74 constructor
75 · intro h
76 have h2 : e.inv (e.hom x) = e.inv 0 := by rw [h]
77 rw [inv_hom_apply, map_zero] at h2
78 exact h2
79 · intro h
80 rw [h, map_zero]
81
82/-- Every element of a zero object vanishes. -/
83lemma eq_zero_of_isZero (hM : IsZero M) (x : ↥M) : x = 0 := by
84 have h : 𝟙 M = 0 := hM.eq_of_src _ _
85 calc x = (𝟙 M) x := (ModuleCat.id_apply _ _).symm
86 _ = (0 : M ⟶ M) x := by rw [h]
87 _ = 0 := zeroApp x
88
89end IsoElements
90
91/-! ## The elementwise homology class toolkit
92
93Concrete homology classes of cycles of a chain complex of `ℤ`-modules,
94through the honest-index short complex `K.sc' (n+2) (n+1) n` and Mathlib's
95`moduleCatLeftHomologyData` (whose `H` is `ker ⧸ range` on the nose). -/
96
97section ClassToolkit
98
99variable (K L : ChainComplex (ModuleCat.{0} ℤ) ℕ)
100
101/-- The canonical isomorphism from `K.sc (n+1)` to the honest-index short
102complex `K.X (n+2) ⟶ K.X (n+1) ⟶ K.X n`. -/
103noncomputable def scIso (n : ℕ) : K.sc (n + 1) ≅ K.sc' (n + 2) (n + 1) n :=
104 K.isoSc' (n + 2) (n + 1) n (ChainComplex.prev ℕ (n + 1)) (ChainComplex.next_nat_succ n)
105
106/-- The homology class of a cycle, as an element of the abstract homology
107object `K.homology (n+1)`. -/
108noncomputable def classOf (n : ℕ) (z : ↥(K.X (n + 1))) (hz : K.d (n + 1) n z = 0) :
109 ↥(K.homology (n + 1)) :=
110 CategoryTheory.ShortComplex.homologyMap (scIso K n).inv
111 ((K.sc' (n + 2) (n + 1) n).moduleCatLeftHomologyData.homologyIso.inv
112 (Submodule.Quotient.mk ⟨z, hz⟩))
113
114/-- **The vanishing criterion.** The class of a cycle is zero iff the cycle
115is a boundary. -/
116lemma classOf_eq_zero_iff (n : ℕ) (z : ↥(K.X (n + 1))) (hz : K.d (n + 1) n z = 0) :
117 classOf K n z hz = 0 ↔ ∃ w : ↥(K.X (n + 2)), z = K.d (n + 2) (n + 1) w := by
118 have h1 : ∀ x : ↥((K.sc' (n + 2) (n + 1) n).homology),
119 CategoryTheory.ShortComplex.homologyMap (scIso K n).inv x = 0 ↔ x = 0 := fun x =>
120 hom_apply_eq_zero_iff (CategoryTheory.ShortComplex.homologyMapIso (scIso K n)).symm x
121 have h2 : ∀ q, (K.sc' (n + 2) (n + 1) n).moduleCatLeftHomologyData.homologyIso.inv q = 0 ↔
122 q = 0 := fun q =>
123 hom_apply_eq_zero_iff (K.sc' (n + 2) (n + 1) n).moduleCatLeftHomologyData.homologyIso.symm q
124 unfold classOf
125 rw [h1, h2, Submodule.Quotient.mk_eq_zero, LinearMap.mem_range]
126 constructor
127 · rintro ⟨w, hw⟩
128 exact ⟨w, (congrArg Subtype.val hw).symm⟩
129 · rintro ⟨w, hw⟩
130 exact ⟨w, Subtype.ext hw.symm⟩
131
132/-- **Representability.** Every homology element is the class of a cycle. -/
133lemma exists_classOf (n : ℕ) (h : ↥(K.homology (n + 1))) :
134 ∃ (z : ↥(K.X (n + 1))) (hz : K.d (n + 1) n z = 0), classOf K n z hz = h := by
135 obtain ⟨⟨z, hz⟩, hzq⟩ := Submodule.mkQ_surjective
136 (LinearMap.range (K.sc' (n + 2) (n + 1) n).moduleCatToCycles)
137 ((K.sc' (n + 2) (n + 1) n).moduleCatLeftHomologyData.homologyIso.hom
138 (CategoryTheory.ShortComplex.homologyMap (scIso K n).hom h))
139 refine ⟨z, hz, ?_⟩
140 unfold classOf
141 have hzq' : Submodule.Quotient.mk
142 (p := LinearMap.range (K.sc' (n + 2) (n + 1) n).moduleCatToCycles) ⟨z, hz⟩ =
143 (K.sc' (n + 2) (n + 1) n).moduleCatLeftHomologyData.homologyIso.hom
144 (CategoryTheory.ShortComplex.homologyMap (scIso K n).hom h) := hzq
145 rw [hzq', inv_hom_apply]
146 exact inv_hom_apply (CategoryTheory.ShortComplex.homologyMapIso (scIso K n)) h
147
148variable {K L}
149
150/-- **Naturality.** Classes push forward along chain maps. -/
151lemma classOf_natural (φ : K ⟶ L) (n : ℕ) (z : ↥(K.X (n + 1)))
152 (hz : K.d (n + 1) n z = 0) (hz' : L.d (n + 1) n (φ.f (n + 1) z) = 0) :
153 HomologicalComplex.homologyMap φ (n + 1) (classOf K n z hz) =
154 classOf L n (φ.f (n + 1) z) hz' := by
155 set ψ := (HomologicalComplex.shortComplexFunctor' (ModuleCat.{0} ℤ)
156 (ComplexShape.down ℕ) (n + 2) (n + 1) n).map φ with hψ
157 set e := HomologicalComplex.natIsoSc' (ModuleCat.{0} ℤ) (ComplexShape.down ℕ)
158 (n + 2) (n + 1) n (ChainComplex.prev ℕ (n + 1)) (ChainComplex.next_nat_succ n) with he
159 have hnat := e.hom.naturality φ
160 have hcomm : (HomologicalComplex.shortComplexFunctor (ModuleCat.{0} ℤ)
161 (ComplexShape.down ℕ) (n + 1)).map φ =
162 (scIso K n).hom ≫ ψ ≫ (scIso L n).inv := by
163 show (HomologicalComplex.shortComplexFunctor (ModuleCat.{0} ℤ)
164 (ComplexShape.down ℕ) (n + 1)).map φ = e.hom.app K ≫ ψ ≫ e.inv.app L
165 rw [← Category.assoc, ← hnat, Category.assoc, Iso.hom_inv_id_app,
166 Category.comp_id]
167 have h1 : HomologicalComplex.homologyMap φ (n + 1) =
168 CategoryTheory.ShortComplex.homologyMap ((scIso K n).hom ≫ ψ ≫ (scIso L n).inv) := by
169 show CategoryTheory.ShortComplex.homologyMap
170 ((HomologicalComplex.shortComplexFunctor (ModuleCat.{0} ℤ)
171 (ComplexShape.down ℕ) (n + 1)).map φ) = _
172 rw [hcomm]
173 have h2 : CategoryTheory.ShortComplex.homologyMap (scIso K n).hom (classOf K n z hz) =
174 (K.sc' (n + 2) (n + 1) n).moduleCatLeftHomologyData.homologyIso.inv
175 (Submodule.Quotient.mk ⟨z, hz⟩) := by
176 unfold classOf
177 exact hom_inv_apply (CategoryTheory.ShortComplex.homologyMapIso (scIso K n)) _
178 have h3 : CategoryTheory.ShortComplex.homologyMap ψ
179 ((K.sc' (n + 2) (n + 1) n).moduleCatLeftHomologyData.homologyIso.inv
180 (Submodule.Quotient.mk ⟨z, hz⟩)) =
181 (L.sc' (n + 2) (n + 1) n).moduleCatLeftHomologyData.homologyIso.inv
182 (Submodule.Quotient.mk ⟨φ.f (n + 1) z, hz'⟩) := by
183 rw [(SingularMayerVietoris.lhMapData ψ).homologyMap_eq, ModuleCat.comp_apply,
184 ModuleCat.comp_apply, hom_inv_apply]
185 have h5 : (SingularMayerVietoris.lhMapData ψ).φH
186 (Submodule.Quotient.mk ⟨z, hz⟩) =
187 Submodule.Quotient.mk (SingularMayerVietoris.kerMap ψ ⟨z, hz⟩) := rfl
188 rw [h5]
189 congr 1
190 calc HomologicalComplex.homologyMap φ (n + 1) (classOf K n z hz)
191 = CategoryTheory.ShortComplex.homologyMap (scIso L n).inv
192 (CategoryTheory.ShortComplex.homologyMap ψ
193 (CategoryTheory.ShortComplex.homologyMap (scIso K n).hom
194 (classOf K n z hz))) := by
195 have hmor : HomologicalComplex.homologyMap φ (n + 1) =
196 CategoryTheory.ShortComplex.homologyMap (scIso K n).hom ≫
197 CategoryTheory.ShortComplex.homologyMap ψ ≫
198 CategoryTheory.ShortComplex.homologyMap (scIso L n).inv := by
199 rw [h1, CategoryTheory.ShortComplex.homologyMap_comp,
200 CategoryTheory.ShortComplex.homologyMap_comp]
201 exact congrArg (fun m : K.homology (n + 1) ⟶ L.homology (n + 1) =>
202 m (classOf K n z hz)) hmor
203 _ = CategoryTheory.ShortComplex.homologyMap (scIso L n).inv
204 (CategoryTheory.ShortComplex.homologyMap ψ
205 ((K.sc' (n + 2) (n + 1) n).moduleCatLeftHomologyData.homologyIso.inv
206 (Submodule.Quotient.mk ⟨z, hz⟩))) :=
207 congrArg _ (congrArg _ h2)
208 _ = CategoryTheory.ShortComplex.homologyMap (scIso L n).inv
209 ((L.sc' (n + 2) (n + 1) n).moduleCatLeftHomologyData.homologyIso.inv
210 (Submodule.Quotient.mk ⟨φ.f (n + 1) z, hz'⟩)) :=
211 congrArg _ h3
212 _ = classOf L n (φ.f (n + 1) z) hz' := rfl
213
214end ClassToolkit
215
216/-! ## Topological wrappers: cycles, bounding, and classes of `1`-chains -/
217
218section TopWrappers
219
220/-- Elementwise boundary/chain-map commutation. -/
221lemma chainMap_bnd {A B : TopCat.{0}} (f : A ⟶ B) (n : ℕ) (x : ↥(Cgrp A (n + 1))) :
222 bnd B n (chainMap f (n + 1) x) = chainMap f n (bnd A n x) := by
223 have h := HomologicalComplex.Hom.comm (sChainMap f) (n + 1) n
224 have h2 := congrArg (fun ψ : Cgrp A (n + 1) ⟶ Cgrp B n => ψ x) h
225 simpa only [ModuleCat.comp_apply] using h2
226
227/-- Pushforwards of cycles are cycles. -/
228lemma chainMap_cycle {A B : TopCat.{0}} (f : A ⟶ B) (z : ↥(Cgrp A 1))
229 (hz : bnd A 0 z = 0) : bnd B 0 (chainMap f 1 z) = 0 := by
230 rw [chainMap_bnd f 0 z, hz, map_zero]
231
232/-- Functoriality of the chain map, elementwise. -/
233lemma chainMap_chainMap {A B C' : TopCat.{0}} (f : A ⟶ B) (g : B ⟶ C') (n : ℕ)
234 (x : ↥(Cgrp A n)) : chainMap g n (chainMap f n x) = chainMap (f ≫ g) n x := by
235 have h : sChainMap (f ≫ g) = sChainMap f ≫ sChainMap g :=
236 CategoryTheory.Functor.map_comp _ _ _
237 have h2 := congrArg (fun ψ : SC A ⟶ SC C' => ψ.f n) h
238 have h3 : chainMap (f ≫ g) n = chainMap f n ≫ chainMap g n := h2
239 rw [h3, ModuleCat.comp_apply]
240
241lemma chainMap_id (A : TopCat.{0}) (n : ℕ) (x : ↥(Cgrp A n)) :
242 chainMap (𝟙 A) n x = x := by
243 have h : sChainMap (𝟙 A) = 𝟙 (SC A) := CategoryTheory.Functor.map_id _ _
244 have h2 := congrArg (fun ψ : SC A ⟶ SC A => ψ.f n) h
245 have h3 : chainMap (𝟙 A) n = 𝟙 (Cgrp A n) := h2
246 rw [h3, ModuleCat.id_apply]
247
248/-- Bounding pushes forward along any continuous map. -/
249lemma bounds_map {A B : TopCat.{0}} (f : A ⟶ B) (z : ↥(Cgrp A 1))
250 (h : ∃ w, z = bnd A 1 w) : ∃ w, chainMap f 1 z = bnd B 1 w := by
251 obtain ⟨w, hw⟩ := h
252 exact ⟨chainMap f 2 w, by rw [hw, chainMap_bnd f 1 w]⟩
253
254/-- Bounding pulls back along a retraction (in particular a homeomorphism). -/
255lemma bounds_of_retract {A B : TopCat.{0}} (f : A ⟶ B) (g : B ⟶ A)
256 (hfg : f ≫ g = 𝟙 A) (z : ↥(Cgrp A 1))
257 (h : ∃ w, chainMap f 1 z = bnd B 1 w) : ∃ w, z = bnd A 1 w := by
258 obtain ⟨w, hw⟩ := h
259 refine ⟨chainMap g 2 w, ?_⟩
260 calc z = chainMap (𝟙 A) 1 z := (chainMap_id A 1 z).symm
261 _ = chainMap g 1 (chainMap f 1 z) := by rw [chainMap_chainMap, hfg]
262 _ = chainMap g 1 (bnd B 1 w) := by rw [hw]
263 _ = bnd A 1 (chainMap g 2 w) := (chainMap_bnd g 1 w).symm
264
265/-- The degree-`1` homology class of a `1`-cycle. -/
266noncomputable def cls (W : TopCat.{0}) (z : ↥(Cgrp W 1)) (hz : bnd W 0 z = 0) :
267 ↥(Hgrp W 1) :=
268 classOf (SC W) 0 z hz
269
270lemma cls_eq_zero_iff (W : TopCat.{0}) (z : ↥(Cgrp W 1)) (hz : bnd W 0 z = 0) :
271 cls W z hz = 0 ↔ ∃ w : ↥(Cgrp W 2), z = bnd W 1 w :=
272 classOf_eq_zero_iff (SC W) 0 z hz
273
274lemma cls_natural {A B : TopCat.{0}} (f : A ⟶ B) (z : ↥(Cgrp A 1))
275 (hz : bnd A 0 z = 0) :
276 HomologicalComplex.homologyMap (sChainMap f) 1 (cls A z hz) =
277 cls B (chainMap f 1 z) (chainMap_cycle f z hz) :=
278 classOf_natural (sChainMap f) 0 z hz (chainMap_cycle f z hz)
279
280/-- A nonvanishing `H₁` yields a nonbounding cycle. -/
281lemma exists_nonbounding {W : TopCat.{0}} (hW : ¬ IsZero (Hgrp W 1)) :
282 ∃ z : ↥(Cgrp W 1), bnd W 0 z = 0 ∧ ¬ ∃ w, z = bnd W 1 w := by
283 have hnz : ∃ h : ↥(Hgrp W 1), h ≠ 0 := by
284 by_contra hall
285 push_neg at hall
286 apply hW
287 haveI : Subsingleton ↥(Hgrp W 1) := ⟨fun x y => by rw [hall x, hall y]⟩
288 exact ModuleCat.isZero_of_subsingleton _
289 obtain ⟨h, hh⟩ := hnz
290 obtain ⟨z, hz, hcl⟩ := exists_classOf (SC W) 0 h
291 refine ⟨z, hz, fun hb => hh ?_⟩
292 rw [← hcl]
293 exact (classOf_eq_zero_iff (SC W) 0 z hz).mpr hb
294
295/-- A vanishing `H₁` makes every cycle bound. -/
296lemma bounds_of_isZero {W : TopCat.{0}} (hW : IsZero (Hgrp W 1))
297 (z : ↥(Cgrp W 1)) (hz : bnd W 0 z = 0) : ∃ w, z = bnd W 1 w :=
298 (cls_eq_zero_iff W z hz).mp (eq_zero_of_isZero hW _)
299
300end TopWrappers
301
302/-! ## Complement-space plumbing -/
303
304section Complements
305
306variable {W : TopCat.{0}}
307
308/-- The inclusion of the complement of a bigger set into the complement of a
309smaller one. -/
310noncomputable def cInc {S T : Set ↥W} (hST : S ⊆ T) :
311 TopCat.of {y : ↥W // y ∉ T} ⟶ TopCat.of {y : ↥W // y ∉ S} :=
312 TopCat.ofHom ⟨fun y => ⟨y.1, fun h => y.2 (hST h)⟩,
313 Continuous.subtype_mk continuous_subtype_val _⟩
314
315/-- The complement subtype's inclusion into the ambient space. -/
316noncomputable def cVal (S : Set ↥W) : TopCat.of {y : ↥W // y ∉ S} ⟶ W :=
317 TopCat.ofHom ⟨Subtype.val, continuous_subtype_val⟩
318
319lemma cVal_injective (S : Set ↥W) : Function.Injective (cVal S).hom :=
320 fun _ _ h => Subtype.ext h
321
322lemma cInc_comp {S T R : Set ↥W} (h1 : T ⊆ R) (h2 : S ⊆ T) :
323 cInc h1 ≫ cInc h2 = cInc (h2.trans h1) := by
324 ext x
325 rfl
326
327lemma cInc_comp_cVal {S T : Set ↥W} (h : S ⊆ T) :
328 cInc h ≫ cVal S = cVal T := by
329 ext x
330 rfl
331
332lemma cInc_cInc_id {S T : Set ↥W} (h1 : S ⊆ T) (h2 : T ⊆ S) :
333 cInc h1 ≫ cInc h2 = 𝟙 (TopCat.of {y : ↥W // y ∉ T}) := by
334 ext x
335 rfl
336
337/-- A `TopCat` morphism from a homeomorphism. -/
338noncomputable def homeoHom {A B : Type} [TopologicalSpace A] [TopologicalSpace B]
339 (e : A ≃ₜ B) : TopCat.of A ⟶ TopCat.of B :=
340 TopCat.ofHom ⟨e, e.continuous⟩
341
342lemma homeoHom_comp_symm {A B : Type} [TopologicalSpace A] [TopologicalSpace B]
343 (e : A ≃ₜ B) : homeoHom e ≫ homeoHom e.symm = 𝟙 (TopCat.of A) := by
344 ext x
345 exact e.symm_apply_apply x
346
347lemma homeoHom_symm_comp {A B : Type} [TopologicalSpace A] [TopologicalSpace B]
348 (e : A ≃ₜ B) : homeoHom e.symm ≫ homeoHom e = 𝟙 (TopCat.of B) := by
349 ext x
350 exact e.apply_symm_apply x
351
352/-! ### Simplex pushing and lifting between complement subtypes -/
353
354/-- The ambient simplex underlying a simplex of a complement subtype. -/
355noncomputable def cPush {S : Set ↥W} {n : ℕ}
356 (s : Idx (TopCat.of {y : ↥W // y ∉ S}) n) : Idx W n :=
357 (TopCat.toSSet.map (cVal S)).app (op ⦋n⦌) s
358
359lemma range_cPush {S : Set ↥W} {n : ℕ} (s : Idx (TopCat.of {y : ↥W // y ∉ S}) n) :
360 ∀ x ∈ Set.range ⇑(simplexEquiv W n (cPush s)), x ∉ S := by
361 intro x hx
362 unfold cPush at hx
363 rw [simplexEquiv_map, ContinuousMap.coe_comp] at hx
364 obtain ⟨t, ht⟩ := hx
365 rw [← ht]
366 exact ((simplexEquiv (TopCat.of {y : ↥W // y ∉ S}) n s) t).2
367
368/-- Lifting an ambient simplex avoiding `T` into the complement subtype. -/
369noncomputable def cLift (T : Set ↥W) {n : ℕ} (s : Idx W n)
370 (h : ∀ x ∈ Set.range ⇑(simplexEquiv W n s), x ∉ T) :
371 Idx (TopCat.of {y : ↥W // y ∉ T}) n :=
372 (simplexEquiv (TopCat.of {y : ↥W // y ∉ T}) n).symm
373 ⟨fun t => ⟨simplexEquiv W n s t, h _ ⟨t, rfl⟩⟩,
374 (map_continuous (simplexEquiv W n s)).subtype_mk _⟩
375
376lemma cPush_cLift (T : Set ↥W) {n : ℕ} (s : Idx W n)
377 (h : ∀ x ∈ Set.range ⇑(simplexEquiv W n s), x ∉ T) :
378 cPush (cLift T s h) = s := by
379 apply (simplexEquiv W n).injective
380 unfold cPush cLift
381 rw [simplexEquiv_map, Equiv.apply_symm_apply]
382 ext t
383 rfl
384
385lemma chainMap_cVal_unitOf {S : Set ↥W} {n : ℕ}
386 (s : Idx (TopCat.of {y : ↥W // y ∉ S}) n) :
387 chainMap (cVal S) n (unitOf s) = unitOf (cPush s) :=
388 chainMap_unitOf _ s
389
390/-- **Compact-support lifting.** A chain of the complement of `S` whose
391support avoids `T` (in the ambient space) comes from a chain of the
392complement of `T`, up to the common ambient pushforward. -/
393lemma exists_chain_lift {S T : Set ↥W} {n : ℕ}
394 (c : ↥(Cgrp (TopCat.of {y : ↥W // y ∉ S}) n))
395 (h : ∀ s ∈ suppOf c, ∀ x ∈ Set.range ⇑(simplexEquiv W n (cPush s)), x ∉ T) :
396 ∃ c' : ↥(Cgrp (TopCat.of {y : ↥W // y ∉ T}) n),
397 chainMap (cVal T) n c' = chainMap (cVal S) n c := by
398 refine ⟨∑ i ∈ (suppOf c).attach,
399 coordAt i.1 c • unitOf (cLift T (cPush i.1) (h i.1 i.2)), ?_⟩
400 have hterm : ∀ i ∈ (suppOf c).attach,
401 chainMap (cVal T) n (coordAt i.1 c • unitOf (cLift T (cPush i.1) (h i.1 i.2))) =
402 coordAt i.1 c • unitOf (cPush i.1) := by
403 intro i _
404 rw [mapSmul, chainMap_cVal_unitOf, cPush_cLift]
405 have hc : chainMap (cVal S) n c = ∑ i ∈ suppOf c, coordAt i c • unitOf (cPush i) := by
406 conv_lhs => rw [sum_coordAt_smul_unitOf c]
407 rw [map_sum]
408 exact Finset.sum_congr rfl fun i _ => by rw [mapSmul, chainMap_cVal_unitOf]
409 calc chainMap (cVal T) n (∑ i ∈ (suppOf c).attach,
410 coordAt i.1 c • unitOf (cLift T (cPush i.1) (h i.1 i.2)))
411 = ∑ i ∈ (suppOf c).attach, coordAt i.1 c • unitOf (cPush i.1) := by
412 rw [map_sum]
413 exact Finset.sum_congr rfl hterm
414 _ = ∑ i ∈ suppOf c, coordAt i c • unitOf (cPush i) :=
415 Finset.sum_attach (suppOf c) (fun i => coordAt i c • unitOf (cPush i))
416 _ = chainMap (cVal S) n c := hc.symm
417
418end Complements
419
420/-! ## The elementwise Mayer-Vietoris bisection step -/
421
422section MVStep
423
424/-- **Elementwise MV injectivity at `H₁(U ∩ V)`.** With `H₂(X) = 0`, a
4251-cycle of `U ∩ V` whose pushforwards bound in `U` and in `V` bounds in
426`U ∩ V`. -/
427theorem bounds_of_mv {X : TopCat.{0}} {U V : Set X}
428 (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
429 (hX2 : IsZero (Hgrp X 2))
430 (z : ↥(Cgrp (TopCat.of (U ∩ V : Set X)) 1))
431 (hz : bnd (TopCat.of (U ∩ V : Set X)) 0 z = 0)
432 (hzU : ∃ w, chainMap (mvInclU U V) 1 z = bnd (TopCat.of U) 1 w)
433 (hzV : ∃ w, chainMap (mvInclV U V) 1 z = bnd (TopCat.of V) 1 w) :
434 ∃ w, z = bnd (TopCat.of (U ∩ V : Set X)) 1 w := by
435 rw [← cls_eq_zero_iff (TopCat.of (U ∩ V : Set X)) z hz]
436 have hU0 : cls (TopCat.of U) (chainMap (mvInclU U V) 1 z)
437 (chainMap_cycle (mvInclU U V) z hz) = 0 :=
438 (cls_eq_zero_iff _ _ _).mpr hzU
439 have hV0 : cls (TopCat.of V) (chainMap (mvInclV U V) 1 z)
440 (chainMap_cycle (mvInclV U V) z hz) = 0 :=
441 (cls_eq_zero_iff _ _ _).mpr hzV
442 have hfst : (biprod.fst : Hgrp (TopCat.of U) 1 ⊞ Hgrp (TopCat.of V) 1 ⟶ _)
443 (mvPair U V 1 (cls (TopCat.of (U ∩ V : Set X)) z hz)) = 0 := by
444 have h1 : mvPair U V 1 ≫
445 (biprod.fst : Hgrp (TopCat.of U) 1 ⊞ Hgrp (TopCat.of V) 1 ⟶ _) =
446 HomologicalComplex.homologyMap (sChainMap (mvInclU U V)) 1 :=
447 biprod.lift_fst _ _
448 rw [← ModuleCat.comp_apply, h1, cls_natural (mvInclU U V) z hz, hU0]
449 have hsnd : (biprod.snd : Hgrp (TopCat.of U) 1 ⊞ Hgrp (TopCat.of V) 1 ⟶ _)
450 (mvPair U V 1 (cls (TopCat.of (U ∩ V : Set X)) z hz)) = 0 := by
451 have h1 : mvPair U V 1 ≫
452 (biprod.snd : Hgrp (TopCat.of U) 1 ⊞ Hgrp (TopCat.of V) 1 ⟶ _) =
453 -(HomologicalComplex.homologyMap (sChainMap (mvInclV U V)) 1) :=
454 biprod.lift_snd _ _
455 rw [← ModuleCat.comp_apply, h1, negApp, cls_natural (mvInclV U V) z hz,
456 hV0, neg_zero]
457 have hpair : mvPair U V 1 (cls (TopCat.of (U ∩ V : Set X)) z hz) = 0 := by
458 apply biprod_elem_ext
459 · rw [hfst]
460 exact (map_zero _).symm
461 · rw [hsnd]
462 exact (map_zero _).symm
463 have hex := mv_exact₁ hU hV hUV 1
464 rw [CategoryTheory.ShortComplex.moduleCat_exact_iff] at hex
465 obtain ⟨y, hy⟩ := hex (cls (TopCat.of (U ∩ V : Set X)) z hz) hpair
466 rw [← hy, eq_zero_of_isZero hX2 y, map_zero]
467
468/-- The homeomorphism from the union complement to the Mayer-Vietoris
469intersection inside the complement of `KP ∩ KM`. -/
470noncomputable def unionComplHomeo {W : TopCat.{0}} (KP KM : Set ↥W) :
471 {y : ↥W // y ∉ KP ∪ KM} ≃ₜ
472 ↥(({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KP} ∩
473 {x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KM} :
474 Set ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)))) where
475 toFun y := ⟨⟨y.1, fun h => y.2 (Set.mem_union_left _ h.1)⟩,
476 fun h => y.2 (Set.mem_union_left _ h),
477 fun h => y.2 (Set.mem_union_right _ h)⟩
478 invFun x := ⟨x.1.1, fun h => h.elim (fun hP => x.2.1 hP) (fun hM => x.2.2 hM)⟩
479 left_inv _ := rfl
480 right_inv _ := rfl
481 continuous_toFun :=
482 Continuous.subtype_mk (Continuous.subtype_mk continuous_subtype_val _) _
483 continuous_invFun :=
484 Continuous.subtype_mk (continuous_subtype_val.comp continuous_subtype_val) _
485
486/-- **The bisection step** (elementwise two-arc Mayer-Vietoris): a 1-cycle
487of the complement of `KU = KP ∪ KM` whose pushforwards bound in the
488complements of both halves bounds already, provided `H₂((KP ∩ KM)ᶜ) = 0`. -/
489theorem bounds_of_halves {W : TopCat.{0}} {KP KM KU : Set ↥W}
490 (hKPc : IsClosed KP) (hKMc : IsClosed KM) (hunion : KU = KP ∪ KM)
491 (hX2 : IsZero (Hgrp (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) 2))
492 (z : ↥(Cgrp (TopCat.of {y : ↥W // y ∉ KU}) 1))
493 (hz : bnd (TopCat.of {y : ↥W // y ∉ KU}) 0 z = 0)
494 (hPU : KP ⊆ KU) (hMU : KM ⊆ KU)
495 (hP : ∃ w, chainMap (cInc hPU) 1 z = bnd (TopCat.of {y : ↥W // y ∉ KP}) 1 w)
496 (hM : ∃ w, chainMap (cInc hMU) 1 z = bnd (TopCat.of {y : ↥W // y ∉ KM}) 1 w) :
497 ∃ w, z = bnd (TopCat.of {y : ↥W // y ∉ KU}) 1 w := by
498 subst hunion
499 -- the MV cover of the midpoint complement by the two half complements
500 have hUopen : IsOpen
501 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KP} :
502 Set (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W))) :=
503 hKPc.isOpen_compl.preimage continuous_subtype_val
504 have hVopen : IsOpen
505 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KM} :
506 Set (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W))) :=
507 hKMc.isOpen_compl.preimage continuous_subtype_val
508 have hUVcover :
509 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KP} :
510 Set (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W))) ∪
511 {x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KM} = Set.univ := by
512 rw [Set.eq_univ_iff_forall]
513 intro x
514 by_cases hxP : x.1 ∈ KP
515 · right
516 intro hxM
517 exact x.2 ⟨hxP, hxM⟩
518 · left
519 exact hxP
520 set e := unionComplHomeo KP KM with hedef
521 set z' := chainMap (homeoHom e) 1 z with hz'def
522 have hz'c : bnd _ 0 z' = 0 := chainMap_cycle _ z hz
523 -- backward transfer of bounding, U side
524 have hU_bounds : ∃ w, chainMap (mvInclU
525 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KP})
526 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KM}) : _) 1 z' =
527 bnd (TopCat.of ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KP} :
528 Set (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)))) 1 w := by
529 set fP := flattenComplHomeo (W := W) (KP ∩ KM) KP Set.inter_subset_left with hfP
530 apply bounds_of_retract (homeoHom fP) (homeoHom fP.symm) (homeoHom_comp_symm fP)
531 have hcommP : homeoHom e ≫ mvInclU _ _ ≫ homeoHom fP = cInc hPU := by
532 ext x
533 rfl
534 have heq : chainMap (homeoHom fP) 1 (chainMap (mvInclU _ _) 1 z') =
535 chainMap (cInc hPU) 1 z := by
536 rw [hz'def, chainMap_chainMap, chainMap_chainMap, hcommP]
537 rw [heq]
538 exact hP
539 -- backward transfer of bounding, V side
540 have hV_bounds : ∃ w, chainMap (mvInclV
541 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KP})
542 ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KM}) : _) 1 z' =
543 bnd (TopCat.of ({x : ↥(TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)) | x.1 ∉ KM} :
544 Set (TopCat.of ((KP ∩ KM)ᶜ : Set ↥W)))) 1 w := by
545 set fM := flattenComplHomeo (W := W) (KP ∩ KM) KM Set.inter_subset_right with hfM
546 apply bounds_of_retract (homeoHom fM) (homeoHom fM.symm) (homeoHom_comp_symm fM)
547 have hcommM : homeoHom e ≫ mvInclV _ _ ≫ homeoHom fM = cInc hMU := by
548 ext x
549 rfl
550 have heq : chainMap (homeoHom fM) 1 (chainMap (mvInclV _ _) 1 z') =
551 chainMap (cInc hMU) 1 z := by
552 rw [hz'def, chainMap_chainMap, chainMap_chainMap, hcommM]
553 rw [heq]
554 exact hM
555 have hmid := bounds_of_mv hUopen hVopen hUVcover hX2 z' hz'c hU_bounds hV_bounds
556 exact bounds_of_retract (homeoHom e) (homeoHom e.symm) (homeoHom_comp_symm e) z hmid
557
558end MVStep
559
560/-! ## The geometric bisection on an embedded arc -/
561
562section Geometry
563
564variable {D : ℕ} (a : C(unitInterval, ↥(Sph D)))
565
566/-- The image of the parameter subinterval `[u, v]` under the arc. -/
567noncomputable def seg (u v : ℝ) : Set ↥(Sph D) :=
568 ⇑a '' {q : unitInterval | u ≤ (q : ℝ) ∧ (q : ℝ) ≤ v}
569
570lemma seg_subset_range (u v : ℝ) : seg a u v ⊆ Set.range ⇑a :=
571 Set.image_subset_range _ _
572
573lemma range_subset_seg : Set.range ⇑a ⊆ seg a 0 1 := by
574 rintro _ ⟨q, rfl⟩
575 exact ⟨q, ⟨q.2.1, q.2.2⟩, rfl⟩
576
577lemma seg_mono {u v u' v' : ℝ} (hu : u' ≤ u) (hv : v ≤ v') :
578 seg a u v ⊆ seg a u' v' := by
579 rintro _ ⟨q, ⟨h1, h2⟩, rfl⟩
580 exact ⟨q, ⟨hu.trans h1, h2.trans hv⟩, rfl⟩
581
582lemma isCompact_seg (u v : ℝ) : IsCompact (seg a u v) := by
583 apply IsCompact.image _ (map_continuous a)
584 have hcl : IsClosed {q : unitInterval | u ≤ (q : ℝ) ∧ (q : ℝ) ≤ v} := by
585 have h : {q : unitInterval | u ≤ (q : ℝ) ∧ (q : ℝ) ≤ v} =
586 (fun q : unitInterval => (q : ℝ)) ⁻¹' (Set.Icc u v) := rfl
587 rw [h]
588 exact isClosed_Icc.preimage continuous_subtype_val
589 exact hcl.isCompact
590
591lemma isClosed_seg (u v : ℝ) : IsClosed (seg a u v) := by
592 haveI : T2Space ↥(Sph D) :=
593 inferInstanceAs (T2Space (sphere (0 : Esp D) 1))
594 exact (isCompact_seg a u v).isClosed
595
596lemma seg_union {u v m : ℝ} (h1 : u ≤ m) (h2 : m ≤ v) :
597 seg a u v = seg a u m ∪ seg a m v := by
598 unfold seg
599 rw [← Set.image_union]
600 congr 1
601 ext q
602 simp only [Set.mem_union, Set.mem_setOf_eq]
603 constructor
604 · rintro ⟨h3, h4⟩
605 rcases le_total (q : ℝ) m with h5 | h5
606 · exact Or.inl ⟨h3, h5⟩
607 · exact Or.inr ⟨h5, h4⟩
608 · rintro (⟨h3, h4⟩ | ⟨h3, h4⟩)
609 · exact ⟨h3, h4.trans h2⟩
610 · exact ⟨h1.trans h3, h4⟩
611
612lemma seg_inter (hinj : Function.Injective ⇑a) {u v m : ℝ}
613 (hm0 : 0 ≤ m) (hm1 : m ≤ 1) (h1 : u ≤ m) (h2 : m ≤ v) :
614 seg a u m ∩ seg a m v = {a ⟨m, hm0, hm1⟩} := by
615 unfold seg
616 rw [← Set.image_inter hinj]
617 have hq : {q : unitInterval | u ≤ (q : ℝ) ∧ (q : ℝ) ≤ m} ∩
618 {q : unitInterval | m ≤ (q : ℝ) ∧ (q : ℝ) ≤ v} =
619 {(⟨m, hm0, hm1⟩ : unitInterval)} := by
620 ext q
621 simp only [Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_singleton_iff]
622 constructor
623 · rintro ⟨⟨_, h4⟩, ⟨h5, _⟩⟩
624 exact Subtype.ext (le_antisymm h4 h5)
625 · rintro rfl
626 exact ⟨⟨h1, le_refl m⟩, ⟨le_refl m, h2⟩⟩
627 rw [hq, Set.image_singleton]
628
629variable (z : ↥(Cgrp (TopCat.of {y : ↥(Sph D) // y ∉ Set.range ⇑a}) 1))
630
631/-- The pushforward of the reference cycle into the complement of
632`a([u, v])`. -/
633noncomputable def zSeg (u v : ℝ) :
634 ↥(Cgrp (TopCat.of {y : ↥(Sph D) // y ∉ seg a u v}) 1) :=
635 chainMap (cInc (seg_subset_range a u v)) 1 z
636
637/-- The bisection invariant: `[u, v] ⊆ [0, 1]` and the pushforward of the
638reference cycle into the complement of `a([u, v])` is not a boundary. -/
639def Bad (u v : ℝ) : Prop :=
640 0 ≤ u ∧ v ≤ 1 ∧ u ≤ v ∧
641 ¬ ∃ w, zSeg a z u v = bnd (TopCat.of {y : ↥(Sph D) // y ∉ seg a u v}) 1 w
642
643lemma zSeg_cycle (hz : bnd (TopCat.of {y : ↥(Sph D) // y ∉ Set.range ⇑a}) 0 z = 0)
644 (u v : ℝ) :
645 bnd (TopCat.of {y : ↥(Sph D) // y ∉ seg a u v}) 0 (zSeg a z u v) = 0 :=
646 chainMap_cycle _ z hz
647
648/-- Restriction of the pushforward to a smaller parameter interval. -/
649lemma zSeg_restrict {u v u' v' : ℝ}
650 (hseg : seg a u' v' ⊆ seg a u v) :
651 chainMap (cInc hseg) 1 (zSeg a z u v) = zSeg a z u' v' := by
652 unfold zSeg
653 rw [chainMap_chainMap, cInc_comp]
654
655/-- **The bisection step**: a bad interval has a bad half. -/
656lemma bad_step (hinj : Function.Injective ⇑a)
657 (hz : bnd (TopCat.of {y : ↥(Sph D) // y ∉ Set.range ⇑a}) 0 z = 0)
658 {u v : ℝ} (h : Bad a z u v) :
659 ∃ q : ℝ × ℝ, Bad a z q.1 q.2 ∧ u ≤ q.1 ∧ q.2 ≤ v ∧
660 q.2 - q.1 = (v - u) / 2 := by
661 obtain ⟨hu0, hv1, huv, hnb⟩ := h
662 set m := (u + v) / 2 with hm
663 have hum : u ≤ m := by rw [hm]; linarith
664 have hmv : m ≤ v := by rw [hm]; linarith
665 have hm0 : 0 ≤ m := hu0.trans hum
666 have hm1 : m ≤ 1 := hmv.trans hv1
667 by_cases hb1 : Bad a z u m
668 · exact ⟨(u, m), hb1, le_refl u, hmv, by rw [hm]; ring⟩
669 · refine ⟨(m, v), ⟨hm0, hv1, hmv, ?_⟩, hum, le_refl v, by rw [hm]; ring⟩
670 intro hb2
671 -- both halves bound: assemble the MV contradiction
672 have hb1' : ∃ w, zSeg a z u m =
673 bnd (TopCat.of {y : ↥(Sph D) // y ∉ seg a u m}) 1 w := by
674 by_contra hb1''
675 exact hb1 ⟨hu0, hm1, hum, hb1''⟩
676 apply hnb
677 -- H₂ of the midpoint complement vanishes (punctured sphere contractible)
678 have hinter : seg a u m ∩ seg a m v = {a ⟨m, hm0, hm1⟩} :=
679 seg_inter a hinj hm0 hm1 hum hmv
680 haveI hcontr : ContractibleSpace
681 ↥((({a ⟨m, hm0, hm1⟩} : Set ↥(Sph D))ᶜ : Set ↥(Sph D))) :=
682 contractibleSpace_compl_singleton_sphere (a ⟨m, hm0, hm1⟩)
683 have hX2 : IsZero (Hgrp (TopCat.of
684 ((seg a u m ∩ seg a m v)ᶜ : Set ↥(Sph D))) 2) := by
685 rw [hinter]
686 exact isZero_homology_of_contractible _ (by norm_num)
687 -- run the two-arc MV step
688 have hPU : seg a u m ⊆ seg a u v := seg_mono a (le_refl u) hmv
689 have hMU : seg a m v ⊆ seg a u v := seg_mono a hum (le_refl v)
690 refine bounds_of_halves (isClosed_seg a u m) (isClosed_seg a m v)
691 (seg_union a hum hmv) hX2 (zSeg a z u v) (zSeg_cycle a z hz u v)
692 hPU hMU ?_ ?_
693 · rw [zSeg_restrict a z hPU]
694 exact hb1'
695 · rw [zSeg_restrict a z hMU]
696 exact hb2
697
698/-- The nested bad-interval sequence, carrying its invariant. -/
699noncomputable def badSeq (hinj : Function.Injective ⇑a)
700 (hz : bnd (TopCat.of {y : ↥(Sph D) // y ∉ Set.range ⇑a}) 0 z = 0)
701 (h0 : Bad a z 0 1) : ℕ → {p : ℝ × ℝ // Bad a z p.1 p.2}
702 | 0 => ⟨(0, 1), h0⟩
703 | (k + 1) =>
704 ⟨(bad_step a z hinj hz (badSeq hinj hz h0 k).2).choose,
705 (bad_step a z hinj hz (badSeq hinj hz h0 k).2).choose_spec.1⟩
706
707variable (hinj : Function.Injective ⇑a)
708 (hz : bnd (TopCat.of {y : ↥(Sph D) // y ∉ Set.range ⇑a}) 0 z = 0)
709 (h0 : Bad a z 0 1)
710
711lemma badSeq_zero : (badSeq a z hinj hz h0 0).1 = (0, 1) := rfl
712
713lemma badSeq_succ (k : ℕ) :
714 (badSeq a z hinj hz h0 k).1.1 ≤ (badSeq a z hinj hz h0 (k + 1)).1.1 ∧
715 (badSeq a z hinj hz h0 (k + 1)).1.2 ≤ (badSeq a z hinj hz h0 k).1.2 ∧
716 (badSeq a z hinj hz h0 (k + 1)).1.2 - (badSeq a z hinj hz h0 (k + 1)).1.1 =
717 ((badSeq a z hinj hz h0 k).1.2 - (badSeq a z hinj hz h0 k).1.1) / 2 := by
718 have hspec := (bad_step a z hinj hz (badSeq a z hinj hz h0 k).2).choose_spec
719 exact ⟨hspec.2.1, hspec.2.2.1, hspec.2.2.2⟩
720
721lemma badSeq_width (k : ℕ) :
722 (badSeq a z hinj hz h0 k).1.2 - (badSeq a z hinj hz h0 k).1.1 =
723 (1 / 2 : ℝ) ^ k := by
724 induction k with
725 | zero =>
726 rw [badSeq_zero]
727 norm_num
728 | succ k IH =>
729 rw [(badSeq_succ a z hinj hz h0 k).2.2, IH]
730 ring
731
732lemma badSeq_mono : Monotone (fun k => (badSeq a z hinj hz h0 k).1.1) :=
733 monotone_nat_of_le_succ fun k => (badSeq_succ a z hinj hz h0 k).1
734
735lemma badSeq_anti : Antitone (fun k => (badSeq a z hinj hz h0 k).1.2) :=
736 antitone_nat_of_succ_le fun k => (badSeq_succ a z hinj hz h0 k).2.1
737
738lemma badSeq_le (j k : ℕ) :
739 (badSeq a z hinj hz h0 j).1.1 ≤ (badSeq a z hinj hz h0 k).1.2 := by
740 rcases le_total j k with h | h
741 · exact (badSeq_mono a z hinj hz h0 h).trans
742 (badSeq a z hinj hz h0 k).2.2.2.1
743 · exact ((badSeq a z hinj hz h0 j).2.2.2.1).trans
744 (badSeq_anti a z hinj hz h0 h)
745
746/-- The interval endpoints of a bad interval, extracted with names (the
747`Bad` conjunction, destructured once for reuse). -/
748lemma badSeq_props (k : ℕ) :
749 0 ≤ (badSeq a z hinj hz h0 k).1.1 ∧ (badSeq a z hinj hz h0 k).1.2 ≤ 1 ∧
750 (badSeq a z hinj hz h0 k).1.1 ≤ (badSeq a z hinj hz h0 k).1.2 :=
751 ⟨(badSeq a z hinj hz h0 k).2.1, (badSeq a z hinj hz h0 k).2.2.1,
752 (badSeq a z hinj hz h0 k).2.2.2.1⟩
753
754end Geometry
755
756/-! ## The main theorem -/
757
758/-- **Arc-complement acyclicity** (Hatcher 2B.1, arc case, formal):
759every topological embedding of the unit interval into `S^D` has
760`H₁`-acyclic complement, in every dimension `D`. -/
761theorem arcComplementsAcyclic (D : ℕ) :
762 LinkingVanishingHighDim.ArcComplementsAcyclic D := by
763 intro a hemb
764 by_contra hH
765 haveI : T2Space ↥(Sph D) :=
766 inferInstanceAs (T2Space (sphere (0 : Esp D) 1))
767 obtain ⟨z, hz, hznb⟩ := exists_nonbounding hH
768 have hinj : Function.Injective ⇑a := hemb.injective
769 -- the initial bad interval
770 have h0 : Bad a z 0 1 := by
771 refine ⟨le_refl 0, le_refl 1, zero_le_one, ?_⟩
772 intro hb
773 apply hznb
774 refine bounds_of_retract (cInc (seg_subset_range a 0 1))
775 (cInc (range_subset_seg a)) (cInc_cInc_id _ _) z ?_
776 exact hb
777 -- the nested bad intervals and their limit point
778 set s : ℕ → ℝ := fun k => (badSeq a z hinj hz h0 k).1.1 with hs
779 set t : ℕ → ℝ := fun k => (badSeq a z hinj hz h0 k).1.2 with ht
780 have hbdd : BddAbove (Set.range s) := by
781 refine ⟨1, ?_⟩
782 rintro _ ⟨k, rfl⟩
783 exact ((badSeq a z hinj hz h0 k).2.2.2.1).trans (badSeq a z hinj hz h0 k).2.2.1
784 set tstar : ℝ := ⨆ k, s k with htstar
785 have hst : ∀ k, s k ≤ tstar := fun k => le_ciSup hbdd k
786 have hts : ∀ k, tstar ≤ t k := fun k =>
787 ciSup_le fun j => badSeq_le a z hinj hz h0 j k
788 have h0t : (0 : ℝ) ≤ tstar := by
789 have h := hst 0
790 rw [show s 0 = 0 from congrArg Prod.fst (badSeq_zero a z hinj hz h0)] at h
791 exact h
792 have ht1 : tstar ≤ 1 := by
793 have h := hts 0
794 rw [show t 0 = 1 from congrArg Prod.snd (badSeq_zero a z hinj hz h0)] at h
795 exact h
796 set tI : unitInterval := ⟨tstar, h0t, ht1⟩ with htI
797 set p : ↥(Sph D) := a tI with hp
798 -- the point complement is contractible, so the pushforward bounds there
799 have hpr : ({p} : Set ↥(Sph D)) ⊆ Set.range ⇑a := by
800 intro x hx
801 rw [Set.mem_singleton_iff] at hx
802 exact ⟨tI, hx.symm⟩
803 haveI hcontr : ContractibleSpace
804 ↥((({p} : Set ↥(Sph D))ᶜ : Set ↥(Sph D))) :=
805 contractibleSpace_compl_singleton_sphere p
806 have hzero : IsZero (Hgrp (TopCat.of
807 {y : ↥(Sph D) // y ∉ ({p} : Set ↥(Sph D))}) 1) := by
808 have h := isZero_homology_of_contractible
809 (TopCat.of ((({p} : Set ↥(Sph D))ᶜ : Set ↥(Sph D)))) one_ne_zero
810 exact h
811 obtain ⟨w, hw⟩ := bounds_of_isZero hzero (chainMap (cInc hpr) 1 z)
812 (chainMap_cycle _ z hz)
813 -- the compact support of the bounding chain misses `a(t*)`
814 set Kc : Set ↥(Sph D) :=
815 ⋃ i ∈ suppOf w, Set.range ⇑(simplexEquiv (Sph D) 2 (cPush i)) with hKc
816 have hKc_compact : IsCompact Kc := by
817 rw [hKc]
818 exact (suppOf w).isCompact_biUnion fun i _ => isCompact_range (map_continuous _)
819 have hKc_closed : IsClosed Kc := hKc_compact.isClosed
820 have hKc_avoids : ∀ x ∈ Kc, x ∉ ({p} : Set ↥(Sph D)) := by
821 intro x hx
822 rw [hKc, Set.mem_iUnion₂] at hx
823 obtain ⟨i, _, hxi⟩ := hx
824 exact range_cPush i x hxi
825 -- an ε-neighbourhood of `t*` avoids the support
826 have hA_closed : IsClosed (⇑a ⁻¹' Kc) := hKc_closed.preimage (map_continuous a)
827 have htA : tI ∈ (⇑a ⁻¹' Kc)ᶜ := by
828 intro hmem
829 exact hKc_avoids (a tI) hmem (by rw [hp]; exact Set.mem_singleton _)
830 obtain ⟨ε, hε, hball⟩ := Metric.isOpen_iff.mp hA_closed.isOpen_compl tI htA
831 obtain ⟨k, hk⟩ := exists_pow_lt_of_lt_one hε (by norm_num : (1 / 2 : ℝ) < 1)
832 -- the k-th interval's arc image avoids the support
833 have hclaim : ∀ x ∈ seg a (s k) (t k), x ∉ Kc := by
834 rintro _ ⟨q, ⟨hq1, hq2⟩, rfl⟩ hxK
835 have hqball : q ∈ Metric.ball tI ε := by
836 rw [Metric.mem_ball, Subtype.dist_eq, Real.dist_eq]
837 have hwidth : t k - s k = (1 / 2 : ℝ) ^ k := badSeq_width a z hinj hz h0 k
838 have h1 : s k ≤ tstar := hst k
839 have h2 : tstar ≤ t k := hts k
840 have habs : |(q : ℝ) - tstar| ≤ (1 / 2 : ℝ) ^ k := by
841 rw [abs_le]
842 constructor
843 · linarith
844 · linarith
845 show |(q : ℝ) - tstar| < ε
846 exact lt_of_le_of_lt habs hk
847 exact hball hqball hxK
848 -- lift the bounding chain below the k-th arc complement
849 obtain ⟨w', hw'⟩ := exists_chain_lift (S := ({p} : Set ↥(Sph D)))
850 (T := seg a (s k) (t k)) w
851 (fun i hi x hx hxT => hclaim x hxT (Set.mem_biUnion hi hx))
852 -- contradiction with the k-th bad interval
853 apply (badSeq a z hinj hz h0 k).2.2.2.2
854 refine ⟨w', ?_⟩
855 apply chainMap_injective (cVal (seg a (s k) (t k))) (cVal_injective _) 1
856 have hL : chainMap (cVal (seg a (s k) (t k))) 1 (zSeg a z (s k) (t k)) =
857 chainMap (cVal (Set.range ⇑a)) 1 z := by
858 unfold zSeg
859 rw [chainMap_chainMap, cInc_comp_cVal]
860 have hR : chainMap (cVal (seg a (s k) (t k))) 1
861 (bnd (TopCat.of {y : ↥(Sph D) // y ∉ seg a (s k) (t k)}) 1 w') =
862 chainMap (cVal (Set.range ⇑a)) 1 z := by
863 rw [← chainMap_bnd (cVal (seg a (s k) (t k))) 1 w', hw',
864 chainMap_bnd (cVal ({p} : Set ↥(Sph D))) 1 w, ← hw,
865 chainMap_chainMap, cInc_comp_cVal]
866 rw [hL, hR]
867
868end ArcComplementAcyclic
869end Foundation
870end IndisputableMonolith
871