singularTwoBoundaryFree
plain-language theorem explainer
Explicit free-module boundary from singular 2-chains to singular 1-chains on S¹: each generator 2-simplex maps to the alternating sum of its three 1-faces. Cited wherever free prisms, geodesic steps, or closed-edge nullhomotopies are checked algebraically. Defined by freeDesc of the three face operators of the singular simplicial set of the circle.
Claim. The free $\mathbb{Z}$-module boundary $\partial_2^{\mathrm{free}} : C_2^{\mathrm{free}}(S^1;\mathbb{Z}) \to C_1^{\mathrm{free}}(S^1;\mathbb{Z})$ sends each singular $2$-simplex generator $s$ to $[\delta_0 s]-[\delta_1 s]+[\delta_2 s]$, the alternating sum of its three singular $1$-faces in the singular simplicial set of $S^1$.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills 2-boundaries, the chain-level fact that makes winding a homology invariant. The free modules here are the explicit $\mathbb{Z}$-span of actual singular simplices of $\mathrm{TopCat.sphere},1$, not the raw singular chain groups of Mathlib's complex.
SingularTwoSimplex is a $2$-simplex in that singular simplicial set. singularTwoChainFree (resp. singularOneChainFree) is the free $\mathbb{Z}$-module on those $2$-simplices (resp. $1$-simplices). Face maps $\delta_i$ are the standard simplicial face operators of $\mathrm{TopCat.toSSet}$.
The companion map from the raw singular $C_1$ into the free $1$-module sends each coproduct summand to the matching free generator. The free boundary defined here is the algebraic target used by hand-built prism and geodesic constructions.
proof idea
Definition by universal property of free modules: ModuleCat.freeDesc extends the assignment on generators. On a singular $2$-simplex $s$, the image is the integer linear combination freeMk($\delta_0 s$) $-$ freeMk($\delta_1 s$) $+$ freeMk($\delta_2 s$), using the three face maps of the singular simplicial set of $S^1$. No further lemmas; the body is exactly that free extension of the alternating face sum.
why it matters
This is the algebraic $\partial_2$ against which every free-prism and geodesic construction in the module is checked. Downstream consumers include: constant $1$-simplices bound constant $2$-simplices; closed singular $1$-cycles bound when equal to a free boundary; geodesic free chains self-bound and step by full turns modulo an explicit free $2$-chain; oriented cyclic families generate free prisms whose free boundary is edge sum minus a fundamental multiple.
Together with simplexDisplacement_boundary (alternating face sum of displacements vanishes by $2$-simplex telescoping), it supplies the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$ via winding. The module doc frames the remaining open half as generation: every $1$-cycle homologous to an integer multiple of the fundamental cycle, needing a simplicial prism/subdivision operator Mathlib does not yet provide. No RS forcing-chain step (T0–T8) is claimed here; the landmark is the classical $H_1(S^1)\cong\mathbb{Z}$ comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.