singularOneChainToFree_boundary_free
plain-language theorem explainer
The free-module isomorphism on singular 1-chains intertwines Mathlib's singular boundary with the explicit free boundary (terminal face minus initial face). Anyone transporting cycle or kernel statements between raw C₁(S¹;ℤ) and the free normal form cites this square. The proof cancels the free-to-raw epi and invokes the already-proved free-to-raw boundary identity.
Claim. Under the identification of Mathlib's singular chain group $C_1(S^1;\mathbb{Z})$ with the free $\mathbb{Z}$-module on singular $1$-simplices, Mathlib's degree-$(1\to 0)$ boundary equals the explicit free boundary that sends each directed edge to $(\text{terminal }0\text{-face})-(\text{initial }0\text{-face})$. Equivalently, the square relating raw and free $C_1$ and $C_0$ via the free isomorphisms and the two boundary maps commutes.
background
The module builds the winding invariant on singular $1$-simplices of $S^1$ and proves it kills boundaries, the chain-level fact needed for a homology invariant. Mathlib supplies the singular chain complex sphereOneSingularIntChainComplex of TopCat.sphere 1 with integer coefficients; its $H_1$ is the strict target of the circle computation.
To work with finite-support normal forms, the development introduces explicit free modules on singular $1$- and $0$-simplices, with mutually inverse maps between raw $C_1$ and free $C_1$ (and likewise in degree $0$). The free boundary sends each generator (a singular $1$-simplex) to the free generator of its terminal $0$-face minus that of its initial $0$-face.
The companion identity already shows that transporting Mathlib's boundary from free $C_1$ to free $C_0$ recovers that free boundary. The present statement is the dual transport direction: Mathlib's raw boundary, pushed along the free isomorphism, is again the free boundary.
proof idea
Mark the free-to-raw map as an isomorphism (it is the inverse half of the free $C_1$ iso), hence an epimorphism. Cancel that epi on the left of the desired equality. The resulting calculation reduces the left composite, via the inverse-hom identity of the free iso, to the free boundary alone; the right composite is identified with the free boundary by the already-proved free-to-raw boundary identity (run in reverse). No generator-wise case split is needed here.
why it matters
Commutativity of this square is the bookkeeping step that lets every later argument about free-boundary kernels transfer to Mathlib's actual singular cycles. Downstream it is used to turn free-kernel decompositions into spanning statements for closed singular $1$-chain lists, to obtain integer-valued cycle winding from directed-cycle decompositions, and to package cyclic edge-list terms whose free images match certified cycle objects. Those feed the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: every $1$-cycle is homologous to an integer multiple of the fundamental cycle.
In the Recognition forcing chain this is foundation for the circle homology computation that supports the eight-tick / $D=3$ landmarks (T7–T8), via the winding left-inverse to the fundamental class. The module doc is explicit that surjectivity of the integer comparison still needs a simplicial prism or subdivision operator Mathlib does not yet supply; this lemma closes only the transport side of that program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.