smallSpan
plain-language theorem explainer
Integer singular n-chains generated by simplices whose image lies wholly in U or wholly in V form a submodule of the full singular chain group. Anyone proving singular Mayer–Vietoris or barycentric-subdivision cover arguments cites this object. The definition is the plain ℤ-span of the corresponding generator units.
Claim. For subsets $U,V\subseteq X$ and $n\in\mathbb{N}$, the small-span submodule is $\mathrm{span}_{\mathbb{Z}}\{\,e_\sigma:\sigma\text{ is a singular }n\text{-simplex with }\mathrm{im}\,\sigma\subseteq U\text{ or }\mathrm{im}\,\sigma\subseteq V\,\}$ inside the degree-$n$ singular chain group of $X$.
background
Work is in the singular chain complex of a topological space $X$ (as a TopCat object). The degree-$n$ chain group is the free $\mathbb{Z}$-module on the set of singular $n$-simplices: each simplex $\sigma$ contributes a generator unit $e_\sigma$.
Relative to a pair of subsets $U,V\subseteq X$, a simplex is called small when its geometric image lies entirely in $U$ or entirely in $V$. Faces of small simplices remain small, so the notion is compatible with the boundary operator.
The local setting is the singular Mayer–Vietoris apparatus: one needs a submodule of “chains supported in the cover pieces” before comparing the full complex to the complex built only from small simplices, and before running subdivision until every chain becomes small.
proof idea
Pure definition: take the set of all generator units $e_\sigma$ for which $\sigma$ is small relative to $U,V$, and form its $\mathbb{Z}$-span as a submodule of the singular chain group. No lemmas are applied; the body is a single Submodule.span of that set comprehension.
why it matters
This is the ambient submodule for every small-chain lemma in the singular Mayer–Vietoris module. Downstream results show: generator units of small simplices lie in it; the inclusion from the small-chain group lands in it; the singular subdivision operator and all its iterates preserve it; and, for an open cover $U\cup V=X$, every chain has some subdivision iterate inside it (uniform smallness). Those facts are the algebraic engine that identifies homology computed from small chains with ordinary singular homology, which is the classical input to the Mayer–Vietoris long exact sequence. In the Recognition foundation stack this sits under the singular-homology scaffolding that later feeds geometric and forcing arguments, not under the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.