chainMap_cVal_unitOf
plain-language theorem explainer
The singular chain map induced by including the complement of S in the ambient space W sends the generator of a complement simplex s to the generator of its ambient image. Arc-complement and compact-support arguments cite this when equating complement chains with ambient pushforwards. The proof is a one-line specialization of the general unit naturality for chain maps of continuous maps.
Claim. Let $S \subseteq W$ and let $s$ be an $n$-simplex of the complement space $W \setminus S$. Write $i_S : W \setminus S \hookrightarrow W$ for the inclusion. Then the induced singular chain map satisfies $C_n(i_S)(\langle s \rangle) = \langle i_S \circ s \rangle$, i.e. the basis chain of $s$ is sent to the basis chain of the ambient simplex underlying $s$.
background
The module develops singular-chain tools for complements of arcs (and more general sets) inside an ambient space $W$, aimed at acyclicity statements used in the Recognition foundation layer.
Two local maps organize the geometry. The inclusion $cVal(S) : W \setminus S \to W$ is the continuous subtype projection. Its simplicial set pushforward on an index simplex $s$ of the complement is $cPush(s)$, "the ambient simplex underlying a simplex of a complement subtype." Basis chains are written $unitOf(\cdot)$: the free-abelian generator attached to a single simplex.
Upstream, SingularMayerVietoris supplies the general fact $chainMap_unitOf$: any continuous map of spaces induces a chain map that sends the unit of a simplex to the unit of its image simplex. The present lemma is that fact specialized to $cVal(S)$.
proof idea
One-line term proof: apply the general naturality lemma $chainMap_unitOf$ from SingularMayerVietoris to the continuous map $cVal(S)$ and the simplex $s$. No extra rewriting is needed; $cPush(s)$ is definitionally the image simplex under $TopCat.toSSet.map(cVal(S))$.
why it matters
This identity is the generator-level step inside $exists_chain_lift$ ("Compact-support lifting"): a chain of the complement of $S$ whose support avoids $T$ in the ambient space comes from a chain of the complement of $T$, up to common ambient pushforward. The lift is built by summing units of pushed simplices; equating $chainMap(cVal(S))(unitOf, s)$ with $unitOf(cPush, s)$ lets the ambient images match termwise.
In the broader foundation stack, arc-complement acyclicity feeds linking and vanishing arguments (via LinkingVanishingHighDim) that underwrite dimensional and topological constraints in the forcing chain. The lemma itself is pure singular-chain bookkeeping, not a physics claim, but without it the compact-support comparison between nested complements does not type-check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.