fundamentalHomologyClass_bijective_of_surjective
plain-language theorem explainer
Assuming the fundamental class generates first homology of the circle, the integer comparison map from Z to H1(S1;Z) is bijective on underlying modules. Anyone assembling the classical isomorphism H1(S1;Z) ≅ Z from the winding half would cite this upgrade. The argument is a short split: injectivity from the already-proved monomorphism (via winding), surjectivity by the generation hypothesis.
Claim. If the comparison morphism $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$, $n\mapsto n\cdot[\mathrm{fundamental}]$, is surjective on underlying modules, then it is bijective as a map of $\mathbb{Z}$-modules.
background
This module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries of $2$-simplices. Combined with the fact that the once-around loop has winding $1$, that yields a winding homomorphism on $H_1(S^1;\mathbb{Z})$ that is a left inverse to the integer comparison map, giving the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The comparison map itself is the morphism in ModuleCat sending $n\in\mathbb{Z}$ to $n$ times the homology class of the fundamental singular $1$-cycle. Upstream, that map is already a monomorphism: distinct integer multiples of the once-around loop are never homologous, proved from the covering-space winding invariant with no axioms.
What remains open is generation: every degree-$1$ class is an integer multiple of the fundamental class. That statement is packaged as a named proposition (surjectivity of the comparison map). The present theorem is the purely formal upgrade from that generation hypothesis to bijectivity of the underlying module map.
proof idea
Bijectivity is split into injectivity and surjectivity. For injectivity, instantiate the monomorphism instance from the winding theorem, then apply the dictionary that monomorphisms in ModuleCat are exactly the injective underlying maps. Surjectivity is exactly the generation hypothesis, passed through unchanged. No new geometric content is introduced.
why it matters
This is the bookkeeping step that turns the open generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ into a full bijection of underlying modules, once generation is supplied. The module already records that winding gives a retraction and a monomorphism; generation is deliberately left as a named proposition because Mathlib's singular homology still lacks the simplicial prism or subdivision operator needed for a hands-on proof.
Per the upstream generation interface, this surjectivity is not required for the strict T0-T8 frontier closure, which only needs nonvanishing of $H_1(S^1;\mathbb{Z})$. The classical isomorphism is the natural completion of the circle-winding chain, and this lemma is the conditional bridge from generation to bijectivity. No downstream consumers are wired yet; the next natural step is the categorical isomorphism (mono+epi in a balanced category), which the neighboring comment sketches.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.