Comparison of categorical and classical CW structures

The conversions between categorical and classical relative CW complexes preserve their cellular presentations. Starting with a categorical complex, its stages are naturally homeomorphic to the stages obtained by passing to the classical structure and back. The homeomorphisms commute with the inclusions into the target. Starting with a classical complex, the recovered cells correspond to the original cells, and their characteristic maps agree on the closed unit ball after inclusion into the original ambient space.

These comparisons use the specified CW structures throughout: no replacement CW model or choice of characteristic maps is made. The target of the categorical round trip is the subspace Set.univ of the original target, identified with it by Homeomorph.Set.univ.

Starting with a classical CW complex C in a Hausdorff space, the round trip is a classical CW structure on the whole subspace C (TauCeti.cwComplexUniv), finite when C is (TauCeti.finite_cwComplexUniv). Consequently the finite CW model of a space of finite CW type can be taken to be a whole space (TauCeti.FiniteCWType.exists_homotopyEquiv_univ), which is the form needed to lift the model along a covering map of it.

References

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

noncomputable def TopCat.RelativeCWComplex.classicalRoundTripStageHomeomorph {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] (n : ℕ) : ↑(c.F.obj n) ≃ₜ ↑(TauCeti.skeletonObj Set.univ n)

Each stage of a categorical relative CW complex is homeomorphic to the corresponding stage obtained by converting to the classical structure and back.

@[simp]

theorem TopCat.RelativeCWComplex.classicalRoundTripStageHomeomorph_apply_coe {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] (n : ℕ) (x : ↑(c.F.obj n)) : ↑((c.classicalRoundTripStageHomeomorph n) x) = (CategoryTheory.ConcreteCategory.hom (c.incl.app n)) x

The stage comparison is the original inclusion, read in the corresponding skeleton.

@[simp]

theorem TopCat.RelativeCWComplex.classicalRoundTripStageHomeomorph_symm_apply_coe {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] (n : ℕ) (x : ↑(TauCeti.skeletonObj Set.univ n)) : (CategoryTheory.ConcreteCategory.hom (c.incl.app n)) ((c.classicalRoundTripStageHomeomorph n).symm x) = ↑x

The inverse stage comparison recovers the point of the original stage with the specified image in the target.

noncomputable def TopCat.RelativeCWComplex.classicalRoundTripIso {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] : c.F ≅ (TauCeti.toRelativeCWComplex Set.univ).F

The stage homeomorphisms form an isomorphism of the sequential diagrams, so they preserve all skeletal inclusions, not only the individual spaces.

theorem TopCat.RelativeCWComplex.classicalRoundTripIso_hom_app {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] (n : ℕ) : c.classicalRoundTripIso.hom.app n = (isoOfHomeo (c.classicalRoundTripStageHomeomorph n)).hom

theorem TopCat.RelativeCWComplex.classicalRoundTripIso_inv_app {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] (n : ℕ) : c.classicalRoundTripIso.inv.app n = (isoOfHomeo (c.classicalRoundTripStageHomeomorph n)).inv

theorem TopCat.RelativeCWComplex.classicalRoundTripIso_hom_app_apply {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] (n : ℕ) (x : ↑(c.F.obj n)) : (CategoryTheory.ConcreteCategory.hom (c.classicalRoundTripIso.hom.app n)) x = (c.classicalRoundTripStageHomeomorph n) x

Evaluation of the forward comparison uses the stage homeomorphism. The application form also fixes the dependent presentation of the reconstructed stage for simplification.

theorem TopCat.RelativeCWComplex.classicalRoundTripIso_inv_app_apply {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] (n : ℕ) (x : ↑(TauCeti.skeletonObj Set.univ n)) : (CategoryTheory.ConcreteCategory.hom (c.classicalRoundTripIso.inv.app n)) x = (c.classicalRoundTripStageHomeomorph n).symm x

Evaluation of the inverse comparison uses the inverse stage homeomorphism.

theorem TopCat.RelativeCWComplex.classicalRoundTripIso_hom_app_incl {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] (n : ℕ) : CategoryTheory.CategoryStruct.comp (c.classicalRoundTripIso.hom.app n) (CategoryTheory.CategoryStruct.comp ((TauCeti.toRelativeCWComplex Set.univ).incl.app n) (isoOfHomeo (Homeomorph.Set.univ ↑Y)).hom) = c.incl.app n

The comparison of sequential diagrams commutes with their maps to the original target, using the canonical identification of the round trip's target Set.univ with that target.

theorem TopCat.RelativeCWComplex.isoBot_inv_classicalRoundTripIso_hom_app_zero {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] : CategoryTheory.CategoryStruct.comp c.isoBot.inv (CategoryTheory.CategoryStruct.comp (c.classicalRoundTripIso.hom.app 0) (TauCeti.toRelativeCWComplex Set.univ).isoBot.hom) = (isoOfHomeo ⋯.toHomeomorph).hom

At the initial stage, the comparison identifies the original base with its image under the given closed embedding.

theorem TopCat.RelativeCWComplex.classicalRoundTrip_cells_ι_apply {X Y : TopCat} {f : X ⟶ Y} (c : RelativeCWComplex f) [T2Space ↑Y] (n : ℕ) (i : ((TauCeti.toRelativeCWComplex Set.univ).attachCells n ⋯).ι) (z : ↑(disk n)) : ↑((CategoryTheory.ConcreteCategory.hom { j := n, hj := ⋯, k := i }.ι) z) = (CategoryTheory.ConcreteCategory.hom { j := n, hj := ⋯, k := (c.toRelCWComplexCellEquiv n) i }.ι) z

After identifying the target, the cell inclusions of the categorical round trip are the original cell inclusions.

theorem TauCeti.categoricalRoundTrip_map_apply {X : Type u} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n) (x : ↑(Metric.closedBall 0 1)) : ↑(↑(Topology.RelCWComplex.map n i) ↑x) = ↑(Topology.RelCWComplex.map n (((toRelativeCWComplex C).toRelCWComplexCellEquiv n) i)) ↑x

The characteristic maps recovered by the classical round trip agree with the original maps on the closed unit ball, after inclusion of the complex into its ambient space.

theorem TauCeti.image_categoricalRoundTrip_skeletonLT {X : Type u} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : Subtype.val '' ↑(Topology.RelCWComplex.skeletonLT Set.univ ↑n) = ↑(Topology.RelCWComplex.skeletonLT C ↑n)

The skeleta of the recovered classical structure are exactly the original skeleta after inclusion into the ambient space. This includes the base, at stage zero.

@[instance_reducible]

noncomputable def TauCeti.cwComplexUniv {X : Type u} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] : Topology.CWComplex Set.univ

A CW complex is a CW structure on its own underlying space. The classical CW structure on the whole subspace C of a Hausdorff space given by the categorical round trip (toRelativeCWComplex C).toRelCWComplex: it has the cells of C, and its base, the range of the map out of the empty subspace, is empty.

theorem TauCeti.finite_cwComplexUniv {X : Type u} [TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] [Topology.RelCWComplex.Finite C] : Topology.RelCWComplex.Finite Set.univ

The CW structure cwComplexUniv C on the whole subspace C is finite when C is.

theorem TauCeti.FiniteCWType.exists_homotopyEquiv_univ (Y : Type u) [TopologicalSpace Y] [h : FiniteCWType Y] : ∃ (Z : Type u) (x : TopologicalSpace Z) (_ : T2Space Z) (x_2 : Topology.CWComplex Set.univ), Topology.RelCWComplex.Finite Set.univ ∧ Nonempty (ContinuousMap.HomotopyEquiv Y Z)

A space of finite CW type is homotopy equivalent to a Hausdorff space carrying a finite CW structure on the whole space.