zeroWindingCycles_homologyClass_zero_of_zeroWindingCycles_bound
plain-language theorem explainer
If every singular 1-cycle on S¹ with vanishing winding is a 2-boundary, then every such cycle is the zero class in H₁(S¹;ℤ). Cited by anyone equating the geometric filling theorem with injectivity of the homology-level winding map. The proof substitutes the filling 2-chain and applies the standard identity that homology projection kills boundaries.
Claim. Assume every singular $1$-cycle $z$ on $S^1$ with winding number zero equals the image of some singular $2$-chain under the boundary-into-cycles map. Then for every such $z$, the homology projection $\pi_1(z)$ is the zero class in $H_1(S^1;\mathbb{Z})$.
background
The module lifts path-level winding on the circle to singular simplices of TopCat.sphere 1. The displacement of a singular 1-simplex is the path displacement of its reparameterization to the unit interval; the key chain-level identity is that the alternating face sum of displacements on any singular 2-simplex vanishes (winding kills boundaries).
Two Prop-targets package the remaining generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The filling target asserts: every 1-cycle of winding zero is literally a 2-boundary. The homology-class target asserts the weaker statement that every such cycle maps to zero under the degree-1 homology projection of the integer singular chain complex of $S^1$.
The singular chain complex in play is Mathlib's singularChainComplexFunctor evaluated at the topological 1-sphere with coefficients in $\mathbb{Z}$. No project-local $S^1$ model is used.
proof idea
Term-mode implication. Fix a 1-cycle $z$ with winding zero. Apply the filling hypothesis to obtain a 2-chain $b$ with $z$ equal to the image of $b$ under the boundary-into-cycles map. Rewrite the goal as the composite (toCycles then homologyπ) applied to $b$ equaling zero. The Mathlib identity toCycles_comp_homologyπ collapses that composite to the zero morphism, and simp finishes.
why it matters
This is the easy direction from geometric filling to the homology-class formulation of zero winding. Downstream, zeroWindingCycles_bound_iff_windingHomologyMap_mono uses it as the first arm of the equivalence between the filling theorem and injectivity (Mono) of the homology-level winding map: filling implies homology-class zero (this lemma), which implies Mono of winding on $H_1$.
In the module's larger program, winding is already a left inverse to the fundamental class (split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). The missing half is generation: every 1-cycle homologous to an integer multiple of the once-around cycle. That is exactly what zero-winding cycles being boundaries (or, equivalently, Mono of winding on homology) supplies. The chain complex here is flagged as the strict T8-adjacent singular object whose degree-1 homology is the target of the comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.