singularTwoChainFree
plain-language theorem explainer
The free abelian group on singular 2-simplices of the circle S¹, written as an object of ModuleCat ℤ. It is the ambient chain group C₂(S¹;ℤ) used throughout the winding-chain development. Anyone building free 2-chains, prism fillings, or cone corrections cites it. The body is a one-line free-module construction on the type of singular 2-simplices.
Claim. Let $C_2^{\mathrm{sing}}(S^1;\mathbb{Z})$ denote the free $\mathbb{Z}$-module on the set of continuous maps $\Delta^2\to S^1$ (singular $2$-simplices of the topological circle). As an object of the category of $\mathbb{Z}$-modules, this is the free module generated by that set.
background
The module CircleWindingChain lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex $F$, the alternating face sum of displacements vanishes. That identity is the chain-level reason winding descends to $H_1$.
A singular $2$-simplex is a continuous map $\Delta^2\to S^1$, i.e. an element of the degree-$2$ object of the singular simplicial set of TopCat.sphere 1. The free $\mathbb{Z}$-module on that set is the raw singular chain group $C_2(S^1;\mathbb{Z})$ in which one writes finite integer combinations of such maps.
This sits next to the analogous free module on singular $1$-simplices. Boundaries, cones, geodesic corrections, and prism generators are all morphisms or elements in these free modules, not yet quotiented by homology.
proof idea
One-line definitional wrapper: apply the free-module functor ModuleCat.free ℤ to the type of singular $2$-simplices of $S^1$. No further proof obligations; the abbrev simply names that free object in ModuleCat ℤ.
why it matters
This is the ambient $C_2$ in which every explicit filling lives. Downstream consumers include closedSingularOneCycle_bounds_of_free_boundary (a closed edge is a cycle-boundary once it is the free boundary of some $B$ here), closedSingularOneCycle_boundary_generate_of_freePrismToFundamental (prism to $n$ times the fundamental cycle), and coneSingularTwoChainOfPathFamily (sum of cone $2$-simplices over a path family).
Generation targets such as orientedCyclicFamilies_freePrism_generate and the path-base/path-cone correction props quantify over existence of an element of this free module with a prescribed free boundary. The geodesic step theorem likewise produces a $K$ here whose free boundary accounts for full-turn shifts.
In the module narrative, this free $C_2$ is the algebraic home for the missing Mathlib prism/subdivision half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding already kills boundaries and hits the generator; surjectivity needs hand-built free $2$-chains of this type. No T0–T8 forcing step is claimed here; the object is pure singular-chain scaffolding for the circle homology split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.