constantSphereOneSingularOneSimplex_faces_eq
plain-language theorem explainer
The two face maps of the constant singular 1-simplex on the topological 1-sphere agree. Anyone assembling singular homology of S^1 against Mathlib's TopCat sphere would cite this as the first face-identity check. The proof is a two-line rewrite through the left- and right-face lemmas, both reducing to the constant basepoint 0-simplex.
Claim. In the singular simplicial set of the topological $1$-sphere, the two face operators $\delta_0$ and $\delta_1$ send the constant singular $1$-simplex at the chosen basepoint to one and the same singular $0$-simplex.
background
This module begins a by-hand circle-$H_1$ derivation against the imported TopCat.sphere 1 object. It fixes the exact carrier, a checked basepoint, and the constant singular 1-simplex face identities inside the singular simplicial set of that sphere. The constant simplex is not the fundamental generator; it is the first API anchor so that later once-around simplices live in the same singular set and use the same face maps.
A singular 1-simplex here is a continuous map from the standard 1-simplex into the sphere. The constant one sits at the fixed basepoint of $S^1$. Face operators $\delta_0$ and $\delta_1$ restrict that map to the two endpoints, yielding singular 0-simplices. Upstream, both faces of the constant 1-simplex are already identified with the constant 0-simplex at the same basepoint (each by rfl).
proof idea
Term-style rewrite proof. Rewrite the left-hand face via the left-face lemma (which equals the constant basepoint 0-simplex) and the right-hand face via the right-face lemma (same constant 0-simplex). Both sides become definitionally identical, so equality follows. No further simplicial identities or continuity arguments are needed.
why it matters
Closes the constant-simplex face package that the module doc names as the first API anchor for the circle-$H_1$ derivation. Downstream once-around generators are expected to inhabit the same singular simplicial set and reuse these face maps; without face agreement on the constant simplex, later boundary computations would not type-check against a single basepoint 0-simplex. No parent theorems yet cite it (used_by is empty), so it is infrastructure rather than a forcing-chain step. It does not touch T0–T8, RCL, or the phi ladder; it is pure topological scaffolding for the Recognition circle parametrization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.