cInc_comp
plain-language theorem explainer
Complement inclusions compose: if S ⊆ T ⊆ R in the ambient space W, the continuous map W\\R → W\\T followed by W\\T → W\\S equals the direct inclusion W\\R → W\\S. Anyone building chain maps or restrictions on arc-complement subtypes cites this. The proof is pointwise extensionality; both sides act as the identity on the underlying point.
Claim. Let $S,T,R \subseteq W$ with $T \subseteq R$ and $S \subseteq T$. Write $cInc$ for the continuous inclusion of complements induced by a subset relation (so $S \subseteq T$ gives $W \setminus T \hookrightarrow W \setminus S$). Then $cInc(T \subseteq R) \circ cInc(S \subseteq T) = cInc(S \subseteq R)$.
background
The ambient object is a topological space $W$ (as a TopCat object). For nested subsets $S \subseteq T \subseteq W$, the complement of the larger set sits inside the complement of the smaller one: $W \setminus T \subseteq W \setminus S$. The definition cInc packages that set-theoretic inclusion as a morphism in TopCat between the corresponding subtype spaces, with continuity coming from the subtype topology.
This module develops arc-complement acyclicity: homology of complements of arcs (and related segments) in $W$. Complement inclusions are the structural maps that let one compare, restrict, and push chain-level data when the removed set grows or shrinks. The composition law is the elementary functoriality step for those maps under a chain of three nested subsets.
proof idea
Both sides are morphisms $W \setminus R \to W \setminus S$ in TopCat. Apply ext on the underlying point of the subtype; each composite (and the direct inclusion) is defined by sending $\langle y, y \notin R \rangle$ to $\langle y, \ldots \rangle$ with the same ambient point $y$. The membership proofs differ only by Subset.trans, so rfl closes the equality of the underlying functions and thus of the morphisms.
why it matters
This is the associativity/functoriality lemma for complement inclusions used when restricting segment chains. Downstream, zSeg_restrict rewrites a chain-map composite via chainMap_chainMap and this lemma to show that pushing $zSeg$ along $cInc$ for a smaller parameter interval recovers the segment chain on that subinterval: restriction of the pushforward equals the segment on the subsegment.
In the Recognition foundation stack, arc-complement acyclicity supports vanishing and linking arguments in high dimension (the module imports LinkingVanishingHighDim). Clean composition of cInc keeps those chain-level identities purely formal rather than ad hoc on points. It does not itself touch T5–T8 or the RCL; it is infrastructure for the topological side of the forcing and linking story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.