cLift
plain-language theorem explainer
Lifts a singular n-simplex of the ambient space W into the complement subtype of a set T, whenever the simplex image misses T. Used by anyone moving ambient singular chains into open complements in the arc-complement acyclicity argument. Construction is pure retyping: invert the simplex equivalence on the continuous map that lands in the subtype.
Claim. Let $T \subseteq W$ and let $s$ be a singular $n$-simplex of $W$ whose image misses $T$. Then $s$ determines a singular $n$-simplex of the complement space $\{ y \in W : y \notin T \}$, obtained by viewing the continuous map of $s$ as landing in that subtype.
background
The ambient object is a topological space $W$ (as a TopCat). Singular $n$-simplices of a space $X$ are the index set of the degree-$n$ singular chain group: continuous maps from the standard simplex $\Delta^n$ into $X$. The retyped equivalence simplexEquiv identifies that index set with $C(\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(n+1)), X)$, so one can build simplices by writing continuous maps and then transporting back.
The module works with open complements of subsets of $W$, written as subtype spaces ${ y : W \mid y \notin T }$. Homology of those complements is the setting for arc-complement acyclicity: one needs to move simplices and chains that avoid a bad set $T$ into the actual complement space, not merely into ambient chains supported off $T$.
Upstream, the only nontrivial ingredient is that equivalence between indices and continuous maps, plus the fact that continuous maps into $W$ that miss $T$ factor continuously through the subtype.
proof idea
One-line construction via the inverse of the simplex equivalence on the complement. Form the continuous map $\Delta^n \to {y \in W : y \notin T}$ by sending $t$ to the pair $(\sigma(t), h)$, where $\sigma$ is the continuous map of the ambient simplex $s$ and $h$ is the avoidance hypothesis on the image of $\sigma$. Continuity of the subtype map is map_continuous of $\sigma$ plus subtype_mk. Apply (simplexEquiv (complement) n).symm to that continuous map to obtain an index in the complement.
why it matters
This is the simplex-level building block for moving data into open complements inside the foundation arc-complement package. Immediately downstream, cPush_cLift records the round-trip: pushing the lifted simplex back to the ambient space recovers $s$ (injectivity of simplexEquiv). That identity is what lets exists_chain_lift promote a compactly supported chain in a larger complement into a chain of a smaller complement with the same ambient pushforward.
In the broader Recognition foundation, arc-complement acyclicity is part of the topological scaffolding that supports vanishing and linking statements in high dimension (the module imports linking-vanishing material). The lift itself is pure singular-set bookkeeping; the physical content sits in the parent acyclicity and linking theorems that consume these chain lifts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.