singularZeroChainFreeToChain
plain-language theorem explainer
The free ℤ-module on singular 0-simplices of S¹ maps into the raw singular chain group C₀(S¹;ℤ) by sending each free generator to the matching coproduct summand unit. Cited by anyone building the C₀ free-module isomorphism or pushing free-form boundaries back to raw chains. Construction is free-module descent of the coproduct inclusions.
Claim. There is a canonical $\mathbb{Z}$-linear map from the free module on singular $0$-simplices of $S^1$ to the degree-$0$ singular chain group $C_0(S^1;\mathbb{Z})$, sending each free generator $s$ to the unit generator of the matching coproduct summand.
background
This module lifts the path-level winding/displacement invariant on the circle to singular simplices of $\mathrm{TopCat.sphere},1$ and proves the chain-level fact that displacement kills boundaries, supplying the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The raw group $C_0(S^1;\mathbb{Z})$ is the degree-$0$ term of Mathlib's singular chain complex of the circle with integer coefficients: a coproduct of copies of $\mathbb{Z}$, indexed by singular $0$-simplices. The explicit free module is the free $\mathbb{Z}$-module on that same type of simplices. The forward arrow sends each coproduct summand to the corresponding free generator; the present map is the reverse direction.
The degree-$1$ analog already packages $C_1$ as an explicit free module via a two-sided isomorphism. The same normal form is needed in degree $0$ so boundaries computed freely can be transported back to the raw chain group.
proof idea
Universal-property one-liner. Free-module descent induces a unique $\mathbb{Z}$-linear map out of the free module on singular $0$-simplices once a target value is chosen on each generator. On generator $s$ the value is the module map that picks the unit $1$ inside the $s$-th coproduct summand of the raw chain group (via the coproduct inclusion). No further lemmas fire; the free functor supplies the arrow.
why it matters
This is the inverse half of the degree-$0$ free-module isomorphism, which records that $C_0(S^1;\mathbb{Z})$ is free on actual singular $0$-simplices. In particular the forward map is injective, so a boundary computed in the explicit free $C_0$ module transports back to the raw chain group.
Downstream, the directed-cycle free-term constructors for cyclic and oriented cyclic families package free edge-sums that must lift to genuine degree-$1$ cycles; free-form boundary vanishing is only useful once it can be read in the raw complex. The free isomorphism itself installs this arrow as its inverse.
In the Recognition chain this supports the winding homomorphism that is a left inverse to the fundamental class, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ feeding the strict T8 target. Generation (surjectivity) still needs simplicial prisms Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.