sgen
plain-language theorem explainer
Canonical generator map sending 1 in ℤ to the basis element of the free small-chain module indexed by a given small singular n-simplex. Algebraic topologists building the small singular complex (for Mayer–Vietoris on an open cover U ∪ V) cite it as the coproduct inclusion. The body is the standard Sigma.ι leg of the coproduct of copies of ℤ.
Claim. For open sets $U,V$ covering a space $X$ and $n\in\mathbb{N}$, if $t$ is a small singular $n$-simplex (image contained in $U$ or in $V$), there is a morphism $s_t:\mathbb{Z}\to C_n^{\mathrm{sm}}(U,V)$ in $\mathbf{Mod}_{\mathbb{Z}}$ placing a generator at the $t$-summand of the free module on small $n$-simplices.
background
This module builds the small singular chain complex relative to an open cover $X=U\cup V$, the classical input to the Mayer–Vietoris long exact sequence in singular homology. A singular $n$-simplex is small when its image lies entirely in $U$ or entirely in $V$; the subtype of such simplices is the index type of the small chain group.
The degree-$n$ small chain group is the free $\mathbb{Z}$-module on those small simplices, realized in the category of modules as the coproduct $\coprod_t \mathbb{Z}$ over the small-simplex index. The ordinary singular chain group is the analogous free module on all singular simplices. Generators of free modules-as-coproducts are the canonical coproduct inclusions of $\mathbb{Z}$.
Upstream, the small-chain group is already packaged as that coproduct; the present definition simply names its $t$-th inclusion leg.
proof idea
Pure definitional wrapper: apply the coproduct inclusion $\Sigma.\iota$ of the family of modules $\mathbb{Z}$ indexed by the small-simplex type, at the given index $t$. No further lemmas or tactics.
why it matters
Every map out of the small chain group is determined by where generators go, so this map is the universal handle used throughout the module. Downstream it feeds the small boundary (alternating sum of faces of a small simplex, still small), the inclusion of small chains into ordinary singular chains, the retraction of that inclusion, and the intertwining identities that make the small complex a subcomplex. Those identities are the algebraic backbone of the singular Mayer–Vietoris sequence for the cover $U\cup V$.
In the Recognition foundation stack this is pure classical singular homology scaffolding: it does not itself invoke the forcing chain (T0–T8), the $J$-cost, or $\phi$, but it supplies the chain-level language later used when recognition geometry is compared with singular data on covers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.