singularTwoBoundaryFree_eq_of_rawBoundary_eq
plain-language theorem explainer
If a raw singular 2-chain on S¹ has boundary equal to the image of a free 1-chain u, then the free-coordinate representative of that 2-chain has free boundary exactly u. Anyone transporting prism witnesses between Mathlib's singular chains and the explicit free modules on actual simplices cites this. The proof is a short iso-chase: commute the free boundary past the degree-2 free/raw isomorphism, cancel both round-trips, and read off u.
Claim. Let $b\in C_2(S^1;\mathbb{Z})$ be a raw singular $2$-chain and $u$ an element of the free $\mathbb{Z}$-module on actual singular $1$-simplices. If the raw boundary $d_2(b)$ equals the image of $u$ under the free-to-raw map $C_1^{\mathrm{free}}\to C_1(S^1;\mathbb{Z})$, then the free boundary of the free-coordinate representative of $b$ equals $u$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries of $2$-simplices, the chain-level fact needed for a winding homomorphism on $H_1(S^1;\mathbb{Z})$. Mathlib supplies the singular chain complex sphereOneSingularIntChainComplex; the project also builds explicit free modules on the actual singular $1$- and $2$-simplices of $\mathrm{TopCat.sphere},1$, with isomorphisms singularOneChainFreeIso and the degree-$2$ analogue identifying free and raw coordinates.
The free-to-raw map on $1$-chains sends each free generator to the matching coproduct summand; its inverse extracts finite-support free coordinates. The free boundary map is the composite that takes a free $2$-chain to free $1$-coordinates of its raw boundary. This theorem is the converse transport: raw boundary data that already lands in the image of a free $1$-chain can be read entirely in free coordinates.
proof idea
Start from the naturality identity that free-to-raw on degree $2$ intertwines free boundary with raw $d_2$ (singularTwoChainFreeToChain_boundary_free). Apply both sides to the free representative of $b$, then simplify the composite. Cancel the degree-$2$ free/raw round-trip via singularTwoChainFreeIso.hom_inv_id, so free-to-raw of the free representative recovers $b$. Substitute the hypothesis that $d_2(b)$ is the free-to-raw image of $u$. Cancel the degree-$1$ free/raw round-trip via singularOneChainFreeIso.inv_hom_id. The resulting equality is free-boundary(free-rep$(b))=u$ after symmetry.
why it matters
Generation of $H_1(S^1;\mathbb{Z})$ by the fundamental cycle needs prism/subdivision witnesses. Those witnesses can be built either as raw singular $2$-chains or in free coordinates; this lemma closes the representational gap so a raw-prism construction yields a free-prism target automatically.
Downstream, orientedCyclicFamilies_freePrism_generate_of_explicitRawPrism applies exactly this transport: given an explicit raw prism for an oriented cyclic family, it obtains the free-coordinate prism hypothesis. The doc-comment there notes the free-prism statement is therefore no stronger in substance than constructing the raw singular $2$-chain.
In the broader Recognition chain this sits under the strict T8 target that $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (split-injective half already comes from winding; surjectivity needs these prisms). No axioms or sorry are involved here; the remaining work flagged by the doc-comment is building the raw prism itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.