windingChainMap
plain-language theorem explainer
The winding chain map is the unique ℤ-linear map W : C₁(S¹;ℤ) → ℝ sending each free generator indexed by a singular 1-simplex s to its real winding number. Anyone building the homology-level winding invariant on cycles of the circle cites it. The definition is the coproduct descent of the span-singleton maps n ↦ n·w(s) over all singular 1-simplices.
Claim. Define the winding chain map $W : C_1(S^1;\mathbb{Z}) \to \mathbb{R}$ as the unique $\mathbb{Z}$-module homomorphism that, on the free generator indexed by a singular $1$-simplex $s$ of $S^1$, acts by $n \mapsto n \cdot w(s)$, where $w(s)\in\mathbb{R}$ is the winding number of $s$.
background
This module lifts the path-level winding/displacement invariant on the circle to singular simplices of $\mathrm{TopCat.sphere},1$, and proves the kills-boundaries identity that makes winding a homology invariant. A singular $1$-simplex is an element of the singular simplicial set of $S^1$ in degree $1$. Its winding number is obtained by reparameterizing the standard $1$-simplex to the unit interval and reading off path displacement (equivalently $2\pi$ times winding).
The domain of the map is degree $1$ of Mathlib's singular chain complex of $S^1$ with integer coefficients: the free $\mathbb{Z}$-module on singular $1$-simplices. That complex is the exact chain-level object whose $H_1$ is the target of the circle computation in this foundation layer. The codomain is $\mathbb{R}$ viewed as a $\mathbb{Z}$-module.
Upstream, each concrete singular $1$-simplex already carries a real winding via the simplex-level displacement construction; the chain map packages those values into one linear map on the whole free module.
proof idea
Pure definition, not a proof. The degree-$1$ chains are a coproduct (sigma) of $\mathbb{Z}$ copies indexed by singular $1$-simplices. The map is Limits.Sigma.desc of the family that, for each simplex $s$, sends the corresponding summand via the span-singleton linear map $n \mapsto n \cdot w(s)$, where $w(s)$ is the already-defined singular winding of $s$. No further lemmas are applied at this site.
why it matters
This is the chain-level packaging of winding that every cycle-level and homology-level statement in the module applies. Downstream, cycle winding is defined by including a $1$-cycle into $C_1$ and composing with this map; the fundamental cycle is shown to have winding equal to its integer coefficient; closed singular generator cycles evaluate as coefficient times simplex winding; and zero-winding residuals after subtracting the matching multiple of the fundamental cycle are constructed from it.
Together with the kills-boundaries identity (alternating face displacements of every $2$-simplex vanish) and the fact that the once-around generator has winding $1$, it supplies the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is a split injection on homology. The module doc is explicit that 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 provide. In the Recognition foundation stack this is the concrete chain map behind the circle $H_1$ computation feeding the forcing chain's topological side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.