range_pushIdx
plain-language theorem explainer
A singular n-simplex of a subspace W, pushed into the ambient space X via the subspace inclusion, has geometric image still inside W. Algebraic topologists building Mayer–Vietoris for singular chains cite this when classifying which ambient simplices are “small.” The proof unfolds the push, applies naturality of the simplex-as-map equivalence, and reads off the second component of the subspace-valued map.
Claim. Let $W \subseteq X$ and let $\sigma$ be a singular $n$-simplex of the subspace topology on $W$. Write $\iota_\ast\sigma$ for the singular $n$-simplex of $X$ obtained by composing with the inclusion $\iota:W\hookrightarrow X$. Viewing $\iota_\ast\sigma$ as a continuous map $\Delta^n\to X$, one has $\operatorname{im}(\iota_\ast\sigma)\subseteq W$.
background
The module builds singular Mayer–Vietoris data for a cover of a space $X$ by open sets $U,V$. Singular $n$-simplices are the index type Idx: the $n$-simplices of the singular simplicial set of a TopCat object, equivalently continuous maps from the standard simplex $\Delta^n$ into the space.
The conversion between an index and that continuous map is simplexEquiv, a retyping of TopCat.toSSetObjEquiv so the domain is literally stdSimplex ℝ (Fin (n+1)). Its naturality lemma states that pushing an index along a continuous map $f$ corresponds to post-composing the geometric map with $f$.
pushIdx W a is the $X$-simplex underlying a singular simplex $a$ of the subspace $W$: apply the singular functor to the subspace inclusion $W\hookrightarrow X$. The geometric content of the present lemma is that this push does not enlarge the image beyond $W$.
proof idea
Term-style proof in four short steps. Unfold pushIdx to expose the singular-set map of the subspace inclusion. Rewrite with simplexEquiv_map (naturality of the index-to-map equivalence) and ContinuousMap.coe_comp, so the geometric map is inclusion composed with the original $W$-valued simplex. For a point in the range, pick a preimage $t\in\Delta^n$; the value is the second component of the pair produced by the $W$-simplex at $t$, which lies in $W$ by construction of the subspace topology.
why it matters
Feeds the small-simplex predicates used throughout the Mayer–Vietoris complex. Immediately, small_pushIdx_left and small_pushIdx_right conclude that any push of a $U$-simplex (resp. $V$-simplex) is small for the cover $(U,V)$, via a one-line Or.inl/Or.inr on this range inclusion.
Those facts support mv_middle_exact, the heart of Mayer–Vietoris exactness: a pair of chains on $U$ and $V$ whose images in the small complex cancel comes from a chain on $U\cap V$. In the Recognition foundation stack this is pure singular-homology scaffolding (not a T0–T8 forcing step), needed so later geometric and physical arguments can quote a fully formal MV sequence rather than an external black box.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.