sInc
plain-language theorem explainer
Degree-n inclusion of the small singular chain group (free on simplices small relative to an open cover U,V) into the ordinary singular chain group of X. Anyone assembling the Mayer–Vietoris exact sequence for singular homology cites it. Defined by coproduct descent: each small-simplex generator maps to the matching singular generator.
Claim. For each $n\in\mathbb{N}$, there is a morphism of free $\mathbb{Z}$-modules $sC_n(U,V)\to C_n(X)$ sending the generator attached to a small singular $n$-simplex $\sigma$ to the ordinary singular generator of $\sigma$ in $C_n(X)$.
background
The ambient setting is singular chain complexes on a space $X$ with an open cover by sets $U$ and $V$. The ordinary degree-$n$ singular chain group $C_n(X)$ is the free $\mathbb{Z}$-module on all continuous maps $\Delta^n\to X$, presented as a coproduct of copies of $\mathbb{Z}$.
The small chain group $sC_n(U,V)$ is the free $\mathbb{Z}$-module on those singular $n$-simplices whose image is contained in $U$ or in $V$ (indexed by SIdx). Its generators are the canonical coproduct inclusions into that free module. The ordinary generators of $C_n(X)$ are the corresponding coproduct inclusions for all simplices on $X$.
This module sits in the Foundation singular-homology stack (prism operators, pairs, subdivision) used to build a Mayer–Vietoris sequence in Lean.
proof idea
One-line definition by the universal property of the coproduct: Sigma.desc assembles a family of maps out of each summand of $sC_n(U,V)$. On the summand indexed by a small simplex $t$, the map is the ordinary singular generator of the underlying simplex $t.1$. No further lemmas are invoked at the definition site; naturality and injectivity are proved downstream.
why it matters
This inclusion is the structural map that makes small chains a subcomplex of singular chains. Downstream it is used to prove: the inclusion is a section of a retraction (sInc_comp_sRet), hence mono and elementwise injective; it intertwines small and ordinary boundaries (sBnd_comp_sInc); the small boundary squares to zero by cancelling the mono (sBnd_comp_sBnd); and every chain in the small span is hit (exists_sInc_eq).
In the Recognition Foundation layer this is pure algebraic-topology scaffolding for Mayer–Vietoris, not a physics forcing step (T0–T8). It supplies the chain-level mono needed before homology long exact sequences and cover arguments can be stated formally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.