Normality of attaching spaces and of sequential colimits in TopCat

Spaces built by attaching along closed subspaces and then passing to a sequential colimit, such as the skeletal filtration of the realization of a simplicial space, stay normal and T1. This file proves the two steps.

• Attaching. In a pushout square

       g
    A ───> X
  m │      │ f
    v      v
    B ───> P
       g₂
  

  of TopCat in which m is a closed embedding, so that P is the space X ∪_g B obtained by attaching B to X along the closed subspace A, the space P is normal when X and B are (TauCeti.TopCat.normalSpace_of_isPushout) and T1 when they are (TauCeti.TopCat.t1Space_of_isPushout). The map f is then a closed embedding by TauCeti.TopCat.isClosedEmbedding_of_isPushout, so X is a closed subspace of P.
• Sequential colimits. If F : ℕ ⥤ TopCat has closed embeddings as transition maps and every F.obj n is normal, its colimit is normal (TauCeti.TopCat.normalSpace_of_isColimit). A directed colimit of T1 spaces along injective transition maps is T1 (TauCeti.TopCat.t1Space_of_isColimit).

Both normality proofs separate two disjoint closed sets by a continuous real function, built from Urysohn functions by the Tietze extension theorem. For attaching, a Urysohn function u on X separating the traces of the two sets is pulled back to A and extended to B, with values 0 and 1 on the traces there (ContinuousMap.exists_extension_eqOn_const). The two functions agree on A, so the sublevel and superlevel sets at 1 / 2 glue to disjoint open sets of P. For a sequential colimit the same extension step, applied stage by stage, gives compatible separating functions on all stages, and these descend to a separating function on the colimit.

References

• A. Hatcher, Algebraic Topology, Proposition A.3, that cell complexes are normal, by the same stagewise extension.
• R. Fritsch and R. Piccinini, Cellular Structures in Topology, Cambridge University Press, 1990, Chapter 1, for adjunction spaces.

theorem TauCeti.TopCat.normalSpace_of_isPushout {A B X P : TopCat} {g : A ⟶ X} {m : A ⟶ B} {f : X ⟶ P} {g₂ : B ⟶ P} (sq : CategoryTheory.IsPushout g m f g₂) (hm : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom m)) [NormalSpace ↑X] [NormalSpace ↑B] : NormalSpace ↑P

Attaching a normal space B to a normal space X along a closed subspace of B gives a normal space: in a pushout square in TopCat whose side m : A ⟶ B is a closed embedding, the corner P is normal.

theorem TauCeti.TopCat.t1Space_of_isPushout {A B X P : TopCat} {g : A ⟶ X} {m : A ⟶ B} {f : X ⟶ P} {g₂ : B ⟶ P} (sq : CategoryTheory.IsPushout g m f g₂) (hm : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom m)) [T1Space ↑X] [T1Space ↑B] : T1Space ↑P

Attaching a T1 space B to a T1 space X along a closed subspace of B gives a T1 space: in a pushout square in TopCat whose side m : A ⟶ B is a closed embedding, the corner P is T1.

theorem TauCeti.TopCat.t1Space_of_isColimit {J : Type w} [Preorder J] [IsDirectedOrder J] {F : CategoryTheory.Functor J TopCat} (hF : ∀ ⦃i j : J⦄ (hij : i ≤ j), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij)))) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) [∀ (j : J), T1Space ↑(F.obj j)] : T1Space ↑c.pt

A directed colimit of T1 spaces in TopCat along injective transition maps is T1.

theorem TauCeti.TopCat.normalSpace_of_isColimit {F : CategoryTheory.Functor ℕ TopCat} {c : CategoryTheory.Limits.Cocone F} (hF : ∀ (n : ℕ), Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯)))) (hc : CategoryTheory.Limits.IsColimit c) [∀ (n : ℕ), NormalSpace ↑(F.obj n)] : NormalSpace ↑c.pt

The colimit of a sequence of normal spaces in TopCat whose transition maps are closed embeddings is normal.