windingChainMap_fundamental
plain-language theorem explainer
The winding chain map sends the once-around fundamental singular 1-chain of S¹ to the real number 1. Anyone proving that the fundamental class has infinite order in H₁(S¹;ℤ), or that winding is a left inverse to the integer comparison map, cites this identity. The proof is a short rewrite unfolding the coproduct inclusion and applying the path-level fact that the fundamental simplex has winding 1.
Claim. Composing the degree-1 singular chain that selects the once-around fundamental 1-simplex of $S^1$ with the winding chain map $W\colon C_1(S^1;\mathbb{Z})\to\mathbb{R}$ yields the standard inclusion $\mathbb{Z}\to\mathbb{R}$, $n\mapsto n\cdot 1$. Equivalently, $W$ evaluates to $1$ on the fundamental cycle.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$. The displacement of a singular 1-simplex is obtained by reparameterizing $\Delta^1$ to the unit interval and taking path displacement; dividing by $2\pi$ gives the winding number. The key chain-level fact is that winding annihilates every degree-2 boundary (the alternating face sum on any singular 2-simplex vanishes by telescoping inside the convex standard simplex).
The winding chain map $W$ is the $\mathbb{Z}$-linear map on free generators that multiplies the coefficient of each singular 1-simplex by that simplex's winding number. The fundamental singular 1-chain is the coproduct summand inclusion picking the once-around generator. Upstream, singularWinding_fundamentalSimplex records that this generator has winding exactly 1, matching the path-level evaluation of the fundamental loop.
proof idea
Three rewrites. Unfold the fundamental singular 1-chain as the coproduct inclusion of the fundamental simplex. Apply the component formula for the winding chain map on a summand inclusion (it returns the span map of that simplex's winding). Finish with the already-proved identity that the fundamental singular 1-simplex has winding number 1, so the composite is the span map of $1$.
why it matters
This is the normalization half of the split-injective story for $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Paired with the boundary-killing identity, it lets winding descend to a homology map $H_1(S^1;\mathbb{Z})\to\mathbb{R}$ that is a left inverse of the integer comparison map $n\mapsto n\cdot[\mathrm{fundamental}]$, so distinct multiples of the fundamental class are never homologous.
Downstream it feeds the cycle-level evaluation (winding of $n$ times the fundamental cycle equals $n$), the homology-level retraction identity, and the conditional boundary-generation theorem that fills zero-winding cycles once integral winding is assumed. The module doc is explicit that only the injective half is closed here: surjectivity (every 1-cycle homologous to an integer multiple of the fundamental cycle) needs a simplicial prism or barycentric subdivision operator that Mathlib's singular homology does not yet supply. In the broader Recognition foundation this pins the topological generator used when circle windings and eight-tick octave structure interface with homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.