closedSingularOneCycle_bounds_of_raw_boundary
plain-language theorem explainer
If a raw singular 2-chain on S¹ has boundary equal to the free generator of a closed singular edge, that same chain witnesses that the corresponding closed 1-cycle is a boundary in singular homology. Anyone proving H₁(S¹;ℤ) ≅ ℤ from winding data cites this raw-to-cycle handoff. The proof is a short injectivity argument: iCycles is mono, so equality after inclusion into C₁ upgrades the raw boundary identity to a cycles identity.
Claim. Let $s$ be a singular $1$-simplex on $S^1$ whose two faces agree (a closed edge). Write $C_\bullet$ for the integer singular chain complex of $S^1$, and let $\zeta_s$ be the closed generator $1$-cycle associated to $s$. If $b\in C_2$ satisfies $\partial b = [s]$ (the free generator of $s$ in $C_1$), then there exists $c\in C_2$ with $\mathrm{toCycles}(c)=\zeta_s$ in the module of $1$-cycles; in fact $c=b$ works.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact needed for a winding homomorphism on $H_1(S^1;\mathbb{Z})$. A SingularOneSimplex is a map $\Delta^1\to S^1$ in the singular simplicial set of TopCat.sphere 1. When the two face maps agree, the edge is closed and defines a genuine $1$-cycle.
sphereOneSingularIntChainComplex is Mathlib's singular chain complex of $S^1$ with $\mathbb{Z}$ coefficients; its degree-$1$ homology is the strict T8 target in this foundation layer. closedSingularOneCycle s hfaces is the cycle-object element generated by such a closed edge (via liftCycles). The companion identity closedSingularOneCycle_iCycles says that including that cycle back into $C_1$ recovers the coproduct summand generator $\Sigma.\iota_s$.
This lemma is the raw-chain twin of the free-boundary version: it accepts a bare $2$-chain whose ordinary boundary is that generator, rather than a freer algebraic package, and concludes the closed cycle bounds.
proof idea
Term-mode proof that takes the witness to be the given raw chain $b$ itself. Mono of iCycles 1 (from the chain-complex structure) gives injectivity of the underlying map on cycles into $C_1$. It therefore suffices to check equality after composing with iCycles. Rewrite via HomologicalComplex.toCycles_i (so toCycles ≫ iCycles = d), apply the hypothesis $\partial b = [s]$, then closedSingularOneCycle_iCycles to replace the closed cycle's inclusion by the same generator, and finish by rfl.
why it matters
In the CircleWindingChain program, winding on singular edges must become a homology invariant and a left inverse to the fundamental class, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module doc states that this, with pathWinding_fundamentalLoop, is exactly that half; surjectivity still needs a prism/subdivision operator Mathlib does not yet supply.
The nearby cone comment records the geometric handoff after singularEdgePath_homotopicRel_const_of_loop_winding_zero: a rel-endpoint nullhomotopy of a zero-winding closed edge produces a cone $2$-simplex whose raw boundary is the edge generator. This theorem turns that raw boundary identity into the statement that the closed generator cycle bounds, without re-entering path homotopy. No downstream uses are recorded yet; it is infrastructure for the generation/bounding direction of the integer comparison map on $H_1(S^1)$. Framework-wise it sits under the T8 spatial-dimension forcing chain's topological prerequisites (circle homology as the model computation).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.