fundamentalHomologyClassIso_of_surjective
plain-language theorem explainer
Assuming the fundamental class generates first homology of the circle, the integer comparison map becomes an isomorphism ℤ ≅ H₁(S¹;ℤ) in ModuleCat. Anyone closing the Mathlib handoff H₁(S¹;ℤ) ≅ ℤ cites this. The argument is purely categorical: winding already gives mono, generation gives epi, and modules are balanced so mono+epi yields an iso.
Claim. If the comparison map $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ sending $n$ to $n$ times the fundamental class is surjective on underlying maps, then that comparison is an isomorphism $\mathbb{Z}\cong H_1(S^1;\mathbb{Z})$ in the category of $\mathbb{Z}$-modules.
background
This module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries, so winding descends to a homology invariant. Combined with the once-around loop having winding $1$, that gives a left inverse to the fundamental class and hence the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The integer comparison map is the morphism $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ sending $n$ to $n$ times the homology class of the fundamental singular $1$-cycle on TopCat.sphere 1. Its monomorphism property is already proved from the covering-space winding invariant: distinct integer multiples of the once-around loop are never homologous.
Surjectivity of that same map (every degree-$1$ class is an integer multiple of the fundamental class) is still open and is packaged as a named hypothesis. The chain complex in play is Mathlib's singular chain complex of the $1$-sphere with integer coefficients; its $H_1$ is the strict T8 target object.
proof idea
One short categorical construction. Install Mono on the comparison map via the already-proved monomorphism theorem. Turn the surjectivity hypothesis into Epi by the ModuleCat criterion that epi means surjective on underlying maps. Modules are balanced, so isIso_of_mono_of_epi upgrades mono+epi to IsIso. Finish with asIso to obtain the isomorphism in ModuleCat.
why it matters
This is the categorical glue between the open generation hypothesis and the exact Mathlib target $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Downstream, the handoff theorem builds the bridge isomorphism as the inverse of this iso under the same surjectivity assumption.
In the Recognition forcing chain, $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is the remaining Mathlib-facing element tied to the circle and the eight-tick/T8 spatial story. Nonvanishing of $H_1$ is already unconditional; only generation (surjectivity) is open, and this definition converts that single Prop into a full ModuleCat isomorphism once it is discharged.
No new geometric content is added here: the mono half is closed by winding, the epi half is the outstanding simplicial-prism/subdivision gap Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.