windingChainMap_
plain-language theorem explainer
On each singular 1-simplex generator of the free chain module on S¹, the winding chain map acts by scalar multiplication by that simplex's winding number. Anyone building the induced map on H₁(S¹;ℤ) from the path-level winding invariant cites this componentwise evaluation. The proof is the coproduct universal-property identity for the defining descent of the chain map.
Claim. For every singular $1$-simplex $s$ on $S^1$, the composite of the coproduct inclusion of the $s$-summand of $\bigoplus_s \mathbb{Z}$ with the winding chain map equals the $\mathbb{Z}$-linear map $\mathbb{Z}\to\mathbb{R}$ sending $1$ to the winding number of $s$.
background
This module lifts the path-level winding and displacement invariant of the circle to singular simplices of $S^1$, and proves that the resulting assignment kills boundaries, so it descends to homology. A singular $1$-simplex is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$: a continuous map $\Delta^1\to S^1$. Displacement of such a simplex is obtained by reparameterizing $\Delta^1$ to the unit interval and taking path displacement; winding is the corresponding integer (displacement over $2\pi$).
The free $\mathbb{Z}$-module on those generators is presented as a coproduct of copies of $\mathbb{Z}$ indexed by singular $1$-simplices. The winding chain map is the unique morphism out of that coproduct determined by sending each generator to its winding number (as a map $\mathbb{Z}\to\mathbb{R}$). The module goal is the chain-level half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding kills boundaries, and on the fundamental loop it recovers $1$.
proof idea
One-line term proof. The winding chain map is defined by descent out of the coproduct of $\mathbb{Z}$-copies indexed by singular $1$-simplices. Applying the coproduct inclusion-desc identity at the component $s$ immediately yields that the composite of the $s$-inclusion with the chain map equals the span-singleton map of the winding number of $s$.
why it matters
This is the generator-wise evaluation clause for the winding chain map: without it, one cannot read off that the induced homology map sends the class of a singular $1$-cycle to the sum of its coefficients times winding numbers. Together with the kills-boundaries identity (alternating face displacements of every singular $2$-simplex vanish by telescoping inside the convex $\Delta^2$) and the normalization that the once-around loop has winding $1$, it supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
In the Recognition foundation stack this is the singular-homology packaging of the circle winding used by the eight-tick and octave arguments: an integer-valued invariant on $1$-cycles that is a left inverse to the fundamental class. The converse generation half (every cycle homologous to an integer multiple of the fundamental cycle) still needs a prism or subdivision operator that Mathlib singular homology does not yet supply; this lemma does not close that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.