circleH1ZIsoInt_of_windingHomologyMap_mono
plain-language theorem explainer
Injectivity of the winding map on H₁(S¹;ℤ) is enough to conclude that the circle's first singular homology is isomorphic to ℤ as a ℤ-module. Anyone closing the Mathlib circle-linking backend for the strict T8 replacement cites this. The proof is a one-line wrapper: mono implies the zero-winding filling bound, which already yields the isomorphism certificate.
Claim. If the homology-level winding homomorphism $H_1(S^1;\mathbb{Z})\to\mathbb{R}$ is monic (injective), then there exists an isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in the category of $\mathbb{Z}$-modules.
background
The module lifts path winding on $S^1$ to singular $1$-simplices. Displacement of a singular $1$-simplex is $2\pi$ times winding after reparameterizing $\Delta^1$ to the unit interval. The key chain-level fact is that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes, by telescoping inside the convex (hence simply connected) standard $2$-simplex.
Because the winding chain map annihilates $\partial_2$, it descends to a homology map $H_1(S^1;\mathbb{Z})\to\mathbb{R}$. Together with the fact that winding sends the once-around generator to $1$, this gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The remaining geometric input is a zero-winding filling theorem: every $1$-cycle of winding zero bounds.
Upstream, circleH1ZIsoInt is the strong Mathlib closure certificate: nonempty isomorphism of the circle's first singular homology with $\mathbb{Z}$. The finite-flow half is already unconditional; the only remaining geometric input named by the parent lemma is the zero-winding filling bound.
proof idea
One-line term wrapper. From monicity of the winding homology map, apply zeroWindingCycles_bound_of_windingHomologyMap_mono to obtain the zero-winding filling bound (every integer $1$-cycle of winding zero is a boundary). Feed that bound into circleH1ZIsoInt_of_zeroWinding_bounds, which already packages the unconditional integral-winding theorem with the filling hypothesis into the Mathlib isomorphism certificate $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
why it matters
This is the mono-to-isomorphism bridge on the circle homology chain. Downstream, mathlibCircleLinkingBackend_of_windingHomologyMap_mono quotes it directly: "Injectivity of the homology-level winding map is enough to build the Mathlib circle-linking backend required by the strict T8 replacement." T8 in the forcing chain forces $D=3$ spatial dimensions; the circle-linking backend is the singular-homology substrate that replacement needs from Mathlib rather than a project-local $S^1$.
The doc-comment records the architectural win: finite-flow is already closed by directed-cycle decomposition, so only mono of the winding map remains. That bypasses the old one-scalar cyclic-edge-list interface. The generation/surjectivity half of the classical computation still sits behind simplicial prism and subdivision operators Mathlib does not yet expose; monicity is the single remaining geometric hypothesis this lemma packages.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.