singularOneChainFreeToChain
plain-language theorem explainer
Canonical map from the free ℤ-module on singular 1-simplices of S¹ into the degree-1 singular chains C₁(S¹;ℤ), sending each free generator to its matching coproduct summand. Downstream cycle-generation and free-boundary arguments cite it constantly. Built by the free-module universal property (freeDesc on the unit of each summand).
Claim. There is a canonical $\mathbb{Z}$-linear map from the free module on singular $1$-simplices of $S^1$ into $C_1(S^1;\mathbb{Z})$ that sends each free generator to the generator of the corresponding coproduct summand in the singular chain module.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact needed for a winding homomorphism on $H_1(S^1;\mathbb{Z})$. The long-term target is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (and, in the RS chain, the strict T8 homology computation).
SingularOneSimplex is a $1$-simplex in the singular simplicial set of TopCat.sphere 1. singularOneChainFree is the free $\mathbb{Z}$-module on that type. sphereOneSingularIntChainComplex is Mathlib's singular chain complex of $S^1$ with integer coefficients; its degree-$1$ object is the usual $C_1(S^1;\mathbb{Z})$, realized as a coproduct of copies of $\mathbb{Z}$ indexed by singular $1$-simplices.
The free module and the singular chain module are therefore parallel presentations of the same generators. This definition is the comparison arrow that puts free-coordinate bookkeeping back into the actual chain complex.
proof idea
One-line definition via the free-module universal property. ModuleCat.freeDesc builds a map out of singularOneChainFree from a family of maps on generators. On each singular $1$-simplex $s$, the component is the coproduct inclusion of the $s$-summand of $C_1(S^1;\mathbb{Z})$, evaluated at $1\in\mathbb{Z}$. No further lemmas are applied.
why it matters
Without this arrow, free-chain constructions (cyclic edge families, oriented cycles, prism-to-fundamental comparisons) cannot be read as genuine singular $1$-chains or cycles. Downstream consumers include d_singularOneChainFreeToChain_eq_zero_of_freeBoundary_zero, the prism generation theorems closedSingularOneCycle_boundary_generate_of_freePrismToFundamental and its raw variant, and the packaging structures DirectedCycleFreeTerm / directedCycleFreeTerm_of_cyclicFamily / directedCycleFreeTerm_of_orientedCyclicFamily.
Those objects discharge the homological half of finite-flow cycle extraction on $S^1$: free edge sums with vanishing free boundary lift to actual degree-$1$ cycles. That is the generation side of the integer comparison map toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, complementary to the winding left-inverse already obtained from simplexDisplacement and the kills-boundaries identity. In the RS forcing narrative this sits under the strict T8 homology target for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.