Classical relative CW complexes are categorical relative CW complexes

Mathlib has two notions of CW complex. The classical Topology.RelCWComplex C D describes a subset C of a topological space through explicit cells and characteristic maps, while the categorical TopCat.RelativeCWComplex f presents the target of a morphism f : X ⟶ Y of TopCat as the colimit of a sequence of spaces, each obtained from the previous one by attaching disks along their boundary spheres in a pushout square. This file goes from the first to the second: when the ambient space is Hausdorff (a T2Space, which this file assumes throughout), a classical relative CW complex C with base D gives a categorical relative CW complex structure on the inclusion of D into C (TauCeti.toRelativeCWComplex).

The n-th space of the sequence is the skeleton skeletonLT C n itself, and the cells attached at step n are the n-cells cell C n. The two ingredients are the following.

• Attaching the n-cells to skeletonLT C n along their boundaries gives skeletonLT C (n + 1): the square formed by the coproducts of the disks 𝔻 n and of their boundaries ∂𝔻 n over the n-cells, the characteristic maps and the inclusion of skeleta is a pushout in TopCat (TauCeti.isPushout_skeletonObj). The disk 𝔻 n of TopCat is the Euclidean unit ball, which is carried onto the closed unit ball of the sup norm on Fin n → ℝ, the domain of the characteristic maps, by the radial homeomorphism TauCeti.diskHomeomorphClosedBall. The characteristic and attaching maps on 𝔻 n and ∂𝔻 n are TauCeti.cellDiskHom and TauCeti.cellAttachingMap, from TauCeti.Topology.CWComplex.Classical.Skeleton.CellMap.
• C is the colimit in TopCat of its skeleta (TauCeti.isColimitSkeletonCocone, proved in TauCeti.Topology.CWComplex.Classical.Skeleton.Colimit).

In both cases the universal property comes from the weak topology of the complex: maps out of the next skeleton, or out of the whole complex, are built cell by cell and skeleton by skeleton with TauCeti.exists_continuousMap_prod_skeletonLT_succ and TauCeti.exists_continuousMap_prod_complex_of_skeletonLT. These rest on the closedness axiom of the classical structure in a Hausdorff space. The Hausdorff hypothesis cannot be dropped: the indiscrete two-point space with two 0-cells satisfies the axioms of a classical CW complex, while attaching two 0-cells to the empty space gives the discrete two-point space.

Main definitions and results

• TauCeti.isPushout_skeletonObj, TauCeti.skeletonAttachCells: skeletonLT C (n + 1) is obtained from skeletonLT C n by attaching the n-cells.
• TauCeti.toRelativeCWComplex: the categorical relative CW complex structure on D ⟶ C. Its n-th space is skeletonLT C n (TauCeti.range_toRelativeCWComplex_incl_app), its cells are those of C (TauCeti.toRelativeCWComplexCellsEquiv), and its cell inclusions are the characteristic maps (TauCeti.coe_toRelativeCWComplex_cells_ι_apply).

References

• A. Hatcher, Algebraic Topology, Appendix, Proposition A.2, on the equivalence of the two definitions of CW complexes.
• R. Fritsch and R. Piccinini, Cellular Structures in Topology, Cambridge University Press, 1990, for the categorical definition.

theorem TauCeti.cellAttachingMap_comp_skeletonFunctor_map {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) : CategoryTheory.CategoryStruct.comp (cellAttachingMap j) ((skeletonFunctor C).map (CategoryTheory.homOfLE ⋯)) = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (cellDiskHom j)

The attaching map of a cell is the characteristic map on the boundary of the disk.

theorem TauCeti.cellAttachingMap_comp_skeletonFunctor_map_assoc {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) {Z : TopCat} (h : skeletonObj C n.succ ⟶ Z) : CategoryTheory.CategoryStruct.comp (cellAttachingMap j) (CategoryTheory.CategoryStruct.comp (TopCat.ofHom (ContinuousMap.inclusion ⋯)) h) = CategoryTheory.CategoryStruct.comp (TopCat.diskBoundaryInclusion n) (CategoryTheory.CategoryStruct.comp (cellDiskHom j) h)

The attaching map of a cell is the characteristic map on the boundary of the disk.

theorem TauCeti.isPushout_skeletonObj {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : CategoryTheory.IsPushout (CategoryTheory.Limits.Sigma.desc cellAttachingMap) (CategoryTheory.Limits.Sigma.map fun (x : Topology.RelCWComplex.cell C n) => TopCat.diskBoundaryInclusion n) ((skeletonFunctor C).map (CategoryTheory.homOfLE ⋯)) (CategoryTheory.Limits.Sigma.desc cellDiskHom)

Attaching the n-cells to the (n - 1)-skeleton gives the n-skeleton. The square formed by the inclusion of the boundary spheres into the disks over the n-cells, the attaching maps, the characteristic maps and the inclusion skeletonLT C n ⊆ skeletonLT C (n + 1) is a pushout in TopCat.

noncomputable def TauCeti.skeletonAttachCells {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : HomotopicalAlgebra.AttachCells (TopCat.RelativeCWComplex.basicCell n) ((skeletonFunctor C).map (CategoryTheory.homOfLE ⋯))

The n-skeleton skeletonLT C (n + 1) is obtained from skeletonLT C n by attaching one n-disk along its boundary sphere for each n-cell, through the attaching maps TauCeti.cellAttachingMap. The body is exposed so that the cells are cell C n by definition.

@[simp]

theorem TauCeti.skeletonAttachCells_cell {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] {n : ℕ} (j : Topology.RelCWComplex.cell C n) : (skeletonAttachCells C n).cell j = cellDiskHom j

The inclusion of an n-cell attached in TauCeti.skeletonAttachCells is its characteristic map.

noncomputable def TauCeti.toRelativeCWComplex {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : TopCat.RelativeCWComplex (TopCat.ofHom (ContinuousMap.inclusion ⋯))

A classical relative CW complex in a Hausdorff space is a categorical relative CW complex. The inclusion of the base D into C is the transfinite composition of the inclusions of the skeleta skeletonLT C n, and the step from skeletonLT C n to skeletonLT C (n + 1) attaches the n-cells of C along their attaching maps. The body is exposed so that the n-th space is the skeleton skeletonObj C n and the cells attached at step n are cell C n by definition.

theorem TauCeti.coe_toRelativeCWComplex_incl_app_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] (n : ℕ) (x : ↑((toRelativeCWComplex C).F.obj n)) : ↑((CategoryTheory.ConcreteCategory.hom ((toRelativeCWComplex C).incl.app n)) x) = ↑x

The n-th space of TauCeti.toRelativeCWComplex C is the skeleton skeletonLT C n, included in C.

theorem TauCeti.range_toRelativeCWComplex_incl_app {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] (n : ℕ) : (Set.range fun (x : ↑((toRelativeCWComplex C).F.obj n)) => ↑((CategoryTheory.ConcreteCategory.hom ((toRelativeCWComplex C).incl.app n)) x)) = ↑(Topology.RelCWComplex.skeletonLT C ↑n)

The image in C of the n-th space of TauCeti.toRelativeCWComplex C is skeletonLT C n.

def TauCeti.toRelativeCWComplexCellsEquiv {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] : HomotopicalAlgebra.RelativeCellComplex.Cells (toRelativeCWComplex C) ≃ (n : ℕ) × Topology.RelCWComplex.cell C n

The cells of TauCeti.toRelativeCWComplex C are the cells of C: a cell attached at step n is an n-cell.

@[simp]

theorem TauCeti.toRelativeCWComplexCellsEquiv_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] (γ : HomotopicalAlgebra.RelativeCellComplex.Cells (toRelativeCWComplex C)) : toRelativeCWComplexCellsEquiv γ = ⟨γ.j, γ.k⟩

@[simp]

theorem TauCeti.toRelativeCWComplexCellsEquiv_symm_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : toRelativeCWComplexCellsEquiv.symm ⟨n, i⟩ = { j := n, hj := ⋯, k := i }

theorem TauCeti.coe_toRelativeCWComplex_cells_ι_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D C : Set X} [Topology.RelCWComplex C D] (γ : HomotopicalAlgebra.RelativeCellComplex.Cells (toRelativeCWComplex C)) (z : ↑(TopCat.disk γ.j)) : ↑((CategoryTheory.ConcreteCategory.hom γ.ι) z) = ↑(Topology.RelCWComplex.map γ.j γ.k) ↑((diskHomeomorphClosedBall γ.j) z)

The inclusion of a cell of TauCeti.toRelativeCWComplex C is the characteristic map of the corresponding cell of C, read on the Euclidean disk through TauCeti.diskHomeomorphClosedBall.