closedSingularOneCycle_iCycles
plain-language theorem explainer
Including a closed singular 1-simplex as a cycle into degree-1 chains recovers the free generator of that simplex in C₁(S¹;ℤ). Cited by anyone assembling cycle-object generators or proving that closed edges bound or generate the fundamental class. Proof is a one-line rewrite through the closed-cycle definition and the universal property of liftCycles.
Claim. Let $s$ be a singular $1$-simplex on $S^1$ whose two face maps agree ($\delta_0 s = \delta_1 s$). Then the inclusion of $1$-cycles into $C_1(S^1;\mathbb{Z})$ applied to the cycle generated by $s$ equals the coproduct summand inclusion of $s$ into $C_1$.
background
The module lifts path-level winding on $S^1$ to singular simplices of TopCat.sphere 1 and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is an element of the singular simplicial set of $S^1$ in degree $1$. It is closed when its two face maps agree, so the alternating boundary vanishes. The integer singular chain complex of $S^1$ is the Mathlib object whose degree-$1$ homology is the strict T8 target.
The closed-cycle constructor builds a morphism from $\mathbb{Z}$ into the cycles object in degree $1$ by lifting the free generator of a closed simplex. The cycles inclusion $i$ is the canonical map $Z_1\hookrightarrow C_1$ of that chain complex.
proof idea
One-line wrapper. Unfold the closed-cycle constructor (it is exactly liftCycles of the free generator of $s$), then apply HomologicalComplex.liftCycles_i, which states that including a lifted cycle back into the chain group recovers the original chain. No geometric content is used.
why it matters
Bookkeeping identity that lets every downstream consumer treat a closed singular edge as an honest cycle-object generator whose image in $C_1$ is the free summand. It is used by the free- and raw-prism generation theorems (closed edge homologous to an integer multiple of the fundamental cycle), by the free/raw boundary consumers, by the zero-winding cone theorem (any closed singular edge of winding $0$ bounds), by the finite-sum term structure for closed-generator decompositions, and by constant-cycle and cyclic-edge-list constructions.
In the module narrative this is infrastructure for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding already gives the left inverse to the fundamental class; prism/subdivision arguments need to move freely between cycle objects and raw chains. The identity is the bridge. Framework landmark: supports the strict T8 homology computation on $S^1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.