SphereOneAmbient
plain-language theorem explainer
Names the ambient Euclidean plane R^2 (as Mathlib's EuclideanSpace over Fin 2) that hosts the metric unit circle for TopCat.sphere 1. Anyone building circle coverings, basepoints, or singular simplices in the Foundation circle-H1 stack cites this type. The body is a one-line type abbreviation with no proof content.
Claim. Write $S^1_{\mathrm{amb}}$ for the Euclidean plane $\mathbb{R}^2$ with the standard $\ell^2$ structure, i.e. $\mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,2)$. This is the ambient metric space in which Mathlib's unit circle (the carrier of $\mathrm{TopCat.sphere}\,1$) is realized as the sphere of radius $1$ about the origin.
background
The module begins a by-hand circle-$H_1$ derivation against the imported object TopCat.sphere 1. It fixes the exact carrier, a checked basepoint, and the constant singular 1-simplex face identities inside TopCat.toSSet.obj (TopCat.sphere 1). The constant simplex is only an API anchor: later once-around simplices must live in the same singular simplicial set and use the same face maps.
Mathlib realizes the topological 1-sphere as the metric sphere of radius 1 about the origin in a two-dimensional Euclidean space. That host space is EuclideanSpace R (Fin 2), the $\ell^2$ product of two real lines indexed by Fin 2. Downstream definitions (base vector, trigonometric parametrization, covering isometry from Circle) all type against this ambient plane.
proof idea
Pure type abbreviation: the right-hand side is Mathlib's EuclideanSpace R (Fin 2). No lemmas, tactics, or obligations.
why it matters
This is the shared ambient type for the whole Foundation circle stack. Downstream it appears in the orthonormal isometry isoE : C ≃ₗᵢ[R] SphereOneAmbient, the homeomorphism from Mathlib's Circle onto the exact metric carrier, the identity that the carrier covering equals the ambient trigonometric vector (cos t, sin t), continuity of that parametrization, and the first-coordinate unit base vector with its membership on the unit sphere.
Without a single named ambient plane, the metric sphere carrier, the complex-to-R^2 isometry, and the singular-set face maps would not share a common type. The module's goal is the circle-$H_1$ generator against the real TopCat.sphere 1 object; this abbrev is the first concrete type pin in that chain. It is foundation infrastructure rather than a forcing-chain (T0-T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.