fundamentalHomologyClass
plain-language theorem explainer
The integer comparison map ℤ → H₁(S¹;ℤ) sending n to n times the once-around fundamental class. Anyone assembling H₁(S¹;ℤ) ≅ ℤ, or the winding retraction, cites this arrow. It is the composite of the fundamental cycle inclusion with the degree-1 homology projection; no extra argument beyond the zero-boundary fact for that cycle.
Claim. The comparison morphism $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ defined by $n\mapsto n\cdot[\gamma]$, where $\gamma$ is the once-around fundamental singular $1$-cycle on $S^1$ (the image of the fundamental cycle under the homology projection $\pi_1$).
background
The module works at the singular-chain level on TopCat.sphere 1. The Mathlib singular chain complex with integer coefficients is the ambient object; its degree-1 homology is the strict target for the circle computation in the foundation chain.
A distinguished singular 1-chain (the once-around simplex) has vanishing boundary, so it lifts to a cycle. That lift is the fundamental cycle: a morphism $\mathbb{Z}\to Z_1(S^1;\mathbb{Z})$. Homology is cycles modulo boundaries, so composing with the canonical projection $\pi_1:Z_1\to H_1$ produces a class in $H_1(S^1;\mathbb{Z})$.
Separately, the module builds a winding (displacement) invariant on singular 1-simplices that kills boundaries, hence descends to homology. Together with the fact that winding of the fundamental loop is 1, this comparison map is the algebraic carrier of "$[\mathrm{fundamental}]$ generates a $\mathbb{Z}$ summand."
proof idea
Pure definition by composition: take the fundamental cycle (the lift of the once-around singular 1-chain into the cycle object, using the zero-boundary lemma) and postcompose with the degree-1 homology projection of the singular integer chain complex of $S^1$. No tactics; the noncomputable marker is inherited from the singular-complex and lift constructions.
why it matters
This is the comparison arrow whose mono/epi status decides $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Downstream, the winding map is shown to be a retraction of it (composite $\mathbb{Z}\to H_1\to\mathbb{R}$ is $n\mapsto n\cdot 1$), which pins the fundamental class to real winding 1 and yields injectivity. Surjectivity remains the open generation half; if granted, one obtains a ModuleCat isomorphism and the final handoff circleH1ZIsoInt.
In the Recognition forcing chain this homology computation is the strict algebraic target tied to the circle/octave geometry behind T7–T8 (eight-tick period and $D=3$). The definition itself closes no open goal; it is the named map every generation and iso lemma is stated about.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.