circleH1ZIsoInt_of_fundamentalCycleClass_generates
plain-language theorem explainer
Assuming every singular 1-cycle on the circle is homologous to an integer multiple of the fundamental cycle, first singular homology of S¹ with integer coefficients is isomorphic to ℤ. Cited by anyone discharging the Mathlib H₁(S¹;ℤ)≅ℤ certificate from the concrete cycle-generation hypothesis. Proof is a two-step term composition: generation implies surjectivity of the fundamental class, which yields the isomorphism.
Claim. If every degree-$1$ singular cycle on $S^1$ is homologous to an integer multiple of the fundamental cycle, then there is an isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as $\mathbb{Z}$-modules.
background
This module lifts path-level winding on the circle to singular 1-simplices and proves the kills-boundaries identity: alternating face displacements of any singular 2-simplex sum to zero. With the fundamental loop having winding one, that gives a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Surjectivity, the generation half, is the remaining geometric work.
The hypothesis here is the concrete cycle-representative form of generation: every degree-1 cycle has the same homology class as some integer multiple of the fundamental cycle. The target is the Mathlib bridge certificate that first singular homology of the circle is nonempty-isomorphic to $\mathbb{Z}$ as a $\mathbb{Z}$-module.
Upstream, that certificate already follows from bare surjectivity of the fundamental homology class map. Cycle-class generation implies that surjectivity because Mathlib's homology projection is an epimorphism, so every class has a cycle representative which generation then matches to an integer multiple.
proof idea
One-line term wrapper. First apply the lemma that cycle-class generation implies surjectivity of the fundamental homology class map. Feed the resulting surjectivity witness into the handoff theorem that turns that surjectivity into the Mathlib isomorphism certificate $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. No new geometric content.
why it matters
Closes the Mathlib-facing $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ certificate once the concrete cycle-generation hypothesis is available. Downstream, the boundary-generation form of the same certificate reduces through this theorem after converting boundary generation into cycle-class generation.
In the module's program, winding-kills-boundaries and fundamental-loop winding one already give the injective half; this declaration packages the surjective half into the final bridge Prop. That circle homology fact anchors the winding invariant used in the Recognition foundation's topological bookkeeping (including the eight-tick octave chain). The open geometric obligation remains: construct the singular 2-chain filling the zero-winding remainder, typically via subdivision or prism operators Mathlib singular homology does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.