singularOneChainToFree_
plain-language theorem explainer
On each singular 1-simplex summand, the comparison from the coproduct of integer lines into the free Z-module on singular 1-simplices is exactly the singleton span map sending 1 to that generator. Anyone wiring free-module presentations of singular 1-chains on S^1 would cite it. The proof is a one-line rewrite of the coproduct description against the sigma-inclusion universal property.
Claim. For every singular $1$-simplex $s$ of $S^1$, the composite of the coproduct inclusion of the $s$-th copy of $\mathbb{Z}$ with the comparison map into the free $\mathbb{Z}$-module on singular $1$-simplices equals the $\mathbb{Z}$-linear map sending $1$ to the free generator labelled by $s$.
background
The ambient module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$, and proves that displacement kills boundaries of singular $2$-simplices. That identity is the chain-level fact making winding a homology invariant, and (with the once-around generator mapping to $1$) supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex here is an object of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$. Singular $1$-chains are assembled as free $\mathbb{Z}$-modules (and as coproducts of copies of $\mathbb{Z}$) on that set of generators. The comparison map in the statement is the canonical identification of those two presentations: from the coproduct of integer lines indexed by singular $1$-simplices into the free module on the same index set.
This lemma records the component of that comparison on a single generator summand.
proof idea
One-line rewrite proof. Unfold the definition of the comparison map (which is the coproduct desc of the family of singleton span maps), then apply the sigma-inclusion identity for that desc: the composite of the $s$-th inclusion with the desc is exactly the $s$-th family member, namely the linear map to the free module sending $1$ to the free generator of $s$.
why it matters
The free-module presentation of singular $1$-chains is the algebraic substrate on which the winding homomorphism acts. Pinning the comparison on generators is bookkeeping needed before one can transport the simplex displacement invariant from individual singular $1$-simplices to integer linear combinations and then to cycles.
In the module's larger program, that transport yields a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). The converse generation half still needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet supply. No Recognition forcing-chain step (T0–T8) is touched directly; the result is pure singular-homology infrastructure for the circle winding story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.