singularOneChainFreeToChain_boundary_free
plain-language theorem explainer
Composing the free-to-Mathlib map on singular 1-chains of S¹ with Mathlib's singular boundary and the Mathlib-to-free map on 0-chains recovers the explicit free boundary (terminal face minus initial face). Anyone moving free-module cycle conditions into Mathlib's singular chain complex of the circle cites this. The proof extends by freeness and checks generators via the one-simplex free-boundary identity.
Claim. The composite of the free-to-raw map on singular $1$-chains of $S^1$, Mathlib's singular boundary $d_1:C_1(S^1;\mathbb{Z})\to C_0(S^1;\mathbb{Z})$, and the raw-to-free map on $0$-chains equals the explicit free boundary that sends each directed edge generator to its terminal $0$-face minus its initial $0$-face.
background
This 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})$. Mathlib supplies the singular chain complex of TopCat.sphere 1 with integer coefficients; its degree-$1$ homology is the strict T8 target.
To compute with generators, the development introduces free modules on singular $1$- and $0$-simplices together with comparison maps to Mathlib's raw chain groups. The free-to-raw map on $C_1$ sends each free generator to the matching coproduct summand. The explicit free boundary sends a directed edge to terminal $0$-face minus initial $0$-face.
The present identity says Mathlib's raw $d_1$, transported along those free comparisons, is exactly that free boundary. Upstream, the free boundary on a generator is already computed by the freeMk evaluation lemma, and the one-simplex case of the transported boundary is available separately.
proof idea
Extend by freeness of the domain: ModuleCat.free_hom_ext reduces equality of morphisms out of the free $C_1$ to agreement on free generators freeMk s.
On a generator, unfold the composite via hom_comp and rewrite the free-to-raw map by its freeMk lemma, so the left side becomes the Mathlib boundary of the corresponding summand inclusion, then mapped to free $C_0$. That one-simplex identity is singularOneSimplexChain_boundary_free. The right side is the free boundary on freeMk s, rewritten by singularOneBoundaryFree_freeMk to terminal minus initial. A short simp on toSpanSingleton finishes the match.
why it matters
This is the naturality square that lets free-module boundary calculations control Mathlib cycles. Downstream, d_singularOneChainFreeToChain_eq_zero_of_freeBoundary_zero uses it (with injectivity of the free $C_0$ comparison) to conclude that a free edge-chain with vanishing free boundary lifts to a genuine degree-$1$ cycle. The converse transport singularOneChainToFree_boundary_free is the inverse square.
Those vanishing lemmas feed directedCycleFreeTerm_of_cyclicFamily and the oriented variant: a cyclically connected family of edges assembles into a free cycle with integer winding, discharging the homological half of cyclic extraction in balanced-flow decompositions.
In the larger program this supports the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via winding (module doc), which is the chain-level input to the strict T8 dimensional target. Generation (surjectivity) still needs prism/subdivision operators Mathlib does not yet provide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.