SphereOneCarrier
plain-language theorem explainer
Names the exact unit circle in the Euclidean plane as the underlying point-set of Mathlib's topological 1-sphere. Anyone building covering maps, winding numbers, or singular H1 on TopCat.sphere 1 cites this carrier. The body is a one-line type abbreviation for the metric sphere of radius 1 about the origin in R^2.
Claim. Write $S^1_{\mathrm{car}}$ for the metric unit sphere $\{ x \in \mathbb{R}^2 : \|x\| = 1 \}$ in the ambient Euclidean plane that underlies Mathlib's $\mathrm{TopCat.sphere}\,1$ (after the standard $\mathrm{ULift}$).
background
The module builds a by-hand circle parametrization against the imported TopCat.sphere 1 object. It needs an exact carrier type, a checked basepoint, and 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.
The ambient space is the Euclidean plane $\mathbb{R}^2$ (as EuclideanSpace R (Fin 2)). Mathlib's topological sphere is built as a metric sphere in that ambient space, then lifted. The present abbreviation pins the unlifted carrier: the set of points at distance 1 from the origin.
Upstream, the ambient type is already fixed as that Euclidean plane. Downstream covering and homeomorphism constructions transport Mathlib's multiplicative Circle and the real-line exponential onto this carrier before lifting into TopCat.sphere 1.
proof idea
Pure definitional abbreviation. The right-hand side is Mathlib's Metric.sphere applied to the zero vector of the ambient Euclidean plane at radius 1. No lemmas or tactics; the name is a type alias for that subtype.
why it matters
This carrier is the concrete point-set that every later circle covering and winding argument in the foundation stack lands on. circleHomeoCarrier builds the homeomorphism from Mathlib's Circle onto it; carrierCovering is the real-line covering map into it; ulift_carrierCovering_eq_trig equates the lifted covering with the trigonometric parametrization of TopCat.sphere 1; and isCoveringMap_trigCirclePoint records that the trig map is a covering map, the foundation for the winding/degree invariant on singular 1-chains. Surjectivity of the trig map (trigCirclePoint_surjective) also routes through this type.
In the Recognition Science forcing chain the eight-tick octave (T7) and the circle's fundamental class sit on this same singular simplicial set. Pinning the carrier to the exact metric sphere under the ULift keeps the H1 derivation honest against Mathlib's imported sphere rather than a parallel hand-rolled model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.