fundamentalCycle_boundary_generates_of_directedCycleTerms
plain-language theorem explainer
If every directed closed walk on S¹ is homologous to an integer multiple of the once-around fundamental cycle, then every singular 1-cycle is. Anyone proving H₁(S¹;ℤ) ≅ ℤ via the winding invariant cites this reduction. The proof pushes a cycle into free chains, decomposes the boundary kernel into directed-cycle terms, and lifts termwise generation back through the cycle inclusion.
Claim. Assume decidable equality on singular $0$- and $1$-simplices of $S^1$. If every directed-cycle free term $t$ admits $n\in\mathbb{Z}$ and a $2$-chain $b$ with $t.\mathrm{cycle}=\partial b+n\cdot[\gamma]$ (where $[\gamma]$ is the fundamental cycle), then every singular $1$-cycle $z$ likewise admits $n$ and $b$ with $z=\partial b+n\cdot[\gamma]$.
background
The module lifts path-level winding on $S^1$ to singular simplices of TopCat.sphere 1. Displacement of a singular $1$-simplex is path displacement after reparameterizing $\Delta^1$ to $[0,1]$; the key identity is that alternating face displacements of any $2$-simplex vanish, so winding kills boundaries and induces a homology invariant.
The integer singular chain complex of $S^1$ is Mathlib's singularChainComplexFunctor evaluated at the sphere. Its degree-$1$ cycles carry the fundamental once-around class. The remaining generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ asks that every $1$-cycle be homologous to an integer multiple of that class.
A local geometric target packages generation for single directed-cycle free terms: each such term's cycle equals a boundary plus an integer multiple of the fundamental cycle. Finite lists of those terms assemble into cycle objects whose free-chain images match the explicit free-chain sums.
proof idea
Fix a $1$-cycle $z$. Map it through the cycle inclusion and the free-chain isomorphism to a free $1$-chain $c$ with vanishing free boundary. Invoke the free-boundary-kernel decomposition into a finite list of directed-cycle free terms. Injectivity of the free-chain map and of the cycle inclusion identifies $z$ with the cycle-object sum of that list. Apply listwise generation (which follows from the termwise hypothesis) to obtain $n$ and a $2$-chain $b$, then transport the equality back along the identification of $z$ with the list cycle.
why it matters
This is the bridge from the minimal geometric target (fill one directed closed walk) to the global chain-level generation theorem. Downstream, circleH1ZIsoInt_of_directedCycleTerms feeds the result straight into the final Mathlib circle $H_1$ isomorphism, and zeroWindingCycles_bound_of_directedCycleTerms closes the zero-winding filling target. Together with the already-proved winding left-inverse (from pathWinding_fundamentalLoop and kills-boundaries), generation supplies the missing surjectivity half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. In the Recognition forcing chain this is the strict topological input behind T8 ($D=3$) via the circle's first homology; the remaining open piece is the geometric hypothesis that each directed-cycle term is itself generated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.