cycleWinding
plain-language theorem explainer
Assigns a real winding number to every singular 1-cycle on S¹ by including the cycle into C₁(S¹;ℤ) and applying the winding chain map. Anyone proving integrality of winding, the fundamental-cycle normalization, or the split H₁(S¹;ℤ)≅ℤ cites this. The body is a one-line composition of the cycle inclusion with the winding chain map.
Claim. For a degree-$1$ cycle $z$ in the singular chain complex of $S^1$ with integer coefficients, define its winding number in $\mathbb{R}$ by including $z$ into $C_1(S^1;\mathbb{Z})$ and applying the winding chain map $W:C_1(S^1;\mathbb{Z})\to\mathbb{R}$ (the map that on each free generator sends the coefficient $n$ to $n$ times the winding of that singular $1$-simplex).
background
The module lifts the path-level winding/displacement of CircleWinding to singular simplices of $S^1$ and proves that winding kills boundaries, so it descends to homology. On a singular $1$-simplex one reparameterizes $\Delta^1$ to the unit interval and takes path displacement (equivalently $2\pi$ times winding). The key identity is that the alternating face sum of displacements on any singular $2$-simplex vanishes, by a telescoping homotopy inside the convex standard $2$-simplex.
The ambient complex is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with coefficients in $\mathbb{Z}$. The winding chain map $W:C_1(S^1;\mathbb{Z})\to\mathbb{R}$ is the coproduct descent that on the free generator indexed by a singular $1$-simplex $s$ acts by $n\mapsto n\cdot(\text{winding of }s)$. Cycles sit inside chains via the standard inclusion of the cycle submodule.
Together with the fact that the once-around generator has winding $1$, this setup supplies the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation (surjectivity) half needs a prism/subdivision operator not yet in Mathlib singular homology.
proof idea
Pure definition, not a proof. Form the composite morphism in $\mathrm{ModuleCat},\mathbb{Z}$ given by the degree-$1$ cycle inclusion into $C_1$ followed by the winding chain map $W$, then apply the underlying $\mathbb{Z}$-linear map of that composite to the cycle $z$. No lemmas are invoked beyond the already-constructed chain map and the cycle inclusion of the singular complex.
why it matters
This is the chain-level winding functional on cycles that every subsequent integrality and normalization statement in the module evaluates. Downstream it is used to show the fundamental cycle has winding equal to its integer coefficient; that a closed singular generator cycle has winding equal to coefficient times simplex winding; that finite closed-generator lists have integer winding; and that subtracting the matching multiple of the fundamental cycle leaves a zero-winding residual (the algebraic shell around the remaining geometric filling problem).
In the Recognition framework this is the concrete left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$, the split-injective half of the integer comparison map. The module doc ties that isomorphism to the strict T8 target (three spatial dimensions via the eight-tick octave). The open geometric half is generation: every $1$-cycle homologous to an integer multiple of the fundamental cycle, packaged as the still-open integrality proposition that every cycle has integer winding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.