Foundation Unknot Complement Retract Part23 Continuous

The continuous projection

In topology, a retraction is a continuous map from a space onto a subspace that leaves every point of that subspace fixed. The declaration part23_continuous establishes one piece of such a retraction: the map that takes a point in four-dimensional space and keeps only its last two coordinates is continuous. This is not a deep fact on its own; it follows from the general principle that coordinate projections from a finite-dimensional Euclidean space are continuous. But it is the load-bearing step in a larger construction.

The construction concerns the complement of an unknot in the three-dimensional sphere. An unknot is the simplest possible loop, a circle embedded in space without any twisting or knotting. In the standard model used here, the unknot sits in the first two coordinates of four-dimensional space, while the remaining two coordinates are left free. The complement is everything in the three-sphere that is not on that circle. The object core is a second circle, placed in the free coordinates, and retractToCore is a continuous map from the complement onto that core circle. The map works by taking the last two coordinates of a point, normalizing them to unit length, and forgetting the rest.

The theorem retract_comp_core proves that this retraction really is a retraction: when you apply it to a point already on the core circle, you get that same point back. The lemma part23_continuous is what guarantees the normalization step is continuous, since dividing by a nonzero norm is continuous exactly when the projection that produces the norm is continuous. Without this lemma, the whole retraction would not be a continuous map, and the topological argument would collapse.

The payoff is a nontrivial fact about the complement: its first singular homology group is not zero. In plain terms, the complement of an unknot in the three-sphere has a hole that a loop can wrap around, and that hole is detected by the core circle. This is the geometric core of DetectsNontrivialLinking, a separate claim about linking in three dimensions. The declaration does not itself prove that the unknot is nontrivial, nor does it show that any other knot has a nontrivial complement. It only supplies the continuous projection needed for one specific retraction.

lemma part23_continuous : Continuous part23 :=
  proj23_continuous.comp
    (continuous_subtype_val.comp (continuous_uliftDown.comp continuous_subtype_val))

theorem retract_comp_core :
    (retractToCore.comp core) = ContinuousMap.id (TopCat.sphere.{0} 1) := by
  ext z
  exact retract_core z

/-- **Capstone.** Given that first singular homology of S¹ with ℤ coefficients
is ℤ (as an iso in `ModuleCat ℤ`), the first singular homology of the unknot
complement in S³ is not the zero object. Pure retraction argument: `core` and
`retractToCore` exhibit H₁(S¹) as a retract of H₁(complement). -/
theorem unknotComplementH1_ne_zero
    (h1 : Nonempty ((((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
      (ModuleCat.of ℤ ℤ)).obj (TopCat.sphere.{0} 1)) ≅ ModuleCat.of ℤ ℤ)) :
    ¬ CategoryTheory.Limits.IsZero
      (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
        (ModuleCat.of ℤ ℤ)).obj (TopCat.of {x : TopCat.sphere.{0} 3 // x ∉ Set.range unknot})) := by
  intro hz
  obtain ⟨e⟩ := h1
  set H : TopCat.{0} ⥤ ModuleCat ℤ :=
    (AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj (ModuleCat.of ℤ ℤ) with hH
  let g : TopCat.sphere.{0} 1 ⟶ Cpl := TopCat.ofHom core
  let r : Cpl ⟶ TopCat.sphere.{0} 1 := TopCat.ofHom retractToCore
  have hgr : g ≫ r = 𝟙 (TopCat.sphere.{0} 1) := by
    ext z
    exact retract_core z
  have hmap : H.map g ≫ H.map r = 𝟙 (H.obj (TopCat.sphere.{0} 1)) := by
    rw [← H.map_comp, hgr, H.map_id]
  have hzC : IsZero (H.obj Cpl) := hz
  have hg0 : H.map g = 0 := hzC.eq_zero_of_tgt _
  have hid0 : 𝟙 (H.obj (TopCat.sphere.{0} 1)) = 0 := by
    rw [← hmap, hg0, zero_comp]
  have hzS1 : IsZero (H.obj (TopCat.sphere.{0} 1)) :=
    (IsZero.iff_id_eq_zero _).mpr hid0
  have hzZ : IsZero (ModuleCat.of ℤ ℤ) := hzS1.of_iso e.symm
  have hsub : Subsingleton ℤ := ModuleCat.isZero_of_iff_subsingleton.mp hzZ
  exact one_ne_zero (hsub.elim (1 : ℤ) 0)

/- Axioms audit (2026-07-17, `#print axioms` on the built module):
`unknotComplementH1_ne_zero`, `unknot_isEmbedding`, `retract_comp_core` each
depend only on `[propext, Classical.choice, Quot.sound]`. No `sorry`, no new
axioms, no `native_decide`. -/

What this page does not claim

This declaration does not prove that the unknot is a nontrivial knot. It does not establish the continuity of any projection other than the one onto the last two coordinates. It does not show that the complement of any other knot has nonzero first homology.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/UnknotComplementRetract.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: