cycleWinding_fundamentalCycle
plain-language theorem explainer
The winding of n times the fundamental singular 1-cycle on S¹ equals the integer n as a real. Anyone proving the split-injective half of H₁(S¹;ℤ) ≅ ℤ, or subtracting a matching multiple to get a zero-winding residual, cites this. The proof unfolds the cycle winding map and reduces to the known fact that the winding chain map sends the fundamental simplex to 1.
Claim. For every integer $n$, if $\gamma$ denotes the fundamental singular $1$-cycle on $S^1$ (the once-around generator lifted to a cycle), then the winding of the degree-$1$ cycle $n\cdot\gamma$ equals $n$ as a real number.
background
This module lifts path-level winding on the circle to singular $1$-simplices of $\mathrm{TopCat.sphere},1$ and proves that winding kills boundaries, so it descends to a homology invariant. The displacement of a singular $1$-simplex is $2\pi$ times its winding, obtained by reparameterizing $\Delta^1$ to the unit interval and taking path displacement. The chain-level identity is that the alternating face sum of displacements on any singular $2$-simplex vanishes (telescoping via a convex homotopy in $\Delta^2$).
The fundamental cycle is the once-around singular $1$-chain, lifted into the cycle object of the integer singular chain complex of $S^1$ using its zero-boundary proof. Cycle winding includes a degree-$1$ cycle into $C_1(S^1;\mathbb{Z})$ and applies the winding chain map $W$, which on a free generator indexed by a singular $1$-simplex $s$ is $n\mapsto n\cdot(\text{winding of }s)$. Upstream, $W$ sends the fundamental singular $1$-chain to $1$, so the integer comparison map $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ is split-injective.
proof idea
Term-mode reduction. Unfold cycle winding to the composite of the cycle inclusion with the winding chain map. Rewrite the fundamental cycle as a lift-cycles morphism and cancel the inclusion via liftCycles_i_assoc, leaving the winding chain map on the underlying fundamental singular $1$-chain applied to $n$. Apply windingChainMap_fundamental (that composite equals the span-singleton map at $1$), then simplify with LinearMap.toSpanSingleton_apply to obtain $(n:\mathbb{R})$.
why it matters
This is the cycle-level left-inverse statement: winding recovers the integer coefficient of the fundamental class. Module context frames it as the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, paired with path winding of the fundamental loop equaling $1$. Downstream, closedSingularOneCycleList_zeroWinding_residual uses it to subtract the matching multiple of the fundamental cycle and produce a zero-winding residual (the algebraic shell around the remaining geometric filling problem). zeroWindingCycles_bound_of_fundamentalCycle_boundary_generates invokes the same fact: write $z=\partial b+n\cdot\gamma$; winding kills $\partial b$ and sends $\gamma$ to $1$, so $W(z)=0$ forces $n=0$. The free-chain variant windingChainMap_fundamentalCycleFreeChain is the parallel statement off the cycle object. The singular chain complex of $S^1$ is flagged as the chain-level object whose degree-$1$ homology is the strict T8 target in this foundation stack; generation (every $1$-cycle homologous to an integer multiple of $\gamma$) remains the open geometric half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.