range_cPush
plain-language theorem explainer
A singular n-simplex of the complement of S in W, pushed into ambient W along the inclusion, has image entirely outside S. Used when lifting complement simplices into ambient singular chains for arc-complement acyclicity (Hatcher 2B.1). Proof unfolds the push, applies naturality of the simplex-to-map equivalence, and reads off the subtype witness.
Claim. Let $S \subseteq W$ and let $\sigma$ be a singular $n$-simplex of the complement space $W \setminus S$. Write $\iota_*\sigma$ for the ambient singular $n$-simplex of $W$ obtained by composing with the inclusion $\iota: W\setminus S \hookrightarrow W$. Then every point of the image of the continuous map representing $\iota_*\sigma$ lies outside $S$.
background
The module develops singular-homology tools for complements of arcs in spheres, aiming at Hatcher's arc-complement acyclicity. Singular $n$-simplices of a space $X$ are indexed by Idx X n, the $n$-simplices of the singular simplicial set of $X$. The retyped equivalence simplexEquiv identifies each such index with a continuous map from the standard geometric $n$-simplex into $X$.
Given $S \subseteq W$, a simplex of the complement subtype ${y \in W : y \notin S}$ is pushed to an ambient simplex of $W$ by cPush: apply the singular-set functor to the continuous inclusion of the complement. Upstream naturality (simplexEquiv_map) says this push corresponds exactly to post-composing the continuous map with that inclusion.
The local goal is bookkeeping: ambient images of complement simplices must avoid $S$, so they remain legitimate chains on the open complement when one compares homology of $W \setminus S$ with ambient singular chains.
proof idea
Short tactic proof. Introduce a point $x$ in the image of the ambient continuous map of cPush s. Unfold cPush and rewrite by simplexEquiv_map together with ContinuousMap.coe_comp, so $x$ is the value of the inclusion composed with the original complement simplex map at some parameter $t$. Transport along that equality; the second component of the subtype-valued point (simplexEquiv (complement) n s) t is precisely the witness $x \notin S$.
why it matters
Feeds the sole downstream consumer arcComplementsAcyclic: every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement, in every dimension $D$ (Hatcher 2B.1, arc case, formal). That theorem is the arc half of the linking-vanishing package imported from LinkingVanishingHighDim, which underwrites high-dimensional topological constraints in the Recognition foundation (complement acyclicity used when comparing linking and homology support for the forcing chain's dimensional claims).
Without image-avoidance of pushed simplices, one cannot safely identify cycles supported on the complement with ambient chains missing $S$. The lemma is pure singular-set bookkeeping, but it is the hinge between subtype simplices and ambient range statements used in the contradiction argument of arcComplementsAcyclic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.