d_singularOneChainFreeToChain_eq_zero_of_freeBoundary_zero
plain-language theorem explainer
A free singular 1-chain on S¹ with vanishing free boundary maps to a genuine cycle in the raw integer singular chain complex. Anyone packaging cyclic edge families into homology classes cites this transport lemma. The proof is a short injectivity argument: free-to-raw boundary commutation plus injectivity of the C₀ free-forgetful map.
Claim. Let $c$ be a free singular $1$-chain on $S^1$. If the free boundary of $c$ vanishes, then the image of $c$ under the free-to-raw chain map is a cycle: $d_1(\iota(c))=0$ in the integer singular chain complex of $S^1$.
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 $1$-cycles. The target complex is Mathlib's singular chain complex of TopCat.sphere 1 with integer coefficients; its degree-$1$ homology is the comparison object for $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Free edge-chains are finitely supported $\mathbb{Z}$-linear combinations of singular $1$-simplices, with an explicit free boundary operator landing in free $0$-chains. The map $\iota$ sends a free $1$-chain into the raw $C_1$ of the singular complex. A companion map on degree $0$ forgets freeness; the proof uses that this $C_0$ map is injective, so vanishing after forgetfulness implies vanishing in the raw group.
The local goal is to move free-boundary computations (easy on generators and cyclic families) back to genuine cycles in the raw complex, without recomputing $d_1$ by hand.
proof idea
Term-mode argument via injectivity. Apply injectivity of the free-forgetful map on singular $0$-chains: it suffices to show the free image of the raw boundary is zero. The key identity is the boundary-commutation square relating free boundary, free-to-raw on $C_1$, and raw $d_1$. Congruence of that square on $c$, simplification of the composite, and substitution of the hypothesis that the free boundary is zero yield the claim. No case split on supports; pure diagram chase.
why it matters
This is the bridge from combinatorial free-boundary vanishing to genuine cycles. Downstream, directedCycleFreeTerm_of_cyclicFamily and directedCycleFreeTerm_of_orientedCyclicFamily use it: a cyclically connected family of edges (or oriented edges) has free boundary zero by telescoping endpoints, and this lemma promotes the free sum to a raw $1$-cycle with integer winding. Those packages discharge the homological half of cyclic extraction in balanced-flow decompositions.
In the module program, winding on cycles plus the once-around generator gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity still needs prism/subdivision operators Mathlib does not yet supply. The lemma itself is fully proved and closes no scaffold; it is infrastructure for the cycle side of that comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.