circleH1ZIsoInt_of_fundamentalCycle_boundary_generates
plain-language theorem explainer
If every singular 1-cycle on S¹ is homologous to an integer multiple of the fundamental cycle plus a 2-boundary, then H₁(S¹;ℤ) ≅ ℤ as ℤ-modules. Algebraic topologists closing the Mathlib singular-homology computation of the circle cite this. The proof is a two-step term composition: boundary generation implies cycle-class generation, which yields the isomorphism certificate.
Claim. Assume that for every degree-$1$ singular cycle $z$ on $S^1$ with integer coefficients there exist $n\in\mathbb{Z}$ and a $2$-chain $b$ such that $z = \partial b + n\,[\gamma]$, where $[\gamma]$ is the lifted fundamental cycle. Then the first singular homology of the circle is isomorphic to $\mathbb{Z}$ as a $\mathbb{Z}$-module: $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular 1-simplices on $S^1$. The key chain-level fact is that simplex displacement kills boundaries: for every singular 2-simplex the alternating face sum of displacements vanishes, by telescoping inside the convex standard 2-simplex and homotopy invariance of path displacement. Together with the fact that the once-around loop has winding 1, this supplies a left inverse to the fundamental class, i.e. the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The remaining half is generation: every 1-cycle must be homologous to an integer multiple of the fundamental cycle. The hypothesis fundamentalCycle_boundary_generates packages that statement at the concrete chain level: every cycle $z$ in degree 1 equals $\partial b + n\cdot\gamma$ for some 2-chain $b$ and integer $n$. The target certificate circleH1ZIsoInt is the Prop asserting a nonempty isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in Mathlib's singular homology, without project-local circle replacements.
Upstream, cycle-class generation is the homology-level shadow of the boundary decomposition: the $\partial b$ term dies under the homology projection, so $[z]=n[\gamma]$. That class-generation statement already closes the isomorphism via a further surjectivity reduction.
proof idea
One-line term wrapper. Apply fundamentalCycleClass_generates_of_boundary_generates to the hypothesis to obtain cycle-class generation (every homology class is an integer multiple of the fundamental class, since the boundary summand vanishes under homologyπ). Feed that into circleH1ZIsoInt_of_fundamentalCycleClass_generates, which itself reduces class generation to surjectivity of the fundamental homology class and thence to the Mathlib isomorphism certificate circleH1ZIsoInt.
why it matters
This is the final Mathlib $H_1$ closure gate from the concrete boundary-generation theorem. Three geometric attack routes discharge through it: directed-cycle term generation (circleH1ZIsoInt_of_directedCycleTerms), oriented cyclic-family filling (circleH1ZIsoInt_of_orientedCyclicFamilies), and the pair of integer-winding-plus-zero-winding-bounds (circleH1ZIsoInt_of_integral_winding_of_zeroWinding_bounds). Each reduces its geometric hypothesis to fundamentalCycle_boundary_generates and then cites this theorem.
In the Recognition foundation the winding homomorphism on 1-cycles is the left inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$; this declaration packages the converse generation half into the official Mathlib bridge certificate. The module doc notes that full geometric generation still needs simplicial prism/subdivision machinery Mathlib does not yet supply, so the open work sits in proving the hypothesis, not in this glue step. No direct T0–T8 forcing step is claimed 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.