Subspace inclusions in TopCat

The canonical inclusions of subspaces are monomorphisms, and the inclusions of nested subspaces compose to an inclusion. These supply the monomorphism hypotheses for the subspace inclusions in the Mayer–Vietoris pushout square, and the functoriality of homology along nested subspaces.

instance TopCat.mono_ofHom_subtypeVal {X : TopCat} (S : Set ↑X) : CategoryTheory.Mono (ofHom (ContinuousMap.subtypeVal S))

The inclusion of a subspace is a monomorphism of topological spaces.

instance TopCat.mono_ofHom_inclusion {X : TopCat} {S T : Set ↑X} (h : S ⊆ T) : CategoryTheory.Mono (ofHom (ContinuousMap.inclusion h))

The inclusion of one subspace in another is a monomorphism of topological spaces.

@[simp]

theorem TopCat.ofHom_inclusion_comp_ofHom_inclusion {α : Type u} [TopologicalSpace α] {r s t : Set α} (hrs : r ⊆ s) (hst : s ⊆ t) : CategoryTheory.CategoryStruct.comp (ofHom (ContinuousMap.inclusion hrs)) (ofHom (ContinuousMap.inclusion hst)) = ofHom (ContinuousMap.inclusion ⋯)

Composing the inclusions r ⊆ s and s ⊆ t gives the inclusion r ⊆ t.

@[simp]

theorem TopCat.ofHom_inclusion_comp_ofHom_inclusion_assoc {α : Type u} [TopologicalSpace α] {r s t : Set α} (hrs : r ⊆ s) (hst : s ⊆ t) {Z : TopCat} (h : ↧↑t ⟶ Z) : CategoryTheory.CategoryStruct.comp (ofHom (ContinuousMap.inclusion hrs)) (CategoryTheory.CategoryStruct.comp (ofHom (ContinuousMap.inclusion hst)) h) = CategoryTheory.CategoryStruct.comp (ofHom (ContinuousMap.inclusion ⋯)) h

Composing the inclusions r ⊆ s and s ⊆ t gives the inclusion r ⊆ t.

theorem TopCat.commSq_ofHom_inter {X : TopCat} (U V : Set ↑X) : CategoryTheory.CommSq (ofHom (ContinuousMap.inclusion ⋯)) (ofHom (ContinuousMap.inclusion ⋯)) (ofHom (ContinuousMap.subtypeVal U)) (ofHom (ContinuousMap.subtypeVal V))

The square of inclusions of U ∩ V, U and V into X commutes.