singularZeroChainFreeIso
plain-language theorem explainer
The degree-0 singular chain group of the circle with integer coefficients is canonically isomorphic to the free ℤ-module on actual singular 0-simplices. Anyone transporting boundaries or free-module calculations back into Mathlib's raw C₀(S¹;ℤ) cites this iso. The maps are the standard free-desc / coproduct-desc pair; both triangle identities are checked by free and Sigma extensionality plus zsmul bookkeeping.
Claim. There is a canonical isomorphism of $\mathbb{Z}$-modules $C_0(S^1;\mathbb{Z}) \cong \mathbb{Z}\langle\{\text{singular $0$-simplices of $S^1$}\}\rangle$, with forward map sending each coproduct summand generator to the corresponding free generator, and inverse sending each free generator to the matching coproduct summand unit.
background
The module works at the chain level of singular homology of the topological circle $S^1 = \mathrm{TopCat.sphere},1$. Mathlib supplies the singular chain complex $C_\bullet(S^1;\mathbb{Z})$; its degree-0 object is a big coproduct of copies of $\mathbb{Z}$, one per continuous map $\Delta^0\to S^1$. That presentation is awkward for explicit free-module arithmetic (boundaries of free 1-chains, cyclic edge families).
The companion object is the free module on the type of singular 0-simplices: $\mathbb{Z}\langle\mathrm{SingularZeroSimplex}\rangle$. Two mutually inverse arrows are already defined: the coproduct-desc map from raw $C_0$ into the free module (each summand spans its free generator), and the free-desc map back (each free generator lands on the unit of its coproduct summand).
Upstream, sphereOneSingularIntChainComplex is exactly Mathlib's singular chain complex of the circle; the free module and the two arrows are the $C_0$ analogs of the degree-1 free-iso package used for winding.
proof idea
The isomorphism is assembled by setting the forward arrow to the coproduct-desc map into the free module and the inverse to the free-desc map back into raw $C_0$.
Forward-then-inverse equals identity: extend over the Sigma coproduct, then over each ModuleCat hom, then pointwise on coefficients. Unfolding the desc and the to-span-singleton map reduces to $n\cdot\iota_s(1)=\iota_s(n)$, which is map_zsmul.
Inverse-then-forward equals identity: free-hom extensionality on generators. The free-desc of a generator is the unit of the matching Sigma summand; feeding that unit through the coproduct-desc recovers the free generator by the to-span-singleton evaluation at 1.
why it matters
This iso is the $C_0$ twin of the degree-1 free-iso. Its forward arrow is therefore mono, which is recorded as injectivity of the raw-to-free map: boundaries computed in the explicit free $C_0$ module transport faithfully back into Mathlib's chain group.
Downstream, cyclic and oriented-cyclic edge families build DirectedCycleFreeTerms whose free edge-chains are genuine degree-1 cycles (free boundary zero) with integer winding. Those packages discharge the homological half of cyclic extraction inside balanced-flow decompositions; the free $C_0$ calculus they rely on is only legitimate because this iso identifies free and raw degree-0 groups.
In the broader Recognition story the module supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via winding (the T8-adjacent circle computation). Surjectivity still needs a prism/subdivision operator Mathlib does not yet provide; this definition does not close that gap, but it keeps free-module bookkeeping honest on the boundary side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.