singularOneChainFreeToChain_freeMk
plain-language theorem explainer
On each free generator labelled by a singular 1-simplex of S¹, the free-to-chain comparison map equals the corresponding coproduct inclusion of the unit in C₁(S¹;ℤ). Anyone transporting free-module identities into Mathlib singular chains cites this evaluation lemma. The proof is a one-line unfold of the freeDesc definition plus freeDesc_apply.
Claim. Let $s$ be a singular $1$-simplex of $S^1$. Applying the free-to-chain map $\mathrm{Free}(\mathrm{Sing}_1(S^1))\to C_1(S^1;\mathbb{Z})$ to the free generator of $s$ yields the coproduct summand generator $\iota_s(1)\in\bigoplus_s\mathbb{Z}$.
background
The module CircleWindingChain lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$. The free $\mathbb{Z}$-module on those simplices is compared to Mathlib's singular chain group $C_1(S^1;\mathbb{Z})$, which is realised as a coproduct of copies of $\mathbb{Z}$ indexed by the same simplices.
The comparison arrow is defined by ModuleCat.freeDesc: on each free generator it inserts the unit into the matching coproduct summand. This lemma records that evaluation on free generators.
proof idea
One-line term proof. Rewrite by the definition of the free-to-chain map (itself a freeDesc of the family of coproduct inclusions), then apply ModuleCat.freeDesc_apply, which states that freeDesc evaluated on freeMk s recovers the component at $s$.
why it matters
This is the generator-wise normalisation that lets every later free-module identity be pushed into raw singular chains. Downstream consumers include the free-boundary transport singularOneChainFreeToChain_boundary_free, the constant-simplex boundary identities, the free-prism generation lemmas that produce closed $1$-cycles homologous to integer multiples of the fundamental cycle, and the winding-chain evaluation on free generators (including constants, which get winding zero).
In the module's programme this sits under the "kills-boundaries" and generation halves of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: free generators must land on the correct coproduct basis vectors before boundary and winding maps can be compared. It does not itself touch the Recognition forcing chain (T0–T8), but it is infrastructure for the circle homology computation that underwrites the eight-tick / winding story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.