small_pushSimplex
plain-language theorem explainer
Pushing a small singular simplex along an affine vertex map yields another small simplex relative to the same open cover. Algebraic topologists cite this when showing that barycentric subdivision stays inside the small-span submodule for singular Mayer–Vietoris. The argument is a one-step range inclusion plus a case split on the two sides of the cover.
Claim. Let $U,V\subseteq X$ and let $s$ be a singular $n$-simplex of $X$ whose image lies in $U$ or in $V$. For any map $w:\mathrm{Fin}(m+1)\to\Delta^n$ of vertices, the singular $m$-simplex obtained by precomposing $s$ with the affine map determined by $w$ again has image contained in $U$ or in $V$.
background
In the singular Mayer–Vietoris setup one works with the pair of subsets $U,V\subseteq X$ and the free $\mathbb{Z}$-modules on singular simplices. A singular $n$-simplex $s$ (an element of the index type $\mathrm{Idx},X,n$) is called small relative to $(U,V)$ when the image of its continuous representative lies entirely in $U$ or entirely in $V$.
The push operation takes a continuous simplex $\sigma:\Delta^n\to X$ and a vertex tuple $w$ in $\Delta^n$, and returns the $m$-simplex obtained by precomposing $\sigma$ with the affine map of $w$. Equivalently, on indices, one transports via the standard equivalence between indices and continuous maps on the standard simplex.
Faces of small simplices are already known to be small. The present lemma extends that inheritance from face operators to arbitrary affine pushes, which is exactly what barycentric subdivision and the prism homotopy apply to generators.
proof idea
First establish that the continuous representative of the pushed simplex factors through the representative of $s$, so its range sits inside the range of $s$. This uses the identity relating the simplex equivalence to push, together with the elementary fact that the range of a composite is contained in the range of the outer map.
Case-split on the disjunction defining smallness of $s$. In each branch, compose the new range inclusion with the given inclusion into $U$ or into $V$. Both branches close by transitivity of $\subseteq$.
why it matters
The lemma is the generator-level step behind two span-preservation results in the same module: the singular subdivision operator maps the small span into itself, and the subdivision homotopy maps the small span into the small span one degree higher. Those facts let one run the usual subdivision argument inside the subcomplex of small chains, which is the classical route to the Mayer–Vietoris long exact sequence for singular homology.
In the Recognition Science foundation stack this sits in the singular-homology toolkit used to control topological invariants of recognition spaces (covers, octaves, and the discrete evolution geometry). It does not itself invoke the forcing chain T0–T8 or the J-cost; it is pure singular-set scaffolding that those later geometric arguments rely on when they need a working Mayer–Vietoris sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.