subIncl_comp_subInc
plain-language theorem explainer
Nested subspace inclusions compose: if W ⊆ W' ⊆ X, the map W → W' followed by W' → X equals the direct inclusion W → X in TopCat. Cited when simplifying double inclusions before singular-set or chain-level pushforwards. Proof is pointwise extensionality plus reflexivity of the underlying set maps.
Claim. Let $X$ be a topological space and $W \subseteq W' \subseteq X$ subspaces. The composition of the continuous inclusion $W \hookrightarrow W'$ with the continuous inclusion $W' \hookrightarrow X$ equals the continuous inclusion $W \hookrightarrow X$.
background
The module builds singular Mayer–Vietoris data over TopCat, using subspace inclusions as the basic morphisms that induce maps of singular simplicial sets and then of chain complexes.
subIncl h is the TopCat morphism TopCat.of W ⟶ TopCat.of W' given by set-theoretic inclusion when W ⊆ W'. Independently, SingularPair.subInc X S is the subspace inclusion TopCat.of S ⟶ X (subtype valuation). Both are continuous by construction.
The present lemma is the elementary compatibility of these two constructions: nesting a relative inclusion under an absolute one recovers the absolute inclusion of the smaller set.
proof idea
Term/tactic hybrid: apply morphism extensionality (ext x) so both sides are compared as functions on points of W. Each side sends x to its image in X via the subtype valuation, so the equality is definitional (rfl). No homology or simplicial identities are used.
why it matters
Feeds pushIdx_subIncl, which equates index pushforwards along subIncl h with the direct push along the smaller subspace. That identity is needed so singular generators supported on nested opens behave coherently when assembling the Mayer–Vietoris short complex from singular pairs and subdivisions.
In the Recognition foundation stack this is pure topological bookkeeping: it keeps the singular-set functoriality of subspace inclusions strict before any cost, forcing-chain, or ladder structure appears. It does not itself touch T0–T8, RCL, or constants; it only stabilizes the geometric input those layers later consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.