IndisputableMonolith.Foundation.UnknotComplementRetract

   1import Mathlib
   2
   3/-!
   4# Unknot complement retract: geometric core of `DetectsNontrivialLinking 3`
   5
   6Standalone module (imports only Mathlib) proving:
   7
   81. `unknot : C(𝕊 1, 𝕊 3)` — the flat unknot `(x₀,x₁) ↦ (x₀,x₁,0,0)`.
   92. `unknot_isEmbedding` — it is a topological embedding.
  103. `core` — the "dual" circle `z ↦ (0,0,z₀,z₁)` valued in the complement of
  11   the unknot.
  124. `retractToCore` — the retraction of the complement onto that circle,
  13   `y ↦ (y₂,y₃)/‖(y₂,y₃)‖`.
  145. `retract_core` — the retraction restricted along `core` is the identity.
  156. `unknotComplementH1_ne_zero` — given `H₁(S¹;ℤ) ≅ ℤ` (singular homology,
  16   Mathlib's `singularHomologyFunctor`), the first singular homology of the
  17   unknot complement in S³ is not the zero object.
  18
  19Everything is at universe 0 and matches the shapes used by
  20`IndisputableMonolith.Foundation.PublicSpine.linkingComplementH1` (not
  21imported here; the gluing happens elsewhere).
  22-/
  23
  24noncomputable section
  25
  26namespace IndisputableMonolith
  27namespace Foundation
  28namespace UnknotComplementRetract
  29
  30open scoped RealInnerProductSpace
  31open CategoryTheory CategoryTheory.Limits
  32
  33/-! ## Linear algebra: coordinate inclusions and projection -/
  34
  35/-- Inclusion `(x₀,x₁) ↦ (x₀,x₁,0,0)` as a linear isometry. -/
  36def incl01 : EuclideanSpace ℝ (Fin 2) →ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4) where
  37  toLinearMap :=
  38    { toFun := fun x => WithLp.toLp 2 ![x 0, x 1, 0, 0]
  39      map_add' := by
  40        intro x y
  41        ext i
  42        fin_cases i <;>
  43          simp [PiLp.add_apply]
  44      map_smul' := by
  45        intro c x
  46        ext i
  47        fin_cases i <;>
  48          simp [PiLp.smul_apply] }
  49  norm_map' := by
  50    intro x
  51    rw [EuclideanSpace.norm_eq, EuclideanSpace.norm_eq]
  52    congr 1
  53    rw [Fin.sum_univ_four, Fin.sum_univ_two]
  54    simp [PiLp.toLp_apply]
  55
  56/-- Inclusion `(x₀,x₁) ↦ (0,0,x₀,x₁)` as a linear isometry. -/
  57def incl23 : EuclideanSpace ℝ (Fin 2) →ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4) where
  58  toLinearMap :=
  59    { toFun := fun x => WithLp.toLp 2 ![0, 0, x 0, x 1]
  60      map_add' := by
  61        intro x y
  62        ext i
  63        fin_cases i <;>
  64          simp [PiLp.add_apply]
  65      map_smul' := by
  66        intro c x
  67        ext i
  68        fin_cases i <;>
  69          simp [PiLp.smul_apply] }
  70  norm_map' := by
  71    intro x
  72    rw [EuclideanSpace.norm_eq, EuclideanSpace.norm_eq]
  73    congr 1
  74    rw [Fin.sum_univ_four, Fin.sum_univ_two]
  75    simp [PiLp.toLp_apply]
  76
  77/-- Projection `y ↦ (y₂,y₃)` as a linear map (continuous by finite dimension). -/
  78def proj23 : EuclideanSpace ℝ (Fin 4) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2) where
  79  toFun := fun y => WithLp.toLp 2 ![y 2, y 3]
  80  map_add' := by
  81    intro x y
  82    ext i
  83    fin_cases i <;>
  84      simp [PiLp.add_apply]
  85  map_smul' := by
  86    intro c x
  87    ext i
  88    fin_cases i <;>
  89      simp [PiLp.smul_apply]
  90
  91lemma proj23_continuous : Continuous proj23 :=
  92  proj23.continuous_of_finiteDimensional
  93
  94@[simp] lemma incl01_apply_coord (x : EuclideanSpace ℝ (Fin 2)) :
  95    (incl01 x : Fin 4 → ℝ) = ![x 0, x 1, 0, 0] := rfl
  96
  97@[simp] lemma incl23_apply_coord (x : EuclideanSpace ℝ (Fin 2)) :
  98    (incl23 x : Fin 4 → ℝ) = ![0, 0, x 0, x 1] := rfl
  99
 100@[simp] lemma proj23_apply_coord (y : EuclideanSpace ℝ (Fin 4)) :
 101    (proj23 y : Fin 2 → ℝ) = ![y 2, y 3] := rfl
 102
 103/-! ## The unknot -/
 104
 105/-- Underlying point-level unknot: `S¹ → S³`, `(x₀,x₁) ↦ (x₀,x₁,0,0)`. -/
 106def unknotFun (z : ULift.{0} (Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)) :
 107    ULift.{0} (Metric.sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) :=
 108  ULift.up ⟨incl01 z.down.1, by
 109    rw [mem_sphere_zero_iff_norm, incl01.norm_map]
 110    exact mem_sphere_zero_iff_norm.1 z.down.2⟩
 111
 112/-- The standard flat unknot `S¹ ↪ S³` as a continuous map between the
 113`TopCat` spheres. -/
 114def unknot : C(TopCat.sphere.{0} 1, TopCat.sphere.{0} 3) where
 115  toFun := unknotFun
 116  continuous_toFun := by
 117    apply continuous_uliftUp.comp
 118    apply Continuous.subtype_mk
 119    exact incl01.continuous.comp
 120      (continuous_subtype_val.comp continuous_uliftDown)
 121
 122lemma unknot_injective : Function.Injective unknot := by
 123  intro a b hab
 124  have h4 : incl01 a.down.1 = incl01 b.down.1 :=
 125    congrArg (fun w => (ULift.down w).1) hab
 126  have h2 : a.down.1 = b.down.1 := incl01.injective h4
 127  exact ULift.ext a b (Subtype.ext h2)
 128
 129instance : CompactSpace (TopCat.sphere.{0} 1) := by
 130  show CompactSpace (ULift.{0} (Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1))
 131  infer_instance
 132
 133instance : T2Space (TopCat.sphere.{0} 3) := by
 134  show T2Space (ULift.{0} (Metric.sphere (0 : EuclideanSpace ℝ (Fin 4)) 1))
 135  infer_instance
 136
 137/-- The unknot is a topological embedding (continuous injective map from a
 138compact space to a Hausdorff space). -/
 139theorem unknot_isEmbedding : Topology.IsEmbedding unknot :=
 140  (unknot.continuous.isClosedEmbedding unknot_injective).isEmbedding
 141
 142/-! ## The complement and the core circle -/
 143
 144/-- The complement of the unknot in S³, as a `TopCat` object (exact shape of
 145`linkingComplementH1`'s argument). -/
 146def Cpl : TopCat.{0} :=
 147  TopCat.of {x : TopCat.sphere.{0} 3 // x ∉ Set.range unknot}
 148
 149/-- Coordinate extraction: a point in the range of the unknot has vanishing
 150coordinates 2 and 3. -/
 151lemma coord23_eq_zero_of_mem_range {y : TopCat.sphere.{0} 3}
 152    (hy : y ∈ Set.range unknot) :
 153    (ULift.down y).1 2 = 0 ∧ (ULift.down y).1 3 = 0 := by
 154  obtain ⟨w, hw⟩ := hy
 155  have h4 : incl01 w.down.1 = (ULift.down y).1 :=
 156    congrArg (fun v => (ULift.down v).1) hw
 157  constructor
 158  · have := congrFun (congrArg WithLp.ofLp h4) 2
 159    simpa using this.symm
 160  · have := congrFun (congrArg WithLp.ofLp h4) 3
 161    simpa using this.symm
 162
 163/-- Point-level core circle `z ↦ (0,0,z₀,z₁)`, landing in the complement. -/
 164def coreFun (z : TopCat.sphere.{0} 1) : Cpl := by
 165  refine ⟨ULift.up ⟨incl23 (ULift.down (α := Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) z).1, ?_⟩, ?_⟩
 166  · rw [mem_sphere_zero_iff_norm, incl23.norm_map]
 167    exact mem_sphere_zero_iff_norm.1 z.down.2
 168  · intro hmem
 169    obtain ⟨h2, h3⟩ := coord23_eq_zero_of_mem_range hmem
 170    have hz0 : z.down.1 0 = 0 := by simpa using h2
 171    have hz1 : z.down.1 1 = 0 := by simpa using h3
 172    have hz : z.down.1 = 0 := by
 173      ext i
 174      fin_cases i
 175      · simpa using hz0
 176      · simpa using hz1
 177    have hnorm : ‖z.down.1‖ = 1 := mem_sphere_zero_iff_norm.1 z.down.2
 178    rw [hz, norm_zero] at hnorm
 179    exact zero_ne_one hnorm
 180
 181/-- The core circle as a continuous map into the complement. -/
 182def core : C(TopCat.sphere.{0} 1, Cpl) where
 183  toFun := coreFun
 184  continuous_toFun := by
 185    apply Continuous.subtype_mk
 186    apply continuous_uliftUp.comp
 187    apply Continuous.subtype_mk
 188    exact incl23.continuous.comp
 189      (continuous_subtype_val.comp continuous_uliftDown)
 190
 191/-! ## The retraction -/
 192
 193/-- The `(y₂,y₃)`-part of a point of the complement. -/
 194def part23 (y : Cpl) : EuclideanSpace ℝ (Fin 2) :=
 195  proj23 (ULift.down y.1).1
 196
 197lemma part23_continuous : Continuous part23 :=
 198  proj23_continuous.comp
 199    (continuous_subtype_val.comp (continuous_uliftDown.comp continuous_subtype_val))
 200
 201/-- Well-definedness: on the complement of the unknot, `(y₂,y₃) ≠ 0`. -/
 202lemma part23_ne_zero (y : Cpl) : part23 y ≠ 0 := by
 203  intro h0
 204  set x : EuclideanSpace ℝ (Fin 4) := (ULift.down y.1).1 with hx
 205  have h2 : x 2 = 0 := by
 206    have := congrFun (congrArg WithLp.ofLp h0) 0
 207    simpa [part23, hx] using this
 208  have h3 : x 3 = 0 := by
 209    have := congrFun (congrArg WithLp.ofLp h0) 1
 210    simpa [part23, hx] using this
 211  -- the head part (x₀,x₁) then has norm 1
 212  set z : EuclideanSpace ℝ (Fin 2) := WithLp.toLp 2 ![x 0, x 1] with hzdef
 213  have hxnorm : ‖x‖ = 1 := mem_sphere_zero_iff_norm.1 (ULift.down y.1).2
 214  have hznorm : ‖z‖ = 1 := by
 215    rw [EuclideanSpace.norm_eq] at hxnorm ⊢
 216    rw [Fin.sum_univ_four] at hxnorm
 217    rw [Fin.sum_univ_two]
 218    rw [h2, h3] at hxnorm
 219    simpa [hzdef, PiLp.toLp_apply] using hxnorm
 220  -- hence y is in the range of the unknot: contradiction
 221  apply y.2
 222  refine ⟨ULift.up ⟨z, mem_sphere_zero_iff_norm.2 hznorm⟩, ?_⟩
 223  apply ULift.ext
 224  apply Subtype.ext
 225  show incl01 z = x
 226  ext i
 227  fin_cases i
 228  · simp [hzdef]
 229  · simp [hzdef]
 230  · simpa using h2.symm
 231  · simpa using h3.symm
 232
 233/-- Point-level retraction `y ↦ (y₂,y₃)/‖(y₂,y₃)‖`. -/
 234def retractFun (y : Cpl) : TopCat.sphere.{0} 1 :=
 235  ULift.up ⟨‖part23 y‖⁻¹ • part23 y, by
 236    rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm,
 237      inv_mul_cancel₀ (norm_ne_zero_iff.2 (part23_ne_zero y))]⟩
 238
 239/-- The retraction of the unknot complement onto the core circle. -/
 240def retractToCore : C(Cpl, TopCat.sphere.{0} 1) where
 241  toFun := retractFun
 242  continuous_toFun := by
 243    apply continuous_uliftUp.comp
 244    apply Continuous.subtype_mk
 245    exact ((part23_continuous.norm.inv₀
 246      fun y => norm_ne_zero_iff.2 (part23_ne_zero y)).smul part23_continuous)
 247
 248/-! ## Retraction identity on the core -/
 249
 250/-- Composite identity: the retraction restricted along the core circle is the
 251identity of S¹. -/
 252theorem retract_core (z : TopCat.sphere.{0} 1) : retractToCore (core z) = z := by
 253  have hpart : part23 (core z) = z.down.1 := by
 254    ext i
 255    fin_cases i <;>
 256      simp [part23, core, coreFun]
 257  have hnorm : ‖z.down.1‖ = 1 := mem_sphere_zero_iff_norm.1 z.down.2
 258  apply ULift.ext
 259  apply Subtype.ext
 260  show ‖part23 (core z)‖⁻¹ • part23 (core z) = z.down.1
 261  rw [hpart, hnorm, inv_one, one_smul]
 262
 263theorem retract_comp_core :
 264    (retractToCore.comp core) = ContinuousMap.id (TopCat.sphere.{0} 1) := by
 265  ext z
 266  exact retract_core z
 267
 268/-! ## Capstone: nontrivial H₁ of the complement -/
 269
 270/-- **Capstone.** Given that first singular homology of S¹ with ℤ coefficients
 271is ℤ (as an iso in `ModuleCat ℤ`), the first singular homology of the unknot
 272complement in S³ is not the zero object. Pure retraction argument: `core` and
 273`retractToCore` exhibit H₁(S¹) as a retract of H₁(complement). -/
 274theorem unknotComplementH1_ne_zero
 275    (h1 : Nonempty ((((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
 276      (ModuleCat.of ℤ ℤ)).obj (TopCat.sphere.{0} 1)) ≅ ModuleCat.of ℤ ℤ)) :
 277    ¬ CategoryTheory.Limits.IsZero
 278      (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
 279        (ModuleCat.of ℤ ℤ)).obj (TopCat.of {x : TopCat.sphere.{0} 3 // x ∉ Set.range unknot})) := by
 280  intro hz
 281  obtain ⟨e⟩ := h1
 282  set H : TopCat.{0} ⥤ ModuleCat ℤ :=
 283    (AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj (ModuleCat.of ℤ ℤ) with hH
 284  let g : TopCat.sphere.{0} 1 ⟶ Cpl := TopCat.ofHom core
 285  let r : Cpl ⟶ TopCat.sphere.{0} 1 := TopCat.ofHom retractToCore
 286  have hgr : g ≫ r = 𝟙 (TopCat.sphere.{0} 1) := by
 287    ext z
 288    exact retract_core z
 289  have hmap : H.map g ≫ H.map r = 𝟙 (H.obj (TopCat.sphere.{0} 1)) := by
 290    rw [← H.map_comp, hgr, H.map_id]
 291  have hzC : IsZero (H.obj Cpl) := hz
 292  have hg0 : H.map g = 0 := hzC.eq_zero_of_tgt _
 293  have hid0 : 𝟙 (H.obj (TopCat.sphere.{0} 1)) = 0 := by
 294    rw [← hmap, hg0, zero_comp]
 295  have hzS1 : IsZero (H.obj (TopCat.sphere.{0} 1)) :=
 296    (IsZero.iff_id_eq_zero _).mpr hid0
 297  have hzZ : IsZero (ModuleCat.of ℤ ℤ) := hzS1.of_iso e.symm
 298  have hsub : Subsingleton ℤ := ModuleCat.isZero_of_iff_subsingleton.mp hzZ
 299  exact one_ne_zero (hsub.elim (1 : ℤ) 0)
 300
 301/- Axioms audit (2026-07-17, `#print axioms` on the built module):
 302`unknotComplementH1_ne_zero`, `unknot_isEmbedding`, `retract_comp_core` each
 303depend only on `[propext, Classical.choice, Quot.sound]`. No `sorry`, no new
 304axioms, no `native_decide`. -/
 305
 306end UnknotComplementRetract
 307end Foundation
 308end IndisputableMonolith
 309