pushIdx_subIncl
plain-language theorem explainer
Nested subspace inclusions commute with pushing singular simplices out to the ambient space X. Anyone assembling Mayer–Vietoris chain maps cites this when comparing the two routes from U∩V through U or V. The proof is a short functoriality rewrite: map composition plus the identity that the composite of nested inclusions equals the direct inclusion.
Claim. Let $W \subseteq W' \subseteq X$ be nested subspaces and let $\sigma$ be a singular $n$-simplex of $W$. Pushing $\sigma$ forward along $W \hookrightarrow W'$ and then along $W' \hookrightarrow X$ yields the same singular $n$-simplex of $X$ as pushing $\sigma$ directly along $W \hookrightarrow X$.
background
In this module one works with singular simplices of a space $X$ (and of its subspaces) as the index sets of free $\mathbb{Z}$-chain groups. The type $\mathrm{Idx}(Y,n)$ is the set of singular $n$-simplices of a space $Y$, i.e. the value of the singular simplicial set functor at $\Delta^n$.
For a subspace $W \subseteq X$, $\mathrm{pushIdx},W$ sends a simplex of $W$ to the underlying simplex of $X$ by applying the singular-set functor to the subspace inclusion $W \hookrightarrow X$. Nested inclusions $W \subseteq W'$ are packaged as $\mathrm{TopCat}$ morphisms $\mathrm{subIncl}$; composing with the ambient inclusion of $W'$ recovers the ambient inclusion of $W$ (lemma $\mathrm{subIncl_comp_subInc}$).
The local setting is the singular Mayer–Vietoris apparatus: one needs naturality of these push maps under the standard inclusions of $U \cap V$ into $U$ and into $V$.
proof idea
Unpack the left-hand side via the definition of $\mathrm{pushIdx}$. Functoriality of $\mathrm{TopCat.toSSet.map}$ turns the composite morphism $\mathrm{subIncl},h \gg \mathrm{subInc},X,W'$ into the composite of the two mapped simplicial-set morphisms, so the intermediate simplex in $W'$ can be rewritten as the image under the composite inclusion. The identity $\mathrm{subIncl},h \gg \mathrm{subInc},X,W' = \mathrm{subInc},X,W$ then collapses the composite to the direct ambient inclusion of $W$, which is exactly $\mathrm{pushIdx},W,a$. Two definitional unfolds of $\mathrm{pushIdx}$ bookend the rewrite.
why it matters
This is the naturality lemma that lets Mayer–Vietoris inclusions act cleanly on generating simplices. Downstream it is applied verbatim as $\mathrm{pushIdx_mvInclU}$ and $\mathrm{pushIdx_mvInclV}$: the two routes $C_n(U \cap V) \to C_n^{U,V}$ through $U$ and through $V$ agree on generators precisely because intersection inclusions are special cases of nested $\mathrm{subIncl}$. Without that agreement the subsequent comparison of the two legs of the MV chain map would not be well-defined on the free generators.
In the broader Recognition foundation stack this sits in the singular-homology toolkit (prisms, pairs, subdivision) that underwrites topological forcing arguments; it is pure algebraic topology scaffolding rather than a T0–T8 landmark, but it is required infrastructure for any homology-level identity used later in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.