arcMap_injective
plain-language theorem explainer
For each sign s = ±1, the continuous semicircle arc from the unit interval into the 1-sphere is injective. High-dimensional linking-vanishing arguments cite this to promote the arc from a continuous path to an embedding. The proof reads the parameter off the first ambient coordinate and finishes by linear arithmetic on [0,1].
Claim. Let $s \in \mathbb{R}$ with $s^2 = 1$. The continuous map $[0,1] \to S^1$ given by $t \mapsto (1-2t,\, s\sqrt{1-(1-2t)^2})$ in ambient coordinates is injective.
background
The module studies vanishing of linking in high dimensions, importing singular sphere geometry and the low-dimensional linking results. Sphere points are handled via ambient coordinate extraction: for $x \in S^n$ one writes $\mathrm{amb}(x)$ for its Euclidean coordinates in the ambient space.
The semicircle arc sends $t \in [0,1]$ to the point of $S^1$ with coordinates $(1-2t,, s\sqrt{1-(1-2t)^2})$, where $s=\pm 1$ selects the upper or lower semicircle. Its continuous packaging is the map whose injectivity is claimed here. A companion identity records that the first ambient coordinate is exactly $1-2t$, so the parameter is algebraically recoverable from the image.
proof idea
Take $t,t'$ in the unit interval with equal images under the arc map. Equality of sphere points implies equality of first ambient coordinates. Rewrite both sides by the first-coordinate identity to obtain $1-2t=1-2t'$. Linear arithmetic forces $t=t'$ as reals; Subtype.ext upgrades that to equality in the unit interval, proving injectivity.
why it matters
The sole downstream consumer is the embedding lemma for the same arc: continuity plus this injectivity, in the $T_2$ space $S^1$, yields a closed embedding and hence a topological embedding. That embedded semicircle is geometric input for the high-dimensional linking-vanishing development in Foundation. Linking control feeds the dimensional side of the forcing chain (T8: three spatial dimensions), where nontrivial linking is available only in low ambient dimension. Without injectivity one would have only a continuous path, not an embedded 1-cell usable in linking or homology arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.