pushIdx
plain-language theorem explainer
Push-forward of a singular n-simplex from a subspace W ⊆ X to the ambient space X, via the continuous inclusion. Algebraic topologists building Mayer–Vietoris for singular chains cite it as the simplex-level map underlying the chain inclusions. The body is a one-line application of the singular simplicial set functor to the subspace inclusion.
Claim. Given a topological space $X$, a subspace $W \subseteq X$, and a singular $n$-simplex $a$ of $W$, write $\mathrm{push}(W,a)$ for the underlying singular $n$-simplex of $X$ obtained by composing $a$ with the continuous inclusion $W \hookrightarrow X$.
background
Singular $n$-simplices of a space $Y$ are the points of the singular simplicial set at degree $n$: continuous maps $\Delta^n \to Y$. In this development they are abbreviated as the index type of the free abelian chain group $C_n(Y;\mathbb{Z})$.
The module builds Mayer–Vietoris for singular homology of a cover $X = U \cup V$. Chains that are small with respect to ${U,V}$ are generated by simplices whose image lies in $U$ or in $V$. Comparing those generators to ordinary singular simplices of $X$ requires a canonical way to view a simplex of a subspace as a simplex of the ambient space.
That comparison is induced by the continuous inclusion of a subspace $S \subseteq X$ as a morphism in $\mathbf{Top}$, which the singular functor $X \mapsto \mathrm{Sing}(X)$ sends to a map of simplicial sets, and hence to a map on $n$-simplices.
proof idea
One-line definition: apply the singular simplicial-set functor $\mathrm{TopCat.toSSet}$ to the subspace inclusion $\mathrm{subInc},X,W : \mathrm{TopCat.of},W \to X$, then evaluate the resulting natural transformation at the opposite simplex category object $\mathrm{op},[n]$, and feed in the given simplex $a$. No further rewriting is needed.
why it matters
This is the simplex-level generator of all subspace-to-ambient comparisons in the Mayer–Vietoris apparatus of the module. Downstream lemmas record that the push is injective, that it inverts the lift of a simplex already supported in $W$, and that it intertwines the two routes from $U \cap V$ through $U$ or through $V$. Those identities feed the middle exactness statement: a cancelling pair of chains on $U$ and $V$ comes from a chain on the intersection.
In the broader Recognition foundation stack, singular Mayer–Vietoris is scaffolding for homology of recognition complexes and covers, not a direct T0–T8 forcing step. It sits under the algebraic topology layer that later supports discrete octave and dimension arguments rather than replacing them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.