cPush
plain-language theorem explainer
Pushforward of a singular n-simplex on the complement of a set S in an ambient space W to a singular n-simplex of W, via the continuous inclusion of the complement subtype. Algebraic topologists proving arc-complement acyclicity (Hatcher 2B.1) use it to compare chains on open complements with ambient singular chains. The body is the degree-n component of the singular simplicial-set map induced by that inclusion.
Claim. Given a subset $S \subseteq W$ and a singular $n$-simplex $\sigma$ of the complement subtype $\{y \in W : y \notin S\}$, write $c\mathrm{Push}(\sigma)$ for the ambient singular $n$-simplex of $W$ obtained by post-composing $\sigma$ with the continuous inclusion $W \setminus S \hookrightarrow W$.
background
Singular homology indexes the degree-$n$ chain group of a space $X$ by the set of continuous maps from the standard $n$-simplex into $X$. In this development that index set is written $\mathrm{Idx}, X, n$. The ambient space is an object $W$ of $\mathbf{Top}$, and for each $S \subseteq W$ one forms the open complement as the subtype ${y : W \mid y \notin S}$.
The continuous inclusion of that subtype into $W$ is the morphism cVal S. Applying the singular simplicial-set functor sends this inclusion to a map of simplicial sets; its component in degree $n$ carries complement simplices to ambient simplices. The module builds chain-level comparison and lifting tools around that map, toward Hatcher's statement that arc complements in spheres are $H_1$-acyclic.
proof idea
One-line definitional wrapper. Form the singular simplicial-set map induced by the inclusion morphism of the complement into $W$, evaluate that natural transformation at the opposite of the standard simplex object $[n]$, and apply the resulting function to the given complement simplex. No further lemmas are invoked in the body.
why it matters
This is the ambient projection used throughout the arc-complement development. Downstream, range_cPush records that the geometric image of a pushed simplex still avoids $S$; cPush_cLift shows lift-then-push recovers the original ambient simplex; chainMap_cVal_unitOf identifies the chain-level unit with the unit of the push; and exists_chain_lift uses the push to state compact-support lifting between two complements. The parent theorem arcComplementsAcyclic (Hatcher 2B.1, arc case, formal) relies on these comparisons to prove every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement in every dimension $D$. In the Recognition foundation layer that vanishing supports higher linking and dimension-forcing arguments tied to the $D=3$ landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.