fundamentalCycle
plain-language theorem explainer
The once-around singular 1-chain on S¹ is promoted to a genuine 1-cycle in the integer singular chain complex, via its vanishing boundary. Anyone citing the generator of H₁(S¹;ℤ) or the split-injective half of the integer comparison map needs this object. Construction is a one-line liftCycles application of the fundamental chain plus its boundary-zero lemma.
Claim. There is a morphism $\mathbb{Z}\to Z_1(S^1;\mathbb{Z})$ in $\mathbf{Mod}_{\mathbb{Z}}$ sending $1$ to the fundamental singular $1$-cycle on $S^1$: the once-around singular $1$-simplex, viewed as a cycle because its boundary vanishes.
background
The module develops the winding invariant on singular $1$-simplices of $\mathrm{TopCat.sphere},1$ and proves that winding kills boundaries. Displacement of a singular $1$-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval; the key identity is that the alternating face sum of displacements on any singular $2$-simplex vanishes (convex telescoping inside $\Delta^2$).
Upstream, the singular chain complex of $S^1$ with integer coefficients is the Mathlib singular chain complex functor applied to $\mathrm{TopCat.sphere},1$. The fundamental singular $1$-chain is the coproduct-summand inclusion selecting the once-around singular $1$-simplex. Its boundary is zero by the equal-faces theorem for that simplex: "the chain-level form of the equal-faces theorem for the once-around singular $1$-simplex."
Together with path winding of the fundamental loop equaling $1$, this cycle is the generator used for the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
One-line wrapper. Apply the chain-complex liftCycles constructor to three ingredients: the fundamental singular $1$-chain (degree-$1$ morphism $\mathbb{Z}\to C_1(S^1;\mathbb{Z})$), the zero morphism as the would-be boundary target (discharged by simp), and the theorem that the fundamental chain has vanishing boundary. The result is a morphism into the cycles object in degree $1$.
why it matters
This is the canonical generator object for all generation and residual arguments in the circle-winding chain module. Downstream consumers include: closed-edge prism generation (free and raw forms), the zero-winding cone theorem (integer coefficient $0$, edge filled by an explicit cone boundary), residual-bound generation for closed-generator lists, and the residual construction that subtracts an integer multiple of this cycle to obtain a zero-winding remainder.
Module doc places it in the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is a left inverse to the fundamental class. The converse (every $1$-cycle homologous to an integer multiple of this cycle) is the generation half and still needs simplicial prism/subdivision operators Mathlib singular homology does not yet supply. In the Recognition forcing chain this feeds the strict T8 target: degree-$1$ homology of the sphere as the dimensional witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.