windingHomologyMap
plain-language theorem explainer
The winding number of singular 1-simplices on the circle induces a homomorphism H₁(S¹;ℤ) → ℝ on first singular homology. Anyone proving that the fundamental class has infinite order, or that H₁(S¹) is nonzero, cites this map as the retraction. It is the canonical descent of the chain-level winding map through opcycles, using that the map annihilates ∂₂.
Claim. The chain-level winding map $W: C_1(S^1;\mathbb{Z})\to\mathbb{R}$ annihilates every degree-$2$ boundary, so it factors uniquely through the degree-$1$ opcycles and induces a homomorphism $H_1(S^1;\mathbb{Z})\to\mathbb{R}$.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices of TopCat.sphere 1 and proves the single identity that makes winding a homology invariant. Each singular $1$-simplex gets a real displacement ($2\pi$ times winding) by reparameterizing $\Delta^1$ to the unit interval; the key chain-level fact is that the alternating face sum of displacements on any singular $2$-simplex vanishes (telescoping via convexity of $\Delta^2$ and homotopy invariance of path displacement).
The ambient complex is Mathlib's singular chain complex of the topological $1$-sphere with integer coefficients: its degree-$1$ homology is the strict T8 target object. The chain-level winding map $W: C_1(S^1;\mathbb{Z})\to\mathbb{R}$ sends each free generator (a singular $1$-simplex) to $n$ times its winding number. The theorem that $W\circ\partial_2=0$ is exactly the kills-boundaries identity needed to descend $W$ to homology.
proof idea
Categorical one-liner. Compose the canonical map from homology into the opcycle object (homologyι in degree $1$) with the unique morphism out of opcycles induced by the chain-level winding map (descOpcycles). The boundary-vanishing hypothesis fed to descOpcycles is precisely windingChainMap_boundary ($W\circ\partial_2=0$); a simp discharges the degree bookkeeping. No new geometric content is proved here: the geometry lives in the kills-boundaries theorem.
why it matters
This is the homology-level winding homomorphism that turns the chain-level invariant into a map on $H_1(S^1;\mathbb{Z})$. Downstream, its composite with the fundamental-class comparison $\mathbb{Z}\to H_1$ is the standard inclusion $n\mapsto n\cdot 1$, so winding is a retraction of the fundamental class. That immediately yields monomorphicity of the fundamental class (injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$) and unconditional nonvanishing of $H_1$ (were homology zero, the composite would force $1=0$ in $\mathbb{R}$).
Injectivity of this winding map itself is the remaining hypothesis that closes the full integer isomorphism and builds the Mathlib circle-linking backend used by the strict T8 replacement. Generation (surjectivity of the fundamental-class map) is still open and needs a prism/subdivision operator Mathlib does not yet supply; nonvanishing for the T-frontier does not require it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.