Categorical relative CW complexes are classical relative CW complexes

A categorical relative CW complex c : TopCat.RelativeCWComplex f induces a classical structure c.toRelCWComplex : Topology.RelCWComplex Set.univ (Set.range f) on its target. No separation assumptions are needed. The cells in dimension n are exactly the cells attached at step n. Their characteristic maps are the original cell inclusions, composed with the inverse of TauCeti.diskHomeomorphClosedBall, the fixed radial comparison between the Euclidean disk and the max-norm closed unit ball.

The construction uses the embeddings and disjointness of open cells, closure finiteness, and the weak topology of categorical relative cell complexes. The equations below identify the classical open and closed cells with the original inclusions, so the classical CW theory applies to spaces constructed by categorical cell attachment. The stage formula in terms of closed cells needs no separation assumption; identification with Mathlib's named skeletonLT requires a Hausdorff target, as that classical subcomplex construction itself has this hypothesis.

For an absolute categorical CW complex c : TopCat.CWComplex X the base is empty, so c gives a classical CW structure on Set.univ (TopCat.CWComplex.toCWComplex), and X has CW type (TopCat.CWComplex.cwType).

References

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

@[instance_reducible]

noncomputable def TopCat.RelativeCWComplex.toRelCWComplex {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) : Topology.RelCWComplex Set.univ (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))

The classical relative CW structure on the target of a categorical relative CW complex. The n-cells are those attached at step n, with their characteristic maps read through the fixed radial identification of the max-norm ball with the Euclidean disk.

def TopCat.RelativeCWComplex.toRelCWComplexCellEquiv {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) (n : ℕ) : Topology.RelCWComplex.cell Set.univ n ≃ (c.attachCells n ⋯).ι

The cells in each dimension of the induced classical structure are the original attachment indices. This equivalence identifies the carriers without unfolding the CW structure.

@[simp]

theorem TopCat.RelativeCWComplex.toRelCWComplex_map_apply {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n) (x : ↑(Metric.closedBall 0 1)) : ↑(Topology.RelCWComplex.map n i) ↑x = (CategoryTheory.ConcreteCategory.hom { j := n, hj := ⋯, k := (c.toRelCWComplexCellEquiv n) i }.ι) ((TauCeti.diskHomeomorphClosedBall n).symm x)

The classical characteristic map on the closed ball is the original cell inclusion after radial identification with the Euclidean disk.

@[simp]

theorem TopCat.RelativeCWComplex.toRelCWComplex_map_disk {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n) (z : ↑(disk n)) : ↑(Topology.RelCWComplex.map n i) ↑((TauCeti.diskHomeomorphClosedBall n) z) = (CategoryTheory.ConcreteCategory.hom { j := n, hj := ⋯, k := (c.toRelCWComplexCellEquiv n) i }.ι) z

Reading a classical characteristic map on the radially corresponding point of the disk recovers the categorical cell inclusion.

theorem TopCat.RelativeCWComplex.toRelCWComplex_openCell {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n) : Topology.RelCWComplex.openCell n i = ⇑(CategoryTheory.ConcreteCategory.hom { j := n, hj := ⋯, k := (c.toRelCWComplexCellEquiv n) i }.ι) '' (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (diskBoundaryInclusion n)))ᶜ

The open cells of the induced classical structure are the original open cells.

theorem TopCat.RelativeCWComplex.toRelCWComplex_closedCell {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n) : Topology.RelCWComplex.closedCell n i = Set.range ⇑(CategoryTheory.ConcreteCategory.hom { j := n, hj := ⋯, k := (c.toRelCWComplexCellEquiv n) i }.ι)

The closed cells of the induced classical structure are the ranges of the original cell inclusions.

theorem TopCat.RelativeCWComplex.toRelCWComplex_cellFrontier {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n) : Topology.RelCWComplex.cellFrontier n i = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (diskBoundaryInclusion n) { j := n, hj := ⋯, k := (c.toRelCWComplexCellEquiv n) i }.ι))

The cell frontiers of the induced classical structure are the original boundary images.

theorem TopCat.RelativeCWComplex.range_incl_app_eq_union_toRelCWComplex_closedCell {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) (n : ℕ) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (c.incl.app n)) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (i : Topology.RelCWComplex.cell Set.univ m), Topology.RelCWComplex.closedCell m i

The image of the n-th categorical stage is the base together with the induced classical closed cells of dimension less than n. No separation hypothesis is needed.

theorem TopCat.RelativeCWComplex.range_incl_app_eq_toRelCWComplex_skeletonLT {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] (n : ℕ) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (c.incl.app n)) = ↑(Topology.RelCWComplex.skeletonLT Set.univ ↑n)

The image of the n-th categorical stage is the classical skeleton below dimension n. The Hausdorff hypothesis is needed only to name Mathlib's classical skeletonLT.

theorem TopCat.RelativeCWComplex.skeletonLT_toRelCWComplex_eq_range {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] {n : ℕ} (hc : ∀ m < n, IsEmpty (c.attachCells m ⋯).ι) : ↑(Topology.RelCWComplex.skeletonLT Set.univ ↑n) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom f)

Below the dimension of its lowest cells, the classical skeleton is the base: if no cells of dimension less than n are attached, then skeletonLT univ n is the range of f.

@[instance_reducible]

noncomputable def TopCat.CWComplex.toCWComplex {X : TopCat} (c : X.CWComplex) : Topology.CWComplex Set.univ

The classical CW structure on a space with a categorical CW structure: the cells and characteristic maps of the classical relative structure c.toRelCWComplex, whose base, the range of the map out of the empty space, is empty.

theorem TopCat.CWComplex.cwType {X : TopCat} (c : X.CWComplex) : TauCeti.CWType ↑X

A space with a categorical CW structure has CW type.