constantSphereOneSingularZeroSimplex
plain-language theorem explainer
Defines the constant singular 0-simplex on the Mathlib circle S¹, pinned at the chosen basepoint. Anyone proving face identities for singular 1-simplices in TopCat.toSSet.obj(S¹) cites it as the common endpoint. Construction is the inverse of the singular-set equivalence applied to the constant continuous map at that basepoint.
Claim. Let $S^1$ be the topological 1-sphere. The constant singular $0$-simplex is the point of the singular simplicial set of $S^1$ in degree $0$ corresponding to the continuous map $\Delta^0 \to S^1$ with constant value equal to the chosen basepoint of $S^1$.
background
The module builds circle $H_1$ primitives against Mathlib's actual TopCat.sphere 1, not a hand-rolled model. It fixes the carrier, a checked basepoint, and the constant singular simplices that live in TopCat.toSSet.obj (TopCat.sphere 1). The constant simplex is an API anchor only: later once-around generators must sit in the same singular set and use the same face maps.
The basepoint is the image of the ambient Euclidean vector that lies on the unit sphere in $\mathbb{R}^2$, lifted into the TopCat sphere object. A singular $0$-simplex is a continuous map from the standard $0$-simplex (a point) into the space; under the Mathlib equivalence toSSetObjEquiv, that is exactly a point of the singular set in degree $0$.
Upstream face machinery (simplicial face maps and topological face inclusions of standard simplices) is what later theorems apply to 1-simplices whose endpoints are identified with this constant $0$-simplex.
proof idea
Definitional construction, not a proof. Transport the constant continuous map $\Delta^0 \to S^1$ with value the sphere basepoint across the inverse of Mathlib's equivalence between singular $0$-simplices and continuous maps out of the standard $0$-simplex. The body is that single symm application; no tactics.
why it matters
This is the shared endpoint for every face identity in the circle singular-set API. Downstream, both faces of the constant singular 1-simplex reduce to it by rfl, and both faces of the fundamental (once-around) singular 1-simplex equal it: $\delta_0$ and $\delta_1$ land on the basepoint, so the generator is a closed loop in $S^1$.
That closed-loop identity is the first concrete step of the by-hand circle-$H_1$ derivation against the imported sphere object. In the broader Recognition stack it supplies the topological side of the eight-tick / octave story (period structure on the circle) without yet computing homology groups or winding numbers. Parent theorems that quote it are the four face lemmas in CircleParam and CircleFundamentalSimplex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.