Closure finiteness for categorical relative CW complexes

The boundary of each cell of a categorical relative CW complex is contained in the base together with finitely many closed cells of strictly smaller dimension. No separation condition on the base is needed. This gives the closure-finiteness condition used when reading a classical relative CW structure from the categorical cell attachments.

We first show that a compact subset of a finite stage is covered by the base and finitely many closed cells. The argument selects one point in each open cell it meets: at a single attachment, every subset of the selected points is closed, since its preimage in any attached disk has at most one point. The resulting compact discrete set is finite.

References

• A. Hatcher, Algebraic Topology, Appendix, Proposition A.1.
• R. Fritsch and R. Piccinini, Cellular Structures in Topology, Cambridge University Press, 1990.

theorem TopCat.RelativeCWComplex.exists_finite_cells_of_isCompact {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) {K : Set ↑Y} (hK : IsCompact K) (n : ℕ) (hKn : K ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (c.incl.app n))) : ∃ (s : Finset (HomotopicalAlgebra.RelativeCellComplex.Cells c)), (∀ γ ∈ s, γ.j < n) ∧ K ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) ∪ ⋃ γ ∈ s, Set.range ⇑(CategoryTheory.ConcreteCategory.hom γ.ι)

A compact subset of a finite stage is covered by the base and finitely many closed cells of dimension below that stage. The base space need not satisfy any separation axiom.

theorem TopCat.RelativeCWComplex.exists_finite_cells_boundary {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) (γ : HomotopicalAlgebra.RelativeCellComplex.Cells c) : ∃ (s : Finset (HomotopicalAlgebra.RelativeCellComplex.Cells c)), (∀ δ ∈ s, δ.j < γ.j) ∧ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (diskBoundaryInclusion γ.j) γ.ι)) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) ∪ ⋃ δ ∈ s, Set.range ⇑(CategoryTheory.ConcreteCategory.hom δ.ι)

The boundary of a cell in a categorical relative CW complex lies in the base and finitely many closed cells of strictly smaller dimension. No separation hypothesis is required.