The cylinder on a relative CW complex

For a relative CW complex (C, D) in a Hausdorff space X, the cylinder C × I in X × I is a CW complex relative to C × {0, 1} ∪ D × I (TauCeti.relCWComplexCylinder). Its (n + 1)-cells are the products of the n-cells of (C, D) with the open interval (0, 1), and it has no 0-cells (TauCeti.cellCylinderEquiv). The characteristic map of the cylinder on an n-cell keeps the n coordinates of the cell first and puts the interval coordinate last, sending x : Fin (n + 1) → ℝ to (φ (Fin.init x), projIcc 0 1 _ ((x (Fin.last n) + 1) / 2)) for the characteristic map φ of the cell; on the closed unit ball the interval coordinate is just (x (Fin.last n) + 1) / 2. The base contains the two ends C × {0} and C × {1}, the images of the inclusions x ↦ (x, 0) and x ↦ (x, 1).

A homotopy of maps out of C is a map out of C × I, and a homotopy relative to D between two given maps is a map out of C × I prescribed on C × {0, 1} ∪ D × I. So this relative structure is what lets cell-by-cell arguments (homotopy extension, compression into a subspace) apply to homotopies themselves; for instance, the injectivity half of Hatcher, Proposition 4.22 (a weak homotopy equivalence f : Y → Z induces injections [K, Y] → [K, Z] for CW complexes K) compresses a homotopy defined on C × I relative to its two ends.

The only point that is not formal is the weak topology. Since I is compact, the cylinder has the weak topology of the closed cells closedCell n j × I and of the base: this holds for the product of a relative CW complex with any compact regular space (Topology.RelCWComplex.closed_prod), because the projection X × Y → X is then a closed map.

Main declarations

• Topology.RelCWComplex.closed_prod: the product of a relative CW complex with a compact regular space has the weak topology of the products of its closed cells and of its base.
• TauCeti.relCWComplexCylinder: the relative CW structure on C ×ˢ univ in X × I, relative to C ×ˢ {0, 1} ∪ D ×ˢ univ.
• TauCeti.cellCylinderEquiv: its (n + 1)-cells are the n-cells of C; it has no 0-cells (TauCeti.isEmpty_cell_relCWComplexCylinder_zero). Its characteristic maps, open cells, closed cells and cell frontiers are described by TauCeti.map_relCWComplexCylinder_apply, TauCeti.openCell_relCWComplexCylinder, TauCeti.closedCell_relCWComplexCylinder and TauCeti.cellFrontier_relCWComplexCylinder.

Implementation notes

The construction adapts that of the finite product TauCeti.cwComplexProd (TauCeti/Topology/CWComplex/Classical/Product.lean): the characteristic map of a cell of the cylinder is the product of the characteristic map of a cell of C with that of the interval, precomposed with the sup-norm isometry Fin.initLastIsometry splitting off the last coordinate.

References

• A. Hatcher, Algebraic Topology, Chapter 0 (products of CW complexes) and Section 4.1 (Proposition 4.22); Appendix, Theorem A.6, for the topology of products of CW complexes.

theorem Topology.RelCWComplex.closed_prod {X : Type u_1} [TopologicalSpace X] [T2Space X] {Y : Type u_2} [TopologicalSpace Y] [CompactSpace Y] [RegularSpace Y] (C : Set X) {D : Set X} [RelCWComplex C D] (A : Set (X × Y)) (hA : A ⊆ C ×ˢ Set.univ) : IsClosed A ↔ (∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j ×ˢ Set.univ)) ∧ IsClosed (A ∩ D ×ˢ Set.univ)

The product of a relative CW complex with a compact regular space has the weak topology: a subset A of C ×ˢ univ in X × Y is closed if and only if its intersections with the products closedCell n j ×ˢ univ and with D ×ˢ univ are closed.

@[instance_reducible]

noncomputable def TauCeti.relCWComplexCylinder {X : Type u} [TopologicalSpace X] (C D : Set X) [Topology.RelCWComplex C D] [T2Space X] : Topology.RelCWComplex (C ×ˢ Set.univ) (C ×ˢ {0, 1} ∪ D ×ˢ Set.univ)

The cylinder on a relative CW complex. For a relative CW complex (C, D) in a Hausdorff space X, the cylinder C ×ˢ univ in X × I is a CW complex relative to C ×ˢ {0, 1} ∪ D ×ˢ univ. Its (n + 1)-cells are the n-cells of C (TauCeti.cellCylinderEquiv), with characteristic maps x ↦ (φ (Fin.init x), projIcc 0 1 _ ((x (Fin.last n) + 1) / 2)) (TauCeti.map_relCWComplexCylinder_apply), and it has no 0-cells.

It is not an instance: the base of a relative CW complex is an outParam, and C ×ˢ univ carries other relative CW structures.

instance TauCeti.isEmpty_cell_relCWComplexCylinder_zero {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] : IsEmpty (Topology.RelCWComplex.cell (C ×ˢ Set.univ) 0)

The cylinder on a relative CW complex has no 0-cells.

def TauCeti.cellCylinderEquiv {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] (n : ℕ) : Topology.RelCWComplex.cell (C ×ˢ Set.univ) (n + 1) ≃ Topology.RelCWComplex.cell C n

The (n + 1)-cells of the cylinder on a relative CW complex (C, D) are the n-cells of C.

@[simp]

theorem TauCeti.map_relCWComplexCylinder_apply {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {n : ℕ} (i : Topology.RelCWComplex.cell (C ×ˢ Set.univ) (n + 1)) (x : Fin (n + 1) → ℝ) : ↑(Topology.RelCWComplex.map (n + 1) i) x = (↑(Topology.RelCWComplex.map n ((cellCylinderEquiv n) i)) (Fin.init x), Set.projIcc 0 1 ⋯ ((x (Fin.last n) + 1) / 2))

The characteristic map of the cylinder on an n-cell with characteristic map φ is x ↦ (φ (Fin.init x), projIcc 0 1 _ ((x (Fin.last n) + 1) / 2)); on the closed unit ball its interval coordinate is (x (Fin.last n) + 1) / 2.

@[simp]

theorem TauCeti.openCell_relCWComplexCylinder {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {n : ℕ} (i : Topology.RelCWComplex.cell (C ×ˢ Set.univ) (n + 1)) : Topology.RelCWComplex.openCell (n + 1) i = Topology.RelCWComplex.openCell n ((cellCylinderEquiv n) i) ×ˢ Set.Ioo 0 1

The open cell of the cylinder on an n-cell is the product of the open cell with the open interval (0, 1).

@[simp]

theorem TauCeti.closedCell_relCWComplexCylinder {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {n : ℕ} (i : Topology.RelCWComplex.cell (C ×ˢ Set.univ) (n + 1)) : Topology.RelCWComplex.closedCell (n + 1) i = Topology.RelCWComplex.closedCell n ((cellCylinderEquiv n) i) ×ˢ Set.univ

The closed cell of the cylinder on an n-cell is the product of the closed cell with I.

@[simp]

theorem TauCeti.cellFrontier_relCWComplexCylinder {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {n : ℕ} (i : Topology.RelCWComplex.cell (C ×ˢ Set.univ) (n + 1)) : Topology.RelCWComplex.cellFrontier (n + 1) i = Topology.RelCWComplex.cellFrontier n ((cellCylinderEquiv n) i) ×ˢ Set.univ ∪ Topology.RelCWComplex.closedCell n ((cellCylinderEquiv n) i) ×ˢ {0, 1}

The boundary of the cylinder on an n-cell is the cylinder on the boundary of the cell together with the two ends of the cylinder on the closed cell.