windingChainMap_singularOneChainFreeToChain_freeMk
plain-language theorem explainer
On a free generator corresponding to one singular 1-simplex of S¹, the winding chain map recovers exactly that simplex's winding number. Anyone assembling the integer-valued winding homomorphism on C₁(S¹;ℤ), or checking it on elementary chains, cites this. The proof rewrites the free-to-chain map on generators, then applies the coproduct-component formula for the winding map and simplifies the span-singleton evaluation.
Claim. Let $s$ be a singular $1$-simplex of $S^1$. Transporting the free generator indexed by $s$ into the singular chain group $C_1(S^1;\mathbb{Z})$ and then applying the winding chain map $W:C_1(S^1;\mathbb{Z})\to\mathbb{R}$ yields exactly 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 that winding kills boundaries, the 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 defined by reparameterizing $\Delta^1$ to the unit interval and taking path winding.
The free $\mathbb{Z}$-module on singular $1$-simplices maps to $C_1(S^1;\mathbb{Z})$ by sending each free generator to the matching coproduct summand generator. The winding chain map $W$ is the coproduct descent that, on the summand for $s$, is $n\mapsto n\cdot(\text{winding of }s)$. Upstream, the free-to-chain map on a free generator is exactly that coproduct inclusion applied to $1$.
proof idea
Short rewrite proof. First apply the free-to-chain evaluation on free generators, replacing the composite with the coproduct inclusion $\iota_s$ applied to $1$. Rephrase the goal as evaluating $\iota_s\gg W$ at $1$. Then use the component formula for the winding chain map on coproduct inclusions, which identifies that composite with the span-singleton map for $\mathrm{singularWinding}(s)$. A final simp on LinearMap.toSpanSingleton_apply yields the scalar $1\cdot\mathrm{singularWinding}(s)$.
why it matters
This is the generator-level normalization of the winding chain map: $W$ on the raw chain of one free edge is the geometric winding of that edge. Downstream it feeds the finite-sum extension (winding of a free edge-family is the sum of windings) and the oriented-edge version (winding of an oriented singular edge equals its oriented winding). Those statements assemble winding on oriented cyclic families, the concrete closed walks used toward the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
In the module's program, together with the fundamental-loop evaluation (once-around maps to $1$) and the kills-boundaries identity, this supplies the left-inverse half of the integer comparison map. The converse generation half still needs a simplicial prism/subdivision operator not yet in Mathlib. No Recognition forcing-chain step (T0–T8) is invoked here; the result is pure singular-homology infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.