cInc_cInc_id
plain-language theorem explainer
Mutual containment of subsets forces the composite of the two complement-inclusion maps to be the identity on the smaller complement in TopCat. Arc-complement and linking arguments cite it to cancel paired inclusions when sets coincide. The proof is pure pointwise extensionality plus reflexivity.
Claim. Let $S,T\subseteq W$. If $S\subseteq T$ and $T\subseteq S$, then the composite of the continuous complement inclusions (complement of $T$ into complement of $S$, then back) equals the identity morphism on $\mathrm{Top}(\{y\in W: y\notin T\})$.
background
The ambient module formalizes arc-complement acyclicity: every topological embedding of the unit interval into the $D$-sphere has $H_1$-acyclic complement (Hatcher 2B.1, arc case). Complements of nested subsets of the ambient space $W$ are related by continuous inclusions of subtypes.
The map cInc sends the complement of a larger set into the complement of a smaller one: given $S\subseteq T$, it is the TopCat morphism ${y\notin T}\to{y\notin S}$ induced by the underlying inclusion of points, with continuity from the subtype topology. When the two sets are equal by mutual inclusion, the two directions compose on either side.
This sits in the foundation layer that supports linking-vanishing statements used later in the dimensional forcing chain.
proof idea
Term-mode proof by category morphism extensionality: after ext x, both sides act on a point of the complement subtype by the same underlying point of $W$, so rfl closes. No continuity or set-theoretic side conditions are re-proved; they are already packaged in the definition of the complement inclusion.
why it matters
Feeds the parent theorem arcComplementsAcyclic, which states that every embedded arc in $S^D$ has $H_1$-acyclic complement in every dimension $D$. That result is the formal Hatcher 2B.1 arc case and is part of the linking-vanishing infrastructure imported from LinkingVanishingHighDim.
In the Recognition framework this is scaffolding for high-dimensional topology used around the forcing chain (notably the $D=3$ spatial-dimension step T8 and related sphere/complement arguments). The lemma itself is purely categorical bookkeeping: without identity cancellation of mutual complement inclusions, naturality and iso arguments on complements stall.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.