zeroWindingCycles_homologyClass_zero_of_windingHomologyMap_mono
plain-language theorem explainer
If the winding map on first homology of the circle is monic, every singular 1-cycle of winding zero is homologous to zero. Algebraic topologists working the split-injective half of H₁(S¹;ℤ) ≅ ℤ cite this bridge from monicity to the homology-class form of the zero-winding target. The proof is a short injectivity chase: monicity gives injectivity of the underlying module map, and the winding of the homology class vanishes when the cycle winding does.
Claim. Assume the winding homomorphism $H_1(S^1;\mathbb{Z})\to\mathbb{R}$ is monic as a morphism of $\mathbb{Z}$-modules. Then for every singular $1$-cycle $z$ on $S^1$, if the winding of $z$ is zero then the image of $z$ under the homology projection is the zero class in $H_1(S^1;\mathbb{Z})$.
background
The module develops the winding invariant on singular 1-simplices of $S^1$ and the chain-level identity that winding kills boundaries. Displacement of a singular 1-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval; the alternating face sum of displacements on any singular 2-simplex vanishes by a convex-simplex homotopy and path-displacement additivity and homotopy invariance.
That kills-boundaries fact lets the winding chain map factor through opcycles and hence through $H_1$, yielding the winding homology map $H_1(S^1;\mathbb{Z})\to\mathbb{R}$. The zero-winding homology-class target is the proposition that every 1-cycle of winding zero has vanishing homology class under the degree-1 homology projection. Combined with the fact that winding sends the once-around generator to 1, this is the split-injective half of the classical isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
Term-mode argument after introducing a zero-winding cycle $z$. Convert monicity of the winding homology map into injectivity of its underlying $\mathbb{Z}$-linear map via ModuleCat.mono_iff_injective. Apply that injectivity to the homology class of $z$. Rewrite the image under the winding homology map using homologyπ_windingHomologyMap_apply and the hypothesis that cycle winding of $z$ is zero; a final simp shows the image is zero, so injectivity forces the homology class itself to vanish.
why it matters
This is the monicity-to-homology-class leg of the zero-winding filling package. Downstream, zeroWindingCycles_bound_of_windingHomologyMap_mono feeds it into the explicit singular 2-boundary target, and zeroWindingCycles_bound_iff_windingHomologyMap_mono packages the equivalence: chain-level zero-winding filling holds if and only if the winding homology map is monic.
In the module's program this closes the "every zero-winding cycle is a boundary" direction once monicity is known, completing the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ relative to the fundamental class. The converse generation half (every 1-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. 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.