sCgrp
plain-language theorem explainer
The degree-n small singular chain group is the free abelian group on those singular n-simplices that land in U or V. It is realized as a coproduct of copies of ℤ indexed by the small-simplex type. Anyone building the small chain complex or the Mayer–Vietoris inclusion cites this object. The body is a one-line coproduct abbreviation in ModuleCat ℤ.
Claim. For open sets $U,V \subseteq X$ and $n \in \mathbb{N}$, write $S_n(U,V)$ for the set of singular $n$-simplices of $X$ that are small relative to $\{U,V\}$. The small chain group is the free $\mathbb{Z}$-module $C_n^{\mathrm{sm}}(U,V) := \bigoplus_{\sigma \in S_n(U,V)} \mathbb{Z}$, presented as a coproduct in the category of $\mathbb{Z}$-modules.
background
This module sits in the singular Mayer–Vietoris development for a space $X$ with a two-set cover $(U,V)$. Ordinary singular chains $C_n(X)$ are free on all continuous maps $\Delta^n \to X$. The small complex keeps only those simplices whose image lies in $U$ or in $V$ (the predicate Small), so that the usual MV connecting maps stay inside the subcomplex.
The index type is the subtype of singular $n$-simplices satisfying that smallness condition. Each generator is a copy of $\mathbb{Z}$ in ModuleCat, and the full group is their categorical coproduct. Downstream maps (generators, inclusion into full singular chains, and the alternating-face boundary) are defined by the universal property of that coproduct.
The surrounding imports are Mathlib homology and biproduct infrastructure plus the local singular prism, pair, and subdivision layers that supply faces and smallness closure under face operators.
proof idea
Pure definitional abbreviation: no proof obligations. The right-hand side is the coproduct $\coprod_{t : S_n(U,V)} \mathbb{Z}$ in ModuleCat ℤ, with index type the subtype of small singular $n$-simplices. Noncomputable only because the ambient singular set and coproduct packaging are.
why it matters
This is the carrier object for the entire small chain complex used in the singular Mayer–Vietoris sequence. Inclusion into ordinary singular chains, the retraction that splits it on small generators, the small boundary (alternating faces, closed by smallness of faces), and the span-membership lemmas that identify the image of inclusion with the submodule generated by small simplices all take values in or out of this group.
In the Recognition foundation stack the construction is classical algebraic topology scaffolding: it supplies the chain-level MV exact sequence that later geometric and forcing arguments can quote when they need excision or cover-controlled homology. It does not itself invoke the J-cost, $\varphi$-ladder, or T0–T8 forcing steps; those sit upstream or downstream of the topological layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.