unknot_isEmbedding
plain-language theorem explainer
The standard flat unknot S¹→S³, (x₀,x₁)↦(x₀,x₁,0,0), is a topological embedding. Anyone citing the geometric half of DetectsNontrivialLinking in dimension 3 needs this fact: the map must be an embedding before its complement's H₁ can be discussed. The proof is a one-line Mathlib chain: continuous injective map from a compact space into a Hausdorff space is a closed embedding, hence an embedding.
Claim. The continuous map $u:S^{1}\to S^{3}$ given by $u(x_{0},x_{1})=(x_{0},x_{1},0,0)$ is a topological embedding (equivalently: a continuous injection from a compact space into a Hausdorff space, hence a closed embedding).
background
This module builds the geometric core of nontrivial linking detection in dimension 3, standalone on Mathlib. The unknot is the continuous map $C(S^{1},S^{3})$ sending $(x_{0},x_{1})$ to $(x_{0},x_{1},0,0)$: the unit circle in the first two coordinates of $\mathbb{R}^{4}$, viewed on the 3-sphere.
A topological embedding is a map that is a homeomorphism onto its image. Mathlib packages the classical criterion: a continuous injection from a compact space into a Hausdorff space is a closed embedding, and every closed embedding is an embedding. Injectivity of the unknot is already proved in-module as a sibling lemma.
Downstream, linkingComplementH1 (PublicSpine) takes such an embedded circle and forms the first singular homology (ℤ coefficients, genuine Mathlib singularHomologyFunctor) of its complement in $S^{D}$. That object is what Alexander duality computes; statements about it cannot be discharged by arithmetic encodings.
proof idea
One-line term proof. Start from continuity of the unknot map (inherited from the continuous-map type). Feed injectivity (unknot_injective) into Mathlib's Continuous.isClosedEmbedding, which upgrades a continuous injection compact→Hausdorff to a closed embedding. Project with .isEmbedding to obtain Topology.IsEmbedding. No case splits and no homology.
why it matters
This is step 2 of the module's six-point program and the embedding witness required by the detection half of campaign P-d3link. Downstream, detectsNontrivialLinking_three packages the unknot, this embedding theorem, and unknotComplementH1_ne_zero into DetectsNontrivialLinking 3:
the flat unknot embeds $S^{1}$ in $S^{3}$, and its complement retracts onto the core circle, so $H_{1}(S^{1};\mathbb{Z})\cong\mathbb{Z}$ is a retract of the complement's first homology, which therefore is not zero.
The sibling capstone unknotComplementH1_ne_zero uses the embedding only indirectly (via the complement type), but the PublicSpine purchase binder lists this theorem explicitly as the second field. In the broader Recognition forcing chain this anchors the D=3 spatial case (T8): nontrivial linking is detectable precisely when the ambient sphere dimension is 3, matching the eight-tick / three-spatial-dimension package. Real singular homology throughout; no arithmetic encoding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.