constantSingularOneSimplex_faces_eq
plain-language theorem explainer
The two face maps of a constant singular 1-simplex on S¹ agree, so that simplex is closed as a singular chain. Anyone building the winding homomorphism on C₁(S¹) or checking that constant loops are null-homologous cites this. The proof reduces through the singular-set equivalence and finishes by reflexivity of the constant continuous map.
Claim. For every point $p$ on $S^1$, the two face operators $\delta_0$ and $\delta_1$ applied to the constant singular $1$-simplex at $p$ yield the same singular $0$-simplex. Equivalently, the constant singular $1$-simplex is a closed $1$-chain.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of the exact Mathlib object $S^1 = \mathrm{TopCat.sphere},1$, and proves that winding kills boundaries. The carrier type is abbreviated SphereOne.
A singular $1$-simplex is a continuous map $\Delta^1 \to S^1$. The constant singular $1$-simplex at $p$ is the continuous map sending every point of the standard $1$-simplex to $p$, transported into the singular set via the standard equivalence TopCat.toSSetObjEquiv.
Face operators $\delta_i$ on the singular simplicial set extract the $i$-th face. For a $1$-simplex the two faces are the endpoint $0$-simplices. A $1$-simplex is closed (a cycle) precisely when those two faces coincide, so that the alternating boundary $\partial_1 = \delta_0 - \delta_1$ vanishes.
proof idea
Apply injectivity of the equivalence identifying singular $0$-simplices with continuous maps $\Delta^0 \to S^1$. Unfold the definitions of the constant singular $1$-simplex, the singular-set functor, face maps, and the homeomorphism congruence on continuous maps. After ext on the unique point of $\Delta^0$, both sides are definitionally the constant map at $p$, so rfl closes the goal.
why it matters
This is the elementary closedness fact needed before constant loops can enter the chain-level story. Downstream, constantSingularOneCycle_bounds uses it to package the constant $1$-simplex as a genuine cycle and exhibit an explicit $2$-chain (the constant $2$-simplex) bounding it.
In the broader module program this supports the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$: the winding chain map $W : C_1(S^1) \to \mathbb{R}$ annihilates boundaries and sends the fundamental cycle to $1$, so the comparison $\mathbb{Z} \to H_1$, $n \mapsto n\cdot[\mathrm{fundamental}]$, has a left inverse. The generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) remains open pending a simplicial prism/subdivision operator not yet in Mathlib singular homology. No axioms or sorry are used.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.