The weak topology of relative cell complexes

A relative cell complex in TopCat carries the final topology for its base map and its characteristic maps. Consequently, a subset is closed exactly when its preimage in the base and in every cell is closed (HomotopicalAlgebra.RelativeCellComplex.isClosed_iff), and a map out of the complex is continuous exactly when its composites with those maps are continuous (HomotopicalAlgebra.RelativeCellComplex.continuous_iff). No separation or embedding assumptions are required.

In particular, these criteria apply directly to TopCat.RelativeCWComplex: the characteristic maps have closed disks as their domains. This establishes the weak-topology part of the comparison with classical relative CW complexes; closure finiteness is a separate property. The same criteria for a single attachment are also provided here.

References

• A. Hatcher, Algebraic Topology, Appendix, Proposition A.2, for the weak topology of CW complexes.
• R. Fritsch and R. Piccinini, Cellular Structures in Topology, Cambridge University Press, 1990, for the categorical construction of cell complexes.

theorem HomotopicalAlgebra.AttachCells.isClosed_iff {α : Type t} {A B : α → TopCat} {g : (a : α) → A a ⟶ B a} {X Y : TopCat} {f : X ⟶ Y} (c : AttachCells g f) (S : Set ↑Y) : IsClosed S ↔ IsClosed (⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' S) ∧ ∀ (i : c.ι), IsClosed (⇑(CategoryTheory.ConcreteCategory.hom (c.cell i)) ⁻¹' S)

A subset of a space obtained by attaching cells is closed exactly when its preimages in the old space and in each attached cell are closed.

theorem HomotopicalAlgebra.AttachCells.continuous_iff {α : Type t} {A B : α → TopCat} {g : (a : α) → A a ⟶ B a} {X Y : TopCat} {f : X ⟶ Y} (c : AttachCells g f) {Z : Type v} [TopologicalSpace Z] (p : ↑Y → Z) : Continuous p ↔ Continuous (p ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)) ∧ ∀ (i : c.ι), Continuous (p ∘ ⇑(CategoryTheory.ConcreteCategory.hom (c.cell i)))

Continuity out of an attachment can be checked on the old space and every attached cell.

theorem HomotopicalAlgebra.RelativeCellComplex.isClosed_iff {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) (S : Set ↑Y) : IsClosed S ↔ IsClosed (⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' S) ∧ ∀ (γ : c.Cells), IsClosed (⇑(CategoryTheory.ConcreteCategory.hom γ.ι) ⁻¹' S)

A relative cell complex has the weak topology for its base and characteristic maps: a subset is closed exactly when its preimages in the base and in every cell are closed.

theorem HomotopicalAlgebra.RelativeCellComplex.continuous_iff {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) {Z : Type v} [TopologicalSpace Z] (p : ↑Y → Z) : Continuous p ↔ Continuous (p ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)) ∧ ∀ (γ : c.Cells), Continuous (p ∘ ⇑(CategoryTheory.ConcreteCategory.hom γ.ι))

A map out of a relative cell complex is continuous exactly when its composite with the base map and with every characteristic map is continuous. The target is arbitrary.