fundamentalHomologyClass_comp_windingHomologyMap
plain-language theorem explainer
The composite of the integer comparison map ℤ → H₁(S¹;ℤ) with the winding map H₁(S¹;ℤ) → ℝ equals the standard inclusion n ↦ n·1. Anyone proving that the fundamental class has infinite order, or that H₁(S¹) is nonzero, cites this identity. The proof unfolds the cycle and homology factorizations and reduces to the chain-level fact that winding sends the fundamental 1-chain to 1.
Claim. The composite $\mathbb{Z} \xrightarrow{[\mathrm{fund}]} H_1(S^1;\mathbb{Z}) \xrightarrow{w} \mathbb{R}$ equals the standard inclusion $n \mapsto n\cdot 1$. Equivalently, the winding homomorphism is a retraction of the comparison map that sends $1$ to the fundamental homology class, so $w([\mathrm{fundamental}]) = 1$.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular 1-simplices and proves that displacement kills boundaries of 2-simplices. That chain-level vanishing lets winding descend to a homology map $H_1(S^1;\mathbb{Z})\to\mathbb{R}$.
The integer comparison map $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ is built by lifting the fundamental singular 1-chain (the once-around generator) to a cycle and projecting to homology. The winding homology map is the factorization of the winding chain map through opcycles, using that winding annihilates $\partial_2$.
Upstream, windingChainMap_fundamental already records that the winding chain map sends the fundamental 1-chain to $1$ in $\mathbb{R}$. The present statement is the same identity after passage to homology.
proof idea
Unfold the definitions of the comparison map (fundamental cycle composed with homology projection) and of the winding homology map (homology inclusion into opcycles, then the opcycle descent of the winding chain map). After the standard homology $\pi$/$\iota$ and lift/desc rewrites and a category association, the composite collapses exactly to the chain-level identity that winding sends the fundamental singular 1-chain to $1$, which is applied by exact.
why it matters
This is the homology-level form of "winding is inverse to the fundamental loop class": it pins $[\mathrm{fundamental}]$ to the real number $1$ and exhibits the comparison map as split-injective on the nose after composing with winding.
It is the key algebraic input to three parents: monomorphicity of $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ (infinite order of the fundamental class), unconditional nonvanishing of $H_1(S^1;\mathbb{Z})$, and the conditional statement that winding itself is mono once the fundamental class generates. Together these give the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ without axioms or sorry; surjectivity/generation remains open pending a simplicial prism or subdivision operator Mathlib does not yet supply.
In the broader Recognition foundation stack this anchors the circle's first homology as a free rank-one $\mathbb{Z}$-module on the once-around generator, the topological substrate for eight-tick and winding arguments later in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.