retract_comp_core
plain-language theorem explainer
The retraction of the unknot complement in S³ onto the dual circle, composed with the dual-circle inclusion, is the identity continuous map on S¹. Anyone proving that H₁ of the unknot complement is nontrivial via a retract argument cites this identity. The proof is pointwise extensionality plus the already-proved pointwise retraction lemma.
Claim. Let $S^1$ and $S^3$ be the unit spheres. Let the dual circle embed $S^1$ into the complement of the flat unknot in $S^3$ by $z \mapsto (0,0,z_0,z_1)$, and let the retraction send a complement point $y$ to the normalization of its last two coordinates. Their composition as continuous maps equals $\mathrm{id}_{S^1}$.
background
This module is a standalone Mathlib-only development of the geometric core behind nontrivial linking detection in dimension 3. It builds the flat unknot $S^1 \hookrightarrow S^3$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, proves it is a topological embedding, and works entirely in the open complement.
The dual circle ("core") lands in that complement by placing the circle in the last two coordinates: $z\mapsto(0,0,z_0,z_1)$. The retraction of the complement onto that circle normalizes the last two coordinates of a point $y$, namely $y\mapsto(y_2,y_3)/|(y_2,y_3)|$. A prior pointwise lemma already records that applying the retraction after the dual-circle inclusion recovers every point of $S^1$.
The present statement lifts that pointwise fact to an equality of continuous maps on the sphere object used by singular homology later in the file.
proof idea
Term-mode proof by continuous-map extensionality: reduce equality of maps $S^1\to S^1$ to agreement at each point $z$, then invoke the pointwise identity that the retraction along the dual circle returns $z$. No further topology is needed; continuity and well-definedness of both maps are already established upstream.
why it matters
This is the continuous-map form of "core is a section of the retraction," which the capstone theorem unknotComplementH1_ne_zero needs. That capstone argues that $H_1(S^1;\mathbb{Z})$ is a retract of $H_1$ of the unknot complement, hence the latter cannot be the zero object once $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is supplied.
In the broader Recognition spine this geometric package is the concrete witness behind DetectsNontrivialLinking in dimension 3: a nontrivial $H_1$ of a link complement is the topological signature that linking is detected. The module deliberately stays universe-0 and Mathlib-shaped so it can glue to the public linking-complement homology interface elsewhere without importing the rest of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.