singularOneChainToFree
plain-language theorem explainer
Canonical comparison from the degree-1 singular chain group of the circle to the free ℤ-module on its singular 1-simplices, sending each coproduct summand to the matching free generator. Downstream free-boundary kernel, directed-cycle, and integer-winding arguments all route through this map. The definition is the coproduct universal property (Sigma.desc) into free generators via span-singleton maps.
Claim. There is a canonical $\mathbb{Z}$-module homomorphism $C_1(S^1;\mathbb{Z})\to\mathbb{Z}^{(S_1(S^1))}$ from the degree-$1$ singular chain group of the circle to the free module on its singular $1$-simplices, sending each coproduct summand generator to the corresponding free generator.
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, the chain-level fact needed for a homology invariant. The long-term target is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (and, with generation, the full comparison), which is the strict T8 homology landmark.
The domain is the degree-$1$ term of Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with integer coefficients: the exact chain-level object whose $H_1$ is the T8 target. The codomain is the free $\mathbb{Z}$-module on the type of actual singular $1$-simplices in the singular simplicial set of the circle. Working in the free module lets later arguments decompose kernels and cycles by listing generators, then push conclusions back to raw singular chains.
proof idea
One-line definitional construction, not a tactic proof. The singular chain group in degree 1 is (up to the usual Mathlib packaging) a coproduct over singular $1$-simplices. Apply the coproduct universal property (Sigma.desc): on the summand indexed by a singular $1$-simplex $s$, take the module homomorphism that sends $1$ to the free generator of $s$ (LinearMap.toSpanSingleton composed with ModuleCat.freeMk), packaged as a ModuleCat arrow. No further lemmas are invoked.
why it matters
This comparison is the bridge every free-side cycle argument uses to talk about actual singular chains. Downstream, the free-boundary kernel decomposition implies raw-chain spanning of cycles by applying the homomorphism to a free chain; the directed-cycle kernel theorem implies integer winding for all singular $1$-cycles the same way; closed-edge prism consumers and the concrete cyclic edge-list term structure record equality of free images under this map.
In the Recognition forcing chain, T8 forces $D=3$ spatial dimensions; the circle computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is the model 1-dimensional homology check that the singular-chain infrastructure must pass before higher-dimensional claims. The module doc is explicit that generation (surjectivity of the integer comparison) still needs a simplicial prism/subdivision operator Mathlib does not yet supply; this map is the free-side handle those generation proofs will use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.