singularZeroChainToFree_injective
plain-language theorem explainer
The canonical map from the raw singular 0-chain group of the circle to the explicit free ℤ-module on singular 0-simplices is injective. Anyone moving a vanishing free-C₀ boundary back into the raw chain complex cites this. The argument is a short instance chase: the map is the forward half of a recorded isomorphism, hence mono, hence injective on underlying maps.
Claim. The canonical $\mathbb{Z}$-linear map $C_0(S^1;\mathbb{Z})\to\mathbb{Z}^{(S^1_0)}$ that sends each coproduct summand of a singular $0$-simplex to the corresponding free generator is injective.
background
The module builds the winding/displacement invariant on singular 1-simplices of $S^1$ and proves it kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Chains appear in two presentations: Mathlib's raw singular chain groups, and explicit free modules on actual singular simplices.
The map in question sends the degree-0 raw group into the free module on singular 0-simplices by taking each Sigma summand to the free generator of that simplex. Its inverse and the two-sided identities are packaged as an isomorphism of modules in the category of $\mathbb{Z}$-modules. The free presentation is where combinatorial face and boundary formulas are written; injectivity is what lets a free-side vanishing statement pull back to the raw complex.
Upstream, the isomorphism records that the forward map is invertible, so it is mono. Downstream work only needs the injective half of that fact.
proof idea
Register that the map is an isomorphism by rewriting it as the forward arrow of the recorded free-module isomorphism and invoking the instance. Then apply the standard equivalence "mono in ModuleCat iff the underlying linear map is injective" and discharge mono from the iso instance. No direct kernel computation is needed.
why it matters
This is the transport lemma that makes free-module boundary calculations usable on the raw singular complex. Its sole recorded consumer is the theorem that if an explicit free 1-chain has free boundary zero, then the image 1-chain in the raw complex has raw $C_1\to C_0$ boundary zero: that proof applies this injectivity to the free-to-raw comparison.
In the module's larger program, free-side telescoping (affine edges of $\Delta^2$, path-displacement additivity and homotopy invariance) shows winding kills boundaries. To conclude that a raw 1-cycle has vanishing winding whenever it is a boundary, one must move vanishing free boundaries back into the raw $C_0$ group; injectivity of the degree-0 comparison is exactly that bridge. It supports the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via the winding homomorphism, without touching the still-open generation/surjectivity half that needs a prism or subdivision operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.