genUnit_mem_smallSpan
plain-language theorem explainer
If a singular n-simplex is small relative to a pair of subsets (U, V), its generator chain lies in the integer span of all small generators. Algebraic topologists assembling the singular Mayer–Vietoris sequence cite this membership lemma. The argument is a one-line term proof via the universal property of submodule span.
Claim. Let $U,V\subseteq X$ and let $s$ be a singular $n$-simplex of $X$. If the image of $s$ lies entirely in $U$ or entirely in $V$, then the corresponding generator of the singular chain group $C_n(X)$ belongs to the $\mathbb{Z}$-span of all generators attached to small $n$-simplices.
background
This module builds the singular Mayer–Vietoris apparatus for a topological space $X$ covered by a pair of subsets $U,V$. Singular $n$-simplices are indexed by Idx X n; each contributes a free generator in the singular chain group $C_n(X)$ via the unit map that sends an index to its basis element.
A simplex is called small (relative to $U,V$) when its geometric image lies wholly in $U$ or wholly in $V$. The small-span submodule is the $\mathbb{Z}$-span inside $C_n(X)$ of exactly those generators whose simplices are small. Faces of small simplices remain small, so the small chains form a subcomplex once boundaries are in place.
The generator attached to a single simplex is the free unit of that index. Membership of that unit in the small span is the elementary seed for every later comparison between the free small-chain group and the ambient singular chains.
proof idea
One-line term proof. The small span is defined as Submodule.span ℤ of the set of generators of small simplices. Given a witness that $s$ is small, the triple $\langle s, hs, \mathrm{rfl}\rangle$ is an element of that generating set, so Submodule.subset_span places the generator inside the span.
why it matters
This is the atomic membership fact for the small-chain submodule. Downstream, sInc_mem_smallSpan lifts it by free induction to show that the inclusion of the free small-chain group lands in the small span, and toChain_one_mem_smallSpan uses it to place evaluations of affine chains (after pushforward by a continuous map) into the same span whenever every support piece is small.
Together those lemmas underwrite the comparison maps in the singular Mayer–Vietoris short complex. In the Recognition Science foundation stack this is pure scaffolding for homology of covers; it does not itself invoke the forcing chain (T0–T8), the J-cost, or the eight-tick octave, but it supplies the chain-level language those geometric arguments later sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.