singularZeroChainToFree
plain-language theorem explainer
The degree-0 singular chain group of the circle maps to the free ℤ-module on its singular 0-simplices by sending each coproduct summand to the matching free generator. Anyone comparing Mathlib singular chains to explicit free-chain coordinates for H₁(S¹) cites this arrow. The construction is a one-line coproduct universal-property map via Sigma.desc and span-of-generator.
Claim. There is a morphism of $\mathbb{Z}$-modules $C_0(S^1;\mathbb{Z})\to \mathbb{Z}^{(S^1_0)}$ from the raw singular chain group of the circle in degree $0$ to the free module on its singular $0$-simplices, sending the coproduct summand indexed by each singular $0$-simplex $s$ to the free generator $\langle s\rangle$.
background
This module lifts the path-level winding and displacement invariant on the circle to singular simplices of TopCat.sphere 1, and proves the chain-level identity that winding kills boundaries. That identity, with the once-around generator mapping to 1, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Upstream, the integer singular chain complex of the circle is Mathlib's singular chain complex functor applied to TopCat.sphere 1; its degree-0 object is the raw group $C_0(S^1;\mathbb{Z})$. A singular 0-simplex is an element of the singular simplicial set in dimension 0. The explicit free module is the free $\mathbb{Z}$-module on that type of 0-simplices.
The comparison arrow defined here is the bridge from Mathlib's coproduct presentation of $C_0$ to those free generators, so later boundary and cycle statements can be written in free-module coordinates.
proof idea
Degree 0 of the singular chain complex is a coproduct of copies of $\mathbb{Z}$, one per singular 0-simplex. The definition applies the coproduct universal property (Sigma.desc): on the summand indexed by $s$, it takes the unique $\mathbb{Z}$-linear map sending $1$ to the free generator of $s$ (LinearMap.toSpanSingleton composed with ModuleCat.freeMk, packaged as a ModuleCat homomorphism). No further lemmas are needed; the body is pure universal-property assembly.
why it matters
This arrow is the degree-0 leg of the free-chain comparison used throughout the winding-chain development. Downstream, the boundary-transport theorems identify Mathlib's singular boundary with the explicit free boundary (terminal minus initial) precisely by composing with this map; those identities are the cancellation surface for cycle decomposition.
It also appears in the free isomorphism at degree 0 and in the packaging of directed cycle pieces: a cyclically connected family of edges becomes a genuine degree-1 cycle whose free edge-chain matches the Mathlib cycle after transport. That packaging discharges the homological obligation of cyclic extraction from balanced flows.
In the broader Recognition chain, the module targets the strict computation of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (the T8-adjacent singular-homology landmark). The generation half still needs a prism or subdivision operator Mathlib does not yet supply; this definition only equips the free $C_0$ side of the comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.