singularTwoChainFreeIso
plain-language theorem explainer
The degree-2 singular chain group of the circle with integer coefficients is canonically isomorphic to the free ℤ-module on continuous maps Δ²→S¹. Algebraic topologists proving the H₁(S¹;ℤ)≅ℤ comparison cite it to pass between Mathlib's coproduct chains and free-coordinate chains. Both directions are the already-built free-module maps; the two triangle identities are checked generator-wise by module extensionality.
Claim. There is a canonical isomorphism of $\mathbb{Z}$-modules $C_2(S^1;\mathbb{Z})\cong\mathbb{Z}[\mathrm{Sing}_2(S^1)]$, where the right-hand side is the free module on continuous maps $\Delta^2\to S^1$. The forward map sends each coproduct-summand generator to the matching free generator; the inverse recovers the summand inclusion.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$ and proves that displacement kills boundaries of $2$-simplices. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
Mathlib presents $C_n(S^1;\mathbb{Z})$ as a coproduct of copies of $\mathbb{Z}$, one per singular $n$-simplex. The sibling free module on the type of actual continuous maps $\Delta^2\to S^1$ is the coordinate-friendly twin of that group. The degree-$1$ analog already identifies $C_1$ with its free twin; the present declaration is the degree-$2$ twin.
Upstream, the singular chain complex of $\mathrm{TopCat.sphere},1$ with integer coefficients is the exact chain-level object whose degree-$1$ homology is the strict target of the circle computation. The two maps assembling the iso send free generators to coproduct summands and conversely.
proof idea
The isomorphism is packaged directly: forward arrow is the map from raw $C_2$ to the free module on singular $2$-simplices; inverse is the free descent that sends each free generator to the matching coproduct summand generator (value $1$).
The composite free$\to$raw$\to$free is the identity by free-module extensionality on generators: after unfolding free descent and the coproduct description, the composite hits the free generator and simplifies to $\mathrm{id}$.
The composite raw$\to$free$\to$raw is the identity by $\Sigma$-extensionality then module-hom extensionality then pointwise extensionality on coefficients: each summand inclusion composed with the two maps recovers itself after rewriting through $\mathrm{toSpanSingleton}$ and $\mathrm{zsmul}$.
why it matters
Without this iso, boundary computations live in Mathlib's opaque coproduct presentation and cannot be compared to free-coordinate prism witnesses. Downstream, the converse transport theorem uses it: if a raw singular $2$-chain has raw boundary equal to the image of a free $C_1$ chain, then its free-coordinate representative has that free boundary. That closes the representational gap between raw-prism and free-prism witnesses; the remaining work is to build the raw prism itself.
In the broader Recognition chain this sits inside the singular-homology computation of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, the topological half of the eight-tick/circle story that feeds the forcing chain (T7 octave, and ultimately T8 on spatial dimension). The module itself uses no axioms or sorry; this definition is pure scaffolding glue, not a new geometric claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.