constantSingularTwoSimplex_face
plain-language theorem explainer
Every face of the constant singular 2-simplex at a point p on S¹ equals the constant singular 1-simplex at p. Homology and chain-complex arguments on the circle cite this when reducing degenerate boundaries. The proof is a short term argument: injectivity of the singular-set equivalence, definitional unfolding of face maps and constants, then pointwise reflexivity.
Claim. For every point $p$ on $S^1$ and every face index $i\in\{0,1,2\}$, the $i$-th face operator $\delta_i$ applied to the constant singular $2$-simplex at $p$ yields the constant singular $1$-simplex at $p$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for any singular $2$-simplex $F$, $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$. That identity, with the generator sending the once-around loop to $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Here $S^1$ is the carrier of TopCat.sphere 1. The constant singular $1$- and $2$-simplices are the continuous maps that send the standard simplices $\Delta^1$ and $\Delta^2$ to a fixed point $p$. Faces of a singular $2$-simplex are compositions with the affine face maps $\Delta^1\to\Delta^2$ induced by the cofaces $\delta_i:[1]\to[2]$ in the simplex category.
This lemma records the fully degenerate case: every face of a constant $2$-simplex is the matching constant $1$-simplex.
proof idea
Work under the equivalence identifying singular simplices with continuous maps out of standard simplices. Apply injectivity of that equivalence on $1$-simplices, then unfold the definitions of the constant $2$- and $1$-simplices, the singular-set face operator $\delta_i$, and the geometric face map. After ext on the domain point of $\Delta^1$, both sides are definitionally the constant map at $p$, so rfl finishes.
why it matters
Feeds directly into constantSingularOneSimplex_free_boundary, which states that the constant singular $1$-simplex bounds the constant singular $2$-simplex in the explicit free chain complex: the degenerate base case of the null-homotopy prism construction.
That base case is needed when building a chain-level null-homotopy for boundaries, the missing generation half toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module already has the kills-boundaries identity and the winding of the fundamental loop; prism/subdivision operators (not yet in Mathlib singular homology) close the surjectivity direction. In the Recognition foundation stack this is pure topological scaffolding for the circle's first homology, not a physics forcing step (T0–T8), but it underwrites later winding and octave arguments that sit on $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.