windingChainMap_constantSingularOneSimplex
plain-language theorem explainer
Constant singular 1-simplices on S¹ contribute zero under the winding chain map: each is the boundary of the constant 2-simplex at the same point. Anyone computing the winding of free singular 1-chains, or assembling oriented cyclic families, cites this vanishing. The proof rewrites the free generator to a boundary, then applies the chain-level kills-boundaries identity and simplifies.
Claim. For every point $p\in S^1$, the winding chain map sends the free $\mathbb{Z}$-generator of the constant singular $1$-simplex at $p$ to $0$ in the target module.
background
This module lifts the path-level winding/displacement of CircleWinding to singular simplices of $\mathrm{TopCat.sphere},1$ and proves that winding kills boundaries. The displacement of a singular $1$-simplex is the path displacement of its reparameterization to the unit interval; the key identity is that the alternating face sum of displacements of any singular $2$-simplex vanishes (2-simplex telescoping via convexity of $\Delta^2$ and homotopy invariance of path displacement).
A constant singular $1$-simplex at $p\in S^1$ is the continuous map $\Delta^1\to S^1$ with value $p$; likewise for the constant $2$-simplex. The raw-boundary lemma identifies the free generator of that constant $1$-simplex with the image of the constant $2$-simplex under the degree-$(2\to 1)$ differential of the integer singular chain complex of $S^1$. The winding chain map is the chain-level lift of simplex winding; its composition with any boundary is zero by the kills-boundaries theorem.
Together with the fact that the once-around generator has winding $1$, this supplies the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
Term-mode rewrite proof. First apply the free-to-chain evaluation on free generators so the goal is winding of the constant $1$-simplex chain. Rewrite via the raw-boundary identity: that chain equals the image of the free generator of the constant $2$-simplex under $d_{2,1}$. Change the goal to the composite $d_{2,1}\circ\mathrm{windingChainMap}$ on that free $2$-chain. Apply the chain-map identity that winding kills boundaries (so the composite is the zero map), then simp to finish.
why it matters
Zero winding on constant edges is the base case needed when evaluating winding on finite free edge families and on oriented cyclic family terms (the sole recorded consumer). Without it, constant loops would pollute the total winding of a closed walk. In the module narrative this is part of the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is a homology invariant (kills boundaries) and sends the fundamental loop to $1$. The singular chain complex of $S^1$ is flagged as the exact chain-level object whose degree-$1$ homology is the strict T8 target in the forcing chain. The converse generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism/subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.