Cgrp
plain-language theorem explainer
Defines the degree-n singular chain group of a topological space X as the free ℤ-module on its singular n-simplices: the coproduct ∐_σ ℤ indexed by those simplices. Algebraic topologists and anyone building singular homology in this codebase cite it as the ambient module for cycles, boundaries, and chain maps. The body is a one-line noncomputable abbreviation as that coproduct in ModuleCat ℤ.
Claim. For a topological space $X$ and $n \in \mathbb{N}$, the degree-$n$ singular chain group $C_n(X;\mathbb{Z})$ is the coproduct $\coprod_{\sigma} \mathbb{Z}$ in $\mathbf{Mod}_{\mathbb{Z}}$, indexed by the set of continuous maps $\sigma:\Delta^n\to X$ (singular $n$-simplices of $X$).
background
Singular homology is built from free abelian groups on continuous simplices. Here the index set of degree-$n$ generators is the type of morphisms $\Delta^n\to X$ in the singular simplicial set of $X$ (the standard Mathlib TopCat.toSSet construction). Each generator contributes one copy of $\mathbb{Z}$ as an object of ModuleCat ℤ.
The ambient category is TopCat in universe 0 with integer coefficients, matching Mathlib's singular-homology stack (chain complexes of modules, colimits, and homotopy equivalences). The local module packages prism operators and face maps that act on these free modules; the chain group is the carrier on which those operators land.
Upstream, the index type is exactly the set of singular $n$-simplices. No geometric hypotheses on $X$ are imposed at this stage: every space gets a free chain group in each degree.
proof idea
Pure definitional abbreviation: expand as the coproduct (colimit) in ModuleCat ℤ of the constant family sending every singular $n$-simplex to the free rank-one module $\mathbb{Z}$. No lemmas are applied; noncomputability is inherited from the large index type and the categorical coproduct.
why it matters
This is the ambient free module for the entire singular-chain layer of the foundation. Downstream, ArcComplementAcyclic uses it as the type of 1-chains when proving that bounding is preserved by continuous maps, retractions, and Mayer–Vietoris bisections on arc complements (bounds_map, bounds_of_retract, bounds_of_mv, bounds_of_halves, bounds_of_isZero), and for elementwise commutation of chain maps with the boundary (chainMap_bnd). Those results feed acyclicity arguments for complements that support the topological side of the Recognition forcing chain (connectivity and dimension constraints tied to the eight-tick and $D=3$ landmarks). Without a uniform $C_n(X;\mathbb{Z})$, the later homology-vanishing and prism-homotopy lemmas have nowhere to live.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.