subInc_injective

In the singular-pair setup one treats a subspace $S \subseteq X$ as an object of TopCat via the subtype topology, and the continuous inclusion $S \hookrightarrow X$ as a morphism whose underlying map is subtype projection. That morphism is the structural input to the relative singular chain complex $C_(X,S)$ and to the degreewise short exact sequence $0 \to C_(S) \to C_(X) \to C_(X,S) \to 0$.

The local module builds pair data and the associated long exact sequence of homology from a general monomorphism of spaces. The inclusion of a set-theoretic subspace is the canonical special case: once its underlying map is known to be injective, every LES lemma for pairs applies with that inclusion as the monomorphism.

Upstream, the inclusion morphism itself is defined as the TopCat hom with continuous subtype valuation; injectivity is the only missing point-set fact before the pair SES can be instantiated.

Term-mode one-liner. Given two points of the subtype with equal images under the inclusion, apply Subtype.ext to recover equality in $S$. No topology or chain-level reasoning is used; only the definition of the underlying function of the inclusion morphism.

This is the monomorphism hypothesis that discharges the pair short exact sequence: the relative SES $0 \to C_(S) \to C_(X) \to C_*(X,S) \to 0$ is obtained by feeding the inclusion and this injectivity lemma into the general pair-SES constructor. Downstream, Mayer–Vietoris uses the same fact three ways: injectivity of the push-forward on singular simplices of a subspace, and injectivity of the two summand inclusions into the union complex. Without it, the relative and MV long exact sequences do not start. In the Recognition foundation stack this is pure scaffolding for singular homology of pairs, not a physics forcing step (T0–T8), but it is required wherever relative or excised homology appears later.