singularTwoChainFreeToChain
plain-language theorem explainer
The free ℤ-module on singular 2-simplices of S¹ maps into Mathlib's singular chain group C₂(S¹;ℤ) by sending each free generator to the matching coproduct summand. Algebraic consumers of free prisms cite this to push free 2-chains into the raw complex before reading boundaries. The map is the universal free-module arrow that places 1 on the corresponding Sigma inclusion.
Claim. There is a canonical $\mathbb{Z}$-linear map from the free module on singular $2$-simplices of $S^1$ into the degree-$2$ term of Mathlib's singular chain complex $C_\bullet(S^1;\mathbb{Z})$, sending the free generator of each singular $2$-simplex $\sigma$ to the generator $1$ of the corresponding coproduct summand.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills $2$-boundaries, the chain-level fact needed for a winding homomorphism on $H_1(S^1;\mathbb{Z})$. Mathlib presents $C_n(S^1;\mathbb{Z})$ as a coproduct of copies of $\mathbb{Z}$, one per singular $n$-simplex; the project also keeps an explicit free module on those simplices for hand-built prism algebra.
SingularTwoSimplex is a point of the singular simplicial set of TopCat.sphere 1 in degree $2$. singularTwoChainFree is the free $\mathbb{Z}$-module on that type. sphereOneSingularIntChainComplex is Mathlib's singular chain complex of $S^1$ with integer coefficients, whose degree-$1$ homology is the strict T8 target.
Degree-$0$ and degree-$1$ already have the opposite arrows (raw chains into free modules). This definition supplies the free-to-raw direction in degree $2$, so free prism constructions can be read as genuine $2$-chains in Mathlib's complex.
proof idea
One-line universal-property definition. ModuleCat.freeDesc builds a map out of the free module by naming the image of each generator. For each singular $2$-simplex $s$, the image is the composite of the coproduct summand inclusion $\Sigma.\iota$ at $s$ with the unit $1\in\mathbb{Z}$. No further lemmas are applied; the arrow is exactly the free-module adjunction counit on the family of summands that underlies Mathlib's $C_2$.
why it matters
Free prism algebra lives on singularTwoChainFree; Mathlib boundaries and toCycles live on sphereOneSingularIntChainComplex.X 2. This map is the bridge. Downstream, rawBoundary_eq_of_singularTwoBoundaryFree_eq transports free $C_2$ boundary equalities into raw $d_2$ equalities; constantSingularOneSimplex_raw_boundary and constantSingularOneCycle_bounds use it for the constant prism; closedSingularOneCycle_bounds_of_free_boundary and closedSingularOneCycle_boundary_generate_of_freePrismToFundamental consume free $2$-chains after transport; orientedCyclicFamilies_explicitRawPrism_generate_of_freePrism packages the free prism as an explicit raw prism.
Together these feed the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: every closed singular $1$-cycle is homologous to an integer multiple of the fundamental cycle. That comparison is the remaining half of the strict T8 circle computation after the winding left-inverse (kills-boundaries plus once-around evaluation) is in place. No new physics constant is fixed here; the declaration is pure chain-level scaffolding for that isomorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.