Relative CW complexes are closed embeddings

Mathlib's categorical relative CW complex c : TopCat.RelativeCWComplex f, for a morphism f : X ⟶ Y of TopCat, presents Y as the colimit of a sequence of spaces c.F.obj n starting at X, each obtained from the previous one by attaching n-disks along their boundary spheres. This file proves that f is a closed embedding (TopCat.RelativeCWComplex.isClosedEmbedding), as are the maps c.F.obj m ⟶ c.F.obj n between the stages and the maps c.incl.app n : c.F.obj n ⟶ Y to the colimit. So X and every stage of the complex are closed subspaces of Y; this is the starting point for reading a classical CW structure on Y, relative to the range of f, off a categorical one.

The statements hold for any relative cell complex in TopCat whose basic cells are closed embeddings (HomotopicalAlgebra.RelativeCellComplex.isClosedEmbedding). Such a complex is a transfinite composition of pushouts of coproducts of basic cells, and closed embeddings are stable under all three operations (TauCeti.TopCat.isClosedEmbedding). For CW complexes the basic cells are the boundary inclusions ∂𝔻 n ⟶ 𝔻 n, which are closed embeddings because they are injective maps from a compact space to a Hausdorff one (TauCeti.TopCat.isClosedEmbedding_diskBoundaryInclusion).

References

• A. Hatcher, Algebraic Topology, Appendix, on the topology of cell complexes.
• R. Fritsch and R. Piccinini, Cellular Structures in Topology, Cambridge University Press, 1990, for the categorical definition.

theorem HomotopicalAlgebra.RelativeCellComplex.isClosedEmbedding_map {J : Type w'} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → TopCat} {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCellComplex basicCell f) (hc : ∀ (s : c.Cells), Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (basicCell s.j s.i))) {i j : J} (hij : i ≤ j) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (c.F.map (CategoryTheory.homOfLE hij)))

In a relative cell complex in TopCat whose basic cells are closed embeddings, the maps between the stages are closed embeddings.

theorem HomotopicalAlgebra.RelativeCellComplex.isClosedEmbedding_incl_app {J : Type w'} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → TopCat} {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCellComplex basicCell f) (hc : ∀ (s : c.Cells), Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (basicCell s.j s.i))) (j : J) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (c.incl.app j))

In a relative cell complex in TopCat whose basic cells are closed embeddings, the map from each stage to the complex is a closed embedding.

theorem HomotopicalAlgebra.RelativeCellComplex.isClosedEmbedding {J : Type w'} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → TopCat} {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCellComplex basicCell f) (hc : ∀ (s : c.Cells), Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (basicCell s.j s.i))) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)

A relative cell complex in TopCat whose basic cells are closed embeddings is a closed embedding.

theorem TopCat.RelativeCWComplex.isClosedEmbedding_map {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) {m n : ℕ} (hmn : m ≤ n) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (c.F.map (CategoryTheory.homOfLE hmn)))

In a relative CW complex, the maps between the stages are closed embeddings.

theorem TopCat.RelativeCWComplex.isClosedEmbedding_incl_app {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) (n : ℕ) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (c.incl.app n))

In a relative CW complex, the map from each stage to the complex is a closed embedding.

theorem TopCat.RelativeCWComplex.isClosedEmbedding {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)

A relative CW complex f : X ⟶ Y is a closed embedding.