closedSingularOneCycleList_spans_of_chainList_spansCycles
plain-language theorem explainer
If every singular 1-cycle on S¹, after inclusion into C₁, equals a finite raw sum of closed singular generators, then every cycle object itself equals that finite closed-generator sum. Anyone proving integer winding on all 1-cycles cites this bridge. The proof is injectivity of the cycle inclusion monomorphism iCycles, plus the list-inclusion identity.
Claim. Assume every $1$-cycle $z$ in the singular chain complex of $S^1$ with $\mathbb{Z}$ coefficients satisfies: its image under the cycle inclusion $i_{\mathrm{cyc}}\colon Z_1\hookrightarrow C_1$ equals a finite integer linear combination of closed singular $1$-simplices. Then every such $z$ equals that same finite combination already as a cycle object (not merely after inclusion).
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 remaining generation half needs a finite combinatorial spanning statement: every $1$-cycle is a finite sum of closed singular generators.
Two Prop-level targets encode that spanning. Raw-chain spanning says: for every cycle $z$, the image $i_{\mathrm{cyc}}(z)\in C_1$ equals a finite list sum of closed generators. Cycle-object spanning says the stronger equality $z$ itself equals the corresponding cycle-list sum. The list-to-chain map and the list-to-cycle map are related by the identity that including a closed-generator cycle list recovers the raw chain list.
The ambient complex is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with integer coefficients; $i_{\mathrm{cyc}}$ is its degree-$1$ cycles inclusion, known to be a monomorphism in $\mathrm{ModuleCat},\mathbb{Z}$.
proof idea
Fix a cycle $z$. Raw-chain spanning supplies a finite list $ts$ of closed-generator terms with $i_{\mathrm{cyc}}(z)$ equal to the raw chain list of $ts$. The companion identity says $i_{\mathrm{cyc}}$ of the cycle-list of $ts$ equals that same raw chain list, so $i_{\mathrm{cyc}}(z)=i_{\mathrm{cyc}}(\mathrm{cycleList}(ts))$. Mono of $i_{\mathrm{cyc}}$ (via ModuleCat.mono_iff_injective) yields $z=\mathrm{cycleList}(ts)$, which is cycle-object spanning.
why it matters
Cycle-object spanning is the finite-chain combinatorial statement flagged as left for proving integral cycle winding: every singular $1$-cycle has an integer winding number via endpoint cancellation. This lemma closes the gap between the more accessible raw-chain formulation (closer to finite-support cancellation) and the cycle-object form needed downstream.
In the module narrative, winding kills boundaries plus the fundamental loop of winding $1$ already give a left inverse to the fundamental class. Surjectivity of the integer comparison map (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs generation; this implication is a pure mono bookkeeping step on that path. It sits in the Foundation circle-homology stack that feeds the strict $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ target tied to the T8 dimensional forcing chain. No downstream consumers are wired yet in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.