singularTwoChainToFree
plain-language theorem explainer
Canonical ℤ-linear map from Mathlib's raw singular chain group C₂(S¹;ℤ) onto the free module generated by actual continuous maps Δ²→S¹. Anyone transporting prism or boundary witnesses between raw and free coordinates cites it. The body is the coproduct universal property: each summand generator is sent to the corresponding free singleton.
Claim. There is a canonical morphism of $\mathbb{Z}$-modules $C_2(S^1;\mathbb{Z})\to\mathbb{Z}\langle\{\text{singular }2\text{-simplices of }S^1\}\rangle$ sending each coproduct summand generator to the free basis vector of the corresponding continuous map $\Delta^2\to S^1$.
background
The module builds the winding 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}$. Mathlib supplies the raw singular chain complex sphereOneSingularIntChainComplex; its degree-2 object is a huge coproduct of copies of $\mathbb{Z}$, one per singular 2-simplex, packaged as an abstract ModuleCat object rather than an explicit free module.
SingularTwoSimplex is the type of actual continuous maps $\Delta^2\to S^1$ in the singular simplicial set. singularTwoChainFree is the free $\mathbb{Z}$-module on that type. Parallel maps already exist in degrees 0 and 1 (singularZeroChainToFree, singularOneChainToFree); this is the degree-2 twin. Face maps on 2-simplices (both the chain-level face and the topological prism face) are used downstream when boundaries are compared.
proof idea
One-line definition via the coproduct universal property. Sigma.desc assembles a map out of the raw degree-2 chain group by specifying, on each summand indexed by a singular 2-simplex $s$, the $\mathbb{Z}$-linear map that sends $1$ to the free basis vector of $s$ (LinearMap.toSpanSingleton composed with ModuleCat.freeMk, then wrapped as a ModuleCat morphism). No further lemmas are invoked.
why it matters
Closes the representational gap between Mathlib's raw $C_2$ and free-coordinate 2-chains. It is the forward half of singularTwoChainFreeIso (the degree-2 analog of the degree-1 free isomorphism). Downstream, singularTwoBoundaryFree_eq_of_rawBoundary_eq uses it to transport boundary equalities: if a raw 2-chain has raw boundary equal to the image of a free 1-chain, the free image has that free boundary. That transport lets orientedCyclicFamilies_freePrism_generate_of_explicitRawPrism promote an explicit raw-prism witness to a free-prism witness, so the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (the missing surjectivity toward the T8 target) can be stated in free coordinates once a raw prism is built. No new topology is proved here; the map is pure bookkeeping that makes prism and boundary arguments interchangeable across the two presentations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.