cycleWinding_integral_of_freeBoundaryKernel_decomposesIntoDirectedCycles
plain-language theorem explainer
If every free singular 1-chain with vanishing boundary decomposes as a finite sum of directed cycle pieces, then every singular 1-cycle on S¹ has integer winding. Anyone closing the split-injective half of H₁(S¹;ℤ) ≅ ℤ cites this bridge. The proof pushes a cycle into free coordinates, applies the kernel decomposition, and transports integrality from the directed-cycle list via injectivity of the cycle and free-chain maps.
Claim. Assume every free singular $1$-chain $c$ with $\partial c = 0$ equals a finite sum of directed cycle pieces. Then for every singular $1$-cycle $z$ on $S^1$ with integer coefficients there exists $n \in \mathbb{Z}$ such that the winding of $z$ equals $n$ as a real number.
background
This module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries of $2$-simplices, so winding descends to a homology invariant. Together with the fact that the once-around generator has winding $1$, that gives the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The target property cycleWinding_integral asserts: every degree-$1$ cycle $z$ in the Mathlib singular chain complex of TopCat.sphere 1 has cycleWinding z equal to some integer viewed in $\mathbb{R}$. The hypothesis is the abstract kernel statement that every free edge-chain with vanishing free boundary is a finite list of directed cycle terms.
Upstream, lists of directed cycle pieces already have integer winding (directedCycleFreeTermList_winding_integral), and their free-chain image matches the explicit free sum (directedCycleFreeTermList_chain_eq). The singular complex is sphereOneSingularIntChainComplex.
proof idea
Fix a cycle $z$. Map it through the cycles inclusion and the free-chain isomorphism to a free $1$-chain $c$. Commutation of free boundary with the complex differential, plus iCycles_d, shows $\partial_{\mathrm{free}} c = 0$.
Apply the hypothesis to obtain a list ts of directed cycle pieces with free-chain equal to $c$. Injectivity of the free-chain map (it is an iso, hence mono) and of iCycles 1 upgrades that equality to $z =$ the cycle-object sum of ts.
Invoke directedCycleFreeTermList_winding_integral on ts to get an integer $n$ with matching winding, then rewrite along the identification of $z$.
why it matters
Integer-valued winding is the first concrete geometric subtarget toward identifying singular $H_1(S^1;\mathbb{Z})$ with $\mathbb{Z}$. The module frames that isomorphism as the chain-level content needed for the strict T8-side homology computation on the circle.
Downstream, the unconditional theorem discharges the hypothesis classically and obtains integer winding with no residual finite-flow assumption. A parallel corollary routes the same conclusion through cyclic edge-list decompositions. The final Mathlib $H_1$ closure circleH1ZIsoInt_of_directedCycles_of_zeroWinding_bounds feeds this result plus zero-winding filling into the comparison iso. With integrality in hand, zero-winding cycles bound if and only if every cycle is a boundary plus an integer multiple of the fundamental cycle.
This is the conditional bridge: decomposition of balanced free edge-flows implies the winding homomorphism lands in $\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.