continuous_injective_circle_self_surjective
plain-language theorem explainer
Any continuous injection from the unit circle to itself is automatically onto. Topologists and anyone tracking low-dimensional linking use this to kill nontrivial H₁ of complements in S¹. The argument is by contradiction: a missed point yields, via stereographic projection, a continuous injection S¹ → ℝ, which is already ruled out.
Claim. Let $f_0$ be a continuous injective map from the unit circle $S^1 \subset \mathbb{R}^2$ to itself. Then $f_0$ is surjective.
background
This module is a Mathlib-only leaf that shows the linking detector fails in dimensions 0 and 1. The detector asks whether an embedded circle in $S^n$ can leave a complement with nontrivial singular homology in degree 1. In dimension 1 the ambient space is the circle itself.
The metric circle is the unit sphere in Euclidean space of dimension 2. Stereographic projection from a point $p \in S^1$ is a homeomorphism from $S^1 \setminus {p}$ onto $\mathbb{R}$. The sibling lemma no_continuous_injective_circle_to_real already records that no continuous injection $S^1 \to \mathbb{R}$ exists: removing a preimage of an interior value keeps the domain connected while splitting the image interval.
Together these facts force every continuous self-injection of $S^1$ to hit every point, so the complement of any embedded circle in $S^1$ is empty.
proof idea
Fix a continuous injection $f_0 : S^1 \to S^1$ and an arbitrary point $p$. Assume for contradiction that $p$ is missed. Stereographic projection $\varphi$ from $p$ is defined on the whole image of $f_0$. The composite $x \mapsto \varphi(f_0(x))$ is continuous into $\mathbb{R}^1$; projecting to the single coordinate gives a continuous map $g : S^1 \to \mathbb{R}$.
Injectivity of $g$ follows from injectivity of $f_0$ and of $\varphi$ on its source (the only coordinate of $\mathbb{R}^1$ is forced by subsingleton). The resulting continuous injection $S^1 \to \mathbb{R}$ contradicts the upstream lemma that no such map exists. Hence every $p$ is hit.
why it matters
The immediate parent is not_detects_one: once every continuous injection $S^1 \hookrightarrow S^1$ is known to be surjective, the complement of an embedded circle is empty, and singular homology of the empty space vanishes in degree 1. That closes the $D=1$ half of the module's claim that the linking detector fails in low dimension.
In the broader Recognition forcing chain this is the topological half of why nontrivial linking (and the associated higher-dimensional structure) cannot appear below the forced spatial dimension $D=3$ (T8). The companion not_detects_zero handles the totally disconnected $0$-sphere; together they justify that the content-typed linking object only becomes nontrivial once dimension is high enough for genuine linking.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.