sInc_sUnit
plain-language theorem explainer
The inclusion of small singular chains sends the free generator of a small n-simplex to the ordinary free generator of that same simplex in the full chain group. Anyone building Mayer–Vietoris or excision for singular homology with a two-set cover cites this identification. The proof is a short term rewrite: evaluate the coproduct inclusion via the unit map, then apply the already-proved generator compatibility.
Claim. Let $U,V\subseteq X$ and let $t$ index a degree-$n$ singular simplex that is small relative to the cover $\{U,V\}$. Writing $s$ for the underlying simplex of $t$, the degree-$n$ inclusion of small chains sends the free $\mathbb{Z}$-generator of $t$ to the free $\mathbb{Z}$-generator of $s$ in the ordinary singular chain group of $X$.
background
The module works in singular chain complexes over $\mathbb{Z}$, with a two-set open cover ${U,V}$ of a space $X$. A singular $n$-simplex is called small when its image lies in $U$ or in $V$. The index type of such small simplices is the subtype of ordinary simplex indices satisfying that support condition; the small chain group is the free $\mathbb{Z}$-module (coproduct of copies of $\mathbb{Z}$) on that index type.
The inclusion morphism from the small chain group into the ordinary singular chain group of $X$ is induced by forgetting smallness. Free generators are the images of the unit $1\in\mathbb{Z}$ under the coproduct inclusions. An upstream evaluation lemma records that any morphism out of a free coproduct, applied to a unit generator, equals the evaluation of the corresponding component map at $1$. A sibling lemma already identifies the composite of the small-index coproduct inclusion with the small-chain inclusion with the ordinary generator map for the underlying simplex.
proof idea
Unfold the small unit as the coproduct unit at index $t$. Apply the evaluation lemma for units under a morphism out of a free coproduct: the inclusion applied to that unit equals the evaluation-at-$1$ of the composite of the $t$-th coproduct inclusion with the small-chain inclusion. That composite is identified, by the sibling generator-compatibility lemma, with the ordinary generator map for the underlying simplex. The two sides therefore agree by definition of the ordinary free generator.
why it matters
This is the generator-level bookkeeping that makes the small-chain inclusion behave like a literal subspace inclusion on basis elements. Downstream, the membership lemma that the inclusion lands in the small span proceeds by free induction on small chains and uses this identity on units; the existence lemma that every chain in the small span is the image of some small chain likewise quotes it on generators of the span. Together those two facts open the standard Mayer–Vietoris exact sequence for singular homology relative to a two-set cover, which is the algebraic engine behind excision and the dimension-forcing arguments in the foundation layer (eight-tick octave, $D=3$). The lemma itself is pure chain-level algebra; it does not yet encode the Recognition Composition Law or the $J$-cost uniqueness step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.