amb_injective
plain-language theorem explainer
The ambient-coordinate map from the unit n-sphere into Euclidean space is injective for every n. Anyone equating sphere points by comparing coordinates, or reducing sphere identities to vector identities, cites this. The proof is a one-line subtype extensionality: equal ambient vectors are equal as sphere points.
Claim. For every $n \in \mathbb{N}$, the map sending a point of the unit sphere $S^n \subset \mathbb{R}^{n+1}$ to its ambient Euclidean coordinates is injective.
background
The ambient space Esp n is Euclidean space $\mathbb{R}^{n+1}$ (indexed by Fin (n+1)). The sphere Sph n is the unit sphere in that space, realized as a topological space (subtype of unit-norm vectors). The helper amb is the coercion that forgets the unit-norm proof and returns the underlying vector in Esp n; the module doc frames it as a coercion helper across TopCat.of.
Working with charts, poles, and arcs on $S^n$ routinely requires comparing points by their coordinates. Injectivity of this coercion is the formal bridge: if two sphere points have the same ambient vector, they are definitionally the same point of the subtype.
proof idea
Term-mode one-liner. Given amb x = amb y, apply Subtype.ext to conclude x = y. No further lemmas are needed; the statement is pure subtype extensionality for the unit-sphere subtype.
why it matters
Local geometry lemmas on the singular sphere package depend on equating points via coordinates. Downstream, sph0_eq_pole classifies $S^0$ as the two poles by reading the single ambient coordinate; coord_zero_ne_zero shows the first coordinate never vanishes on the doubly punctured circle. In LinkingVanishingHighDim, arcFun_arcParam recovers a circle point from its arc parameter by applying this injectivity after an ambient identity, and the two semicircle ranges meet exactly at the east and west points. The lemma is pure differential-topology scaffolding inside the Foundation layer that supports linking-vanishing arguments; it does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.