cVal
plain-language theorem explainer
Continuous inclusion of the complement of a subset S of the ambient space W into W itself. Downstream chain-level lemmas (pushforwards, lifts, injectivity) cite it as the basic TopCat arrow from a complement subtype. The definition is the morphism induced by Subtype.val with its standard continuity.
Claim. For any subset $S \subseteq W$, write $cVal(S)$ for the continuous inclusion $\{ y \in W : y \notin S \} \hookrightarrow W$ of the complement subtype into the ambient space.
background
The module develops singular-homology facts about complements of arcs in spheres, aiming at Hatcher's arc-complement acyclicity (every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement). Working objects are TopCat spaces and their singular chain groups; subsets of an ambient space $W$ appear as forbidden loci whose complements carry the chains of interest.
Given $S \subseteq W$, the type ${ y : W \mid y \notin S }$ is the complement subtype. Its forgetful map to $W$ is continuous, so it determines a morphism in TopCat. That morphism is the bridge from chains written on the complement to chains written on $W$.
Sibling constructions (complement-to-complement inclusions when $S \subseteq T$, ambient push of simplices, chain maps) all compose with or factor through this inclusion.
proof idea
One-line definition: package Subtype.val together with continuous_subtype_val as a TopCat.ofHom. No further lemmas are invoked; the continuity of the subtype projection is library fact.
why it matters
This is the structural arrow that lets the module move data off complement subtypes and into $W$. It is used by cPush (ambient simplex underlying a complement simplex), by chainMap_cVal_unitOf and exists_chain_lift (compact-support lifting of chains between nested complements), by cInc_comp_cVal (naturality under enlarging the removed set), and by cVal_injective.
Those pieces feed the main theorem 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). In the Recognition foundation stack this is topological scaffolding for linking and vanishing statements that sit upstream of dimension and octave constraints (T7–T8), not a physics claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.