constantSingularOneSimplex
plain-language theorem explainer
Constant singular 1-simplex on S¹ at a chosen point p: the degenerate map sending all of Δ¹ to p. Cited as the base case whenever winding or boundary identities are checked on constant chains. Construction is transport of ContinuousMap.const along the singular-set equivalence for TopCat.sphere 1.
Claim. For each point $p\in S^1$, there is a singular $1$-simplex given by the constant continuous map $\Delta^1\to S^1$ with value $p$, viewed as an element of the singular simplicial set of the topological circle.
background
The module lifts the path-level winding and displacement invariants of CircleWinding to singular simplices of the actual Mathlib object TopCat.sphere 1, and proves that displacement vanishes on boundaries. That vanishing is the chain-level fact making winding a homology invariant, and with the generator evaluation it supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex here is an object of the singular simplicial set of the circle in degree $1$, equivalently a continuous map from the standard $1$-simplex $\Delta^1=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$ into $S^1$. The carrier type of that circle is abbreviated SphereOne. Constant maps are the degenerate base of every later boundary and prism identity in the module.
proof idea
Pure definition, not a proof. Take the constant continuous map from the standard real $1$-simplex to the point $p$, then apply the inverse of the singular-set object equivalence TopCat.toSSetObjEquiv in degree $1$. The result is the corresponding element of the singular simplicial set of the circle. No lemmas are invoked beyond that equivalence and ContinuousMap.const.
why it matters
Supplies the degenerate generator used throughout the winding-chain development. Downstream: every face of the constant $2$-simplex is this constant $1$-simplex; the two faces of the constant $1$-simplex agree (it is closed); it bounds the constant $2$-simplex in both the free and raw chain complexes; the constant closed $1$-cycle bounds at the cycle-object level; and the map-based constructor agrees with this definition on constant maps. The free-boundary theorem calls it the degenerate base case of the null-homotopy prism construction that underpins simplexDisplacement_boundary (winding kills boundaries). That identity, with the once-around generator evaluation, is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in the module doc. Surjectivity still needs a simplicial prism or subdivision operator Mathlib does not yet provide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.