fundamentalCycleFreeChain_eq_zsmul
plain-language theorem explainer
The free-chain image of an integer coefficient n on the fundamental 1-cycle of S¹ equals n times the geodesic free chain from 0 to 2π. Anyone identifying the generator of H₁(S¹;ℤ) with the once-around geodesic cites this. The proof rewrites the geodesic as the fundamental free chain, then chases the cycle inclusion and the free-span map through the singular chain complex.
Claim. For every integer coefficient $n\in\mathbb{Z}$, the free-coordinate image of $n$ times the fundamental singular $1$-cycle on $S^1$ equals the scalar multiple $n\cdot\gamma$, where $\gamma$ is the free $1$-chain of the geodesic path from $0$ to $2\pi$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The once-around singular $1$-simplex is the geometric generator candidate; its coproduct summand inclusion is the fundamental singular $1$-chain in the integer singular chain complex of $\mathrm{TopCat.sphere},1$.
The fundamental cycle is that chain lifted into the cycles object via the zero-boundary proof. Free chains are the free $\mathbb{Z}$-module on singular $1$-simplices; the free-coordinate image of a cycle is its image under the inclusion of cycles followed by the map that sends a simplex to the corresponding free generator. The geodesic free chain from $0$ to $2\pi$ is the free generator of the linear once-around path on the circle cover.
Upstream, the fundamental singular $1$-chain is the $\Sigma$-inclusion at the once-around simplex, and the cycle lift uses the already-proved vanishing of its boundary.
proof idea
Rewrite the right-hand side via the identification that the geodesic free chain $0\to 2\pi$ equals the free image of the fundamental cycle. Unfold the free-chain map on the left. First, the composition of the fundamental cycle with the cycles inclusion recovers the fundamental singular $1$-chain; apply both sides to the coefficient $n$. Second, the free-span map on that singular chain is the span-singleton of the once-around simplex (by the free-map identity on generators). Congruence on $n$, then transport through the cycles-inclusion identity, yields the scalar multiple equality.
why it matters
This pins the free-coordinate normal form of integer multiples of the fundamental class: they are exactly integer multiples of the geodesic $0\to 2\pi$. Downstream, orientedCyclicFamilies_terminalSideCorrection_generate_holds uses it when assembling the bounding $2$-chain for terminal-side corrections on oriented cyclic families, where total winding $n=\sum m_i$ must match $n$ copies of the once-around geodesic.
In the module's program this is bookkeeping for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: every $1$-cycle should be homologous to an integer multiple of the fundamental cycle. The free-chain identification makes that multiple concrete as a geodesic multiple, which is the chain-level input to winding as a left inverse of the fundamental class. Framework-wise it supports the circle homology computation that feeds the strict T8 target (three spatial dimensions via the eight-tick / sphere package), without claiming the full surjectivity half yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.