constantSphereOneSingularOneSimplex_face_one
plain-language theorem explainer
The right face map of the constant singular 1-simplex on the topological 1-sphere lands on the constant basepoint 0-simplex. Anyone building singular homology of S^1 against Mathlib's TopCat.sphere 1 cites this as the right-face half of the constant-simplex face identities. The proof is definitional equality (rfl).
Claim. In the singular simplicial set of the topological 1-sphere, the face map $\delta_1$ applied to the constant singular 1-simplex at the chosen basepoint equals the constant singular 0-simplex at that same basepoint.
background
This module begins a by-hand derivation of $H_1(S^1)$ against Mathlib's actual TopCat.sphere 1, rather than an abstract circle model. It fixes the carrier, a checked basepoint, and the constant singular 1-simplex inside TopCat.toSSet.obj (TopCat.sphere 1). The constant simplex is an API anchor only: later once-around generators must live in the same singular simplicial set and use the same face maps.
The constant singular 1-simplex is the continuous map from the standard 1-simplex that sends everything to the sphere basepoint; the constant 0-simplex is the analogous point map. Face maps $\delta_i$ of a singular simplicial set restrict a simplex along the $i$-th face inclusion of the standard simplex. For a constant map, every face is again the constant map at the same point, so the identities are definitional once the constructions are aligned.
proof idea
One-line rfl. Both sides reduce, by unfolding the constant 1-simplex, the constant 0-simplex, and the singular face operator, to the same continuous constant map at the basepoint, so the equality is by definition.
why it matters
Feeds the sibling theorem that the two faces of the constant singular 1-simplex coincide: that result rewrites the left face via the matching left-face identity and this right-face identity, then closes. Together they certify that the constant 1-simplex is a singular 1-cycle (boundary zero) in the actual singular complex of $S^1$.
In the Recognition Science foundation stack this is scaffolding for a checked circle parametrization, not yet the fundamental generator of $H_1$. The module doc is explicit: the constant simplex is the first API anchor so that later once-around simplices share face maps and ambient singular set. No forcing-chain landmark (T5–T8, RCL, $\varphi$) is touched here; the link is topological hygiene for later recognition calculus on the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.