constantSingularTwoSimplex
plain-language theorem explainer
Defines the constant singular 2-simplex on S¹ at a basepoint p: the continuous map Δ² → S¹ with value p everywhere. Homology and free-chain arguments cite it as the degenerate filler for constant 1-cycles and equal-endpoint geodesics. Construction is the constant continuous map on the standard 2-simplex, transported by the singular simplicial-set equivalence.
Claim. For each point $p \in S^1$, write $\sigma_p : \Delta^2 \to S^1$ for the continuous map with constant value $p$. Under the identification of singular $2$-simplices of $\mathrm{TopCat.sphere}\,1$ with continuous maps from the standard $2$-simplex, $\sigma_p$ is the constant singular $2$-simplex at $p$.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$ and proves that displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\partial_0 F)-\mathrm{disp}(\partial_1 F)+\mathrm{disp}(\partial_2 F)=0$. That identity, with the generator evaluation on the once-around loop, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $2$-simplex here is an element of the degree-$2$ object of the singular simplicial set of $\mathrm{TopCat.sphere},1$, equivalently a continuous map $\Delta^2\to S^1$. Faces are obtained by precomposition with the standard face maps of $\Delta^2$. SphereOne is the carrier type of that sphere object.
Constant maps are the degenerate base case of the null-homotopy/prism constructions used later for free and raw chain boundaries.
proof idea
Definitional construction, not a proof. Take the constant continuous map $\mathrm{ContinuousMap.const},(\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},3)),p$, then apply the inverse of $\mathrm{TopCat.toSSetObjEquiv}$ at simplex degree $2$ to land in the singular simplicial set of $\mathrm{TopCat.sphere},1$. The result is noncomputable only because that equivalence and the topological simplex infrastructure are.
why it matters
Supplies the explicit $2$-chain that bounds constant $1$-simplices and degenerate geodesics in the free and raw singular chain complexes. Downstream: every face equals the constant $1$-simplex at the same point; the free boundary of the free generator on this $2$-simplex is the free generator on the constant $1$-simplex; the same holds at the cycle-object and raw-chain levels; equal-endpoint geodesic free chains bound this constant $2$-simplex; oriented cyclic family terminal-side corrections use it in the prism assembly.
In the module narrative this is the degenerate base of the "winding kills boundaries" chain, supporting the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation/surjectivity half still needs simplicial prisms and subdivision, which Mathlib singular homology does not yet provide. No direct T0–T8 forcing step; pure topological foundation for the circle winding invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.