exists_chain_lift
plain-language theorem explainer
Compact-support lifting for singular chains on open complements: a chain on W\\S whose ambient geometric support avoids T lifts to a chain on W\\T with identical pushforward into W. Cited by anyone chasing arc-complement H₁-acyclicity (Hatcher 2B.1 style) in this foundation layer. Proof rebuilds the chain termwise from lifted basis simplices and matches pushforwards by linearity of chainMap.
Claim. Let $S,T\subseteq W$ and let $c$ be a singular $n$-chain on the complement $W\\S$. Suppose every ambient simplex in the support of $c$ has image disjoint from $T$. Then there exists a singular $n$-chain $c'$ on $W\\T$ such that the two chains have the same image under the chain maps induced by the inclusions $W\\S\hookrightarrow W$ and $W\\T\hookrightarrow W$.
background
The module develops singular-chain tools for complements of subsets of an ambient space $W$, aimed at arc-complement acyclicity. Complements are realized as subtypes ${y\in W: y\notin S}$; the continuous inclusion into $W$ is written as the morphism $cVal(S)$. Pushing a simplex of the complement forward along that inclusion yields an ambient simplex $cPush(s)$. Conversely, if an ambient simplex has image disjoint from $T$, $cLift$ rebuilds it as a simplex of the complement of $T$, and $cPush\circ cLift$ is the identity on such simplices.
Chains live in the free abelian groups $C_n$ on those simplices. The support of a chain is the finite set of basis indices with nonzero coefficient; the reconstruction identity writes any chain as the corresponding finite sum of coefficient times unit basis chains. The companion lemma $chainMap\circ cVal$ on a unit basis chain equals the unit ambient chain of its $cPush$.
Local setting is the Complements section of ArcComplementAcyclic, feeding the later Mayer–Vietoris bisection step and the global arc-complement theorem.
proof idea
Construct the lift explicitly: sum, over the attached support of $c$, each coefficient times the unit chain of $cLift(T,cPush(s))$ (the hypothesis supplies the avoidance proof needed by $cLift$).
For each term, $mapSmul$, $chainMap_cVal_unitOf$, and $cPush_cLift$ collapse the $T$-side pushforward back to the ambient unit of $cPush(s)$. Summing with $map_sum$ and $Finset.sum_congr$ therefore yields the ambient sum of coefficient times unit $cPush$.
On the other side, rewrite $c$ via the support reconstruction identity, push termwise with $map_sum$ and $chainMap_cVal_unitOf$, and obtain the same ambient sum. $Finset.sum_attach$ identifies the attached and unattached sums, closing the equality.
why it matters
This is the compact-support bookkeeping step that lets chains migrate between nested or related complements without changing their ambient class. The sole direct consumer is $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 acyclicity is the geometric engine behind linking-vanishing statements imported from LinkingVanishingHighDim, which sit in the Foundation layer that underwrites higher Recognition forcing (spatial dimension $D=3$, eight-tick structure, and the topological side of the Clifford bridge). Without termwise lifts that preserve ambient pushforwards, the Mayer–Vietoris bisection argument later in the module cannot move cycles between $U$, $V$, and $U\cap V$ while keeping supports under control.
No open scaffold remains here: the lemma is fully proved and only packages already-established simplex lift/push identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.