cInc
plain-language theorem explainer
If one subset of a space sits inside another, the complement of the larger set includes continuously into the complement of the smaller. Algebraic topologists running the arc-complement acyclicity argument (Hatcher 2B.1 style) use this as the basic morphism of complements. The body is the subtype inclusion packaged as a TopCat arrow, with continuity from the ambient subtype projection.
Claim. Let $W$ be a topological space and $S \subseteq T \subseteq W$. There is a continuous map $W \setminus T \to W \setminus S$ given by the identity on underlying points (the inclusion of the smaller complement into the larger one).
background
The ambient setting is the module on arc-complement acyclicity: every topological embedding of the unit interval into the $D$-sphere has $H_1$-acyclic complement. Complements are handled as subtype spaces in TopCat, so morphisms between them must be continuous maps of those subtypes.
When $S \subseteq T$, set-theoretically $W \setminus T \subseteq W \setminus S$. The present definition turns that inclusion into a morphism of topological spaces. Downstream constructions push singular chains along such morphisms (e.g. the reference 1-cycle into the complement of a subsegment of an arc).
Related companion maps include the valuation of a complement into the ambient space and the functoriality lemmas that say successive inclusions compose and that double inclusion along mutual containment is the identity.
proof idea
Definition, not a proof. The arrow is TopCat.ofHom applied to the subtype map $y \mapsto y$, with the membership witness rewritten by the subset hypothesis: if $y \notin T$ and $x \in S \subseteq T$, then $y \notin S$. Continuity is Continuous.subtype_mk continuous_subtype_val, i.e. the map is continuous because the underlying map to $W$ is the continuous subtype projection.
why it matters
This is the elementary geometric arrow that the whole arc-complement package rides on. It is applied in the pushforward that builds the segment cycle in the complement of an arc image, in the bisection/Mayer-Vietoris step that compares complements of two halves of a closed set, and in the composition and identity lemmas that make the inclusion system a functor on the poset of subsets.
The parent target is arc-complement acyclicity in every dimension $D$ (Hatcher 2B.1, arc case): every embedded interval in $S^D$ has $H_1$-acyclic complement. That statement is the arc case of linking-vanishing in high dimensions, which sits in the Foundation layer supporting the forced spatial dimension $D = 3$ (forcing chain T8) and the topological side of the Recognition composition setup. Without a clean complement-inclusion morphism, the chain maps that move cycles under bisection do not typecheck.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.