cPush_cLift
plain-language theorem explainer
Pushing forward a lifted singular simplex recovers the original ambient simplex whenever the simplex misses a closed set T. Algebraic topologists working on relative singular chains of arc complements cite this as the left-inverse half of the lift/push adjunction on indices. The proof is a short injectivity argument through the standard-simplex equivalence and its naturality.
Claim. Let $W$ be the ambient space and $T \subseteq W$. For any singular $n$-simplex $s$ of $W$ whose image misses $T$, if one lifts $s$ into the complement subtype $\{y \in W : y \notin T\}$ and then pushes that lift back to $W$, the result equals $s$.
background
The module develops singular-chain acyclicity for complements of arcs in a fixed ambient space $W$. Singular $n$-simplices are indexed by $\mathrm{Idx},X,n$, the degree-$n$ objects of the singular simplicial set of a topological space $X$. The retyped equivalence $\mathrm{simplexEquiv}$ identifies each index with a continuous map from the standard simplex $\Delta^n$ into $X$, chosen so that domain normal forms do not block rewriting.
Two companion maps move simplices between $W$ and open complements. The push takes a simplex of the complement subtype ${y \notin S}$ and forgets the subtype, recovering an ambient simplex of $W$. The lift goes the other way: given an ambient simplex whose image entirely avoids $T$, it rebuilds a continuous map into the complement subtype. The hypothesis on the range of $\mathrm{simplexEquiv},W,n,s$ is exactly the geometric condition that makes the lift well-defined.
Naturality of $\mathrm{simplexEquiv}$ with respect to continuous maps (the lemma $\mathrm{simplexEquiv_map}$) says that pushing a simplex and then reading it as a continuous map is the same as composing the original map with the inclusion of the complement.
proof idea
Apply injectivity of $\mathrm{simplexEquiv},W,n$ so it is enough to check equality after translating both sides into continuous maps $\Delta^n \to W$. Unfold the definitions of push and lift: the left-hand side becomes the image under $\mathrm{simplexEquiv}$ of the simplicial-set pushforward of the lifted index. Naturality ($\mathrm{simplexEquiv_map}$) rewrites that as the composition of the inclusion of the complement with the lifted map. The lifted map was built as the subtype-valued version of the original continuous map, so applying the inclusion and then the inverse of $\mathrm{simplexEquiv}$ cancels by $\mathrm{Equiv.apply_symm_apply}$. Pointwise extensionality finishes with reflexivity.
why it matters
The identity is the left-inverse half of the index-level correspondence between ambient simplices missing $T$ and simplices of the complement. Downstream, $\mathrm{exists_chain_lift}$ uses it to promote a chain in the complement of $S$ whose geometric support also misses $T$ into a chain in the complement of $T$, with equal ambient pushforwards (compact-support lifting). That lifting step is part of the arc-complement acyclicity argument in the Foundation layer, which supplies vanishing of high-dimensional singular homology needed for the linking and forcing infrastructure. Without the recovery identity, the chain-level lift would only be defined up to an unidentified ambient simplex rather than matching the original support termwise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.