singularTwoChainFreeToChain_boundary_free
plain-language theorem explainer
Mathlib's singular boundary C₂→C₁, after transport between free and raw chain groups on S¹, equals the explicit free alternating-face boundary. Anyone equating free-coordinate and Mathlib-native boundary witnesses cites this. The proof extends by freeness on generators and reduces facewise to the three δ-maps.
Claim. The composition of the free-to-raw map on singular $2$-chains of $S^1$, Mathlib's singular boundary $d_2\colon C_2\to C_1$, and the raw-to-free map on singular $1$-chains equals the explicit free alternating-face boundary operator sending a free generator $s$ to $\mathrm{freeMk}(\delta_0 s)-\mathrm{freeMk}(\delta_1 s)+\mathrm{freeMk}(\delta_2 s)$.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of TopCat.sphere 1, and proves that alternating face displacements vanish on every singular $2$-simplex. That vanishing is the chain-level "winding kills boundaries" identity used for the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Two presentations of the singular chain groups sit side by side. Mathlib supplies the raw complex sphereOneSingularIntChainComplex (singular chains of $S^1$ with integer coefficients). The module also builds explicit free modules on the sets of singular $1$- and $2$-simplices, with maps singularTwoChainFreeToChain (free $C_2$ into the raw complex) and singularOneChainToFree (raw $C_1$ back to free $C_1$, sending each coproduct summand to the corresponding free generator). The free alternating-face operator singularTwoBoundaryFree is the explicit $\delta_0-\delta_1+\delta_2$ map on free generators.
The present theorem identifies Mathlib's $d_2$ with that free face operator after the free/raw transport.
proof idea
Extend by freeness: ModuleCat.free_hom_ext reduces the morphism equality to evaluation on free generators freeMk s for each singular $2$-simplex $s$. Unfold the free-to-raw description (freeDesc_apply) and the Mathlib boundary on a generator (singularTwoSimplex_boundary_apply), then the free boundary on a generator (singularTwoBoundaryFree_freeMk). The left-hand side becomes the alternating sum of three composite maps through the face inclusions $\delta_0,\delta_1,\delta_2$ of the singular simplicial set. Apply singularOneChainToFree_ι on each face and simplify the span-singleton maps to recover exactly $\mathrm{freeMk}(\delta_0 s)-\mathrm{freeMk}(\delta_1 s)+\mathrm{freeMk}(\delta_2 s)$.
why it matters
This is the bridge that lets free-coordinate boundary computations speak to Mathlib's native chain complex. Downstream, rawBoundary_eq_of_singularTwoBoundaryFree_eq uses it to push a free $C_2$ boundary equality into a raw $d_2$ equality, and the converse singularTwoBoundaryFree_eq_of_rawBoundary_eq pulls a raw boundary equality back to free coordinates. The latter's doc-comment states the point: it "closes the representational gap between raw-prism and free-prism witnesses; the remaining mathematical work is to build the raw prism itself."
In the larger program this supports the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (every $1$-cycle homologous to an integer multiple of the fundamental loop). The injective half is already proved by hand via the winding invariant (has infinite order). Surjectivity still needs a simplicial prism/subdivision operator that Mathlib's singular homology does not yet provide; these transport lemmas isolate that remaining construction from the free/raw bookkeeping.
Relative to the Recognition forcing chain, the degree-$1$ homology of this complex is the strict T8 target object on which the circle's fundamental class lives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.