constantSphereOneSingularOneSimplex_face_zero
plain-language theorem explainer
The 0-face of the constant singular 1-simplex on $S^1$ equals the constant basepoint 0-simplex in the singular simplicial set of $\mathrm{TopCat.sphere}\,1$. Anyone wiring face identities for the circle-$H_1$ setup cites this. The proof is pure definitional equality (`rfl`).
Claim. In the singular simplicial set of the topological 1-sphere, the face map $\delta_0$ applied to the constant singular 1-simplex at the chosen basepoint equals the constant singular 0-simplex at that same basepoint.
background
The module builds circle-parametrization primitives against the imported TopCat.sphere 1 object: exact carrier, a checked basepoint, and constant singular simplex face identities inside TopCat.toSSet.obj (TopCat.sphere 1). The constant simplex is an API anchor, not the fundamental winding generator; later once-around simplices must live in the same singular set and use the same face maps.
The constant singular 1-simplex is the continuous map that sends the standard 1-simplex constantly to the sphere basepoint, transported into the singular set via the standard equivalence. The constant singular 0-simplex is the analogous constant map on the 0-simplex. Face operators $\delta_i$ are the simplicial face maps of that singular set (skipping vertex $i$).
proof idea
One-line definitional proof: rfl. Both sides reduce to the same constant continuous map at the basepoint after unfolding the singular-set equivalence and the face operator on a constant simplex, so no further lemmas are required.
why it matters
Feeds constantSphereOneSingularOneSimplex_faces_eq, which states that the two faces of the constant singular 1-simplex coincide (by rewriting with this identity and its right-face twin). That pair of face facts is the first checked anchor in the by-hand circle-$H_1$ derivation: every later winding simplex is required to sit in the same singular simplicial set of $S^1$ and to interact with the same $\delta$ maps. Without a verified constant-simplex face calculus, the comparison between constant and once-around chains cannot be stated inside the imported Mathlib singular-set API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.