A CW complex is a quotient of its base and its closed cells

The weak-topology axiom of a relative CW complex C with base D says that a subset of C is closed as soon as its intersections with D and with every closed cell are. Equivalently, the map from the disjoint union of D and of one closed unit ball for each cell, given by the inclusion of D and by the characteristic maps, is a quotient map onto C.

Products with a locally compact space preserve quotient maps, so a map out of Z × C, for Z locally compact, is continuous as soon as it is continuous on Z × D and on the product of Z with every closed cell, the latter read through the characteristic maps. This is how homotopies out of a CW complex (the case Z = I) are built cell by cell.

Main results

• TauCeti.isQuotientMap_sumElim_base_map: the base inclusion and the characteristic maps together form a quotient map onto the complex.
• TauCeti.continuous_complex_iff: a map out of a CW complex is continuous exactly when it is continuous on the base and along every characteristic map.
• TauCeti.continuous_prod_complex_iff: the same criterion for maps out of Z × C with Z locally compact.

References

• A. Hatcher, Algebraic Topology, Chapter 0 and the Appendix "Topology of Cell Complexes": the topology of a CW complex is the quotient topology from its cells, and products with locally compact spaces.

theorem TauCeti.isQuotientMap_sumElim_base_map {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] : Topology.IsQuotientMap (Sum.elim (fun (d : ↑D) => ⟨↑d, ⋯⟩) fun (p : (m : (n : ℕ) × Topology.RelCWComplex.cell C n) × ↑(Metric.closedBall 0 1)) => ⟨↑(Topology.RelCWComplex.map p.fst.fst p.fst.snd) ↑p.snd, ⋯⟩)

A relative CW complex is a quotient of its base and its closed cells. The map from the disjoint union of the base D and of one closed unit ball for every cell, given by the inclusion of D and by the characteristic maps, is a quotient map onto C.

theorem TauCeti.continuous_complex_iff {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {Y : Type u_1} [TopologicalSpace Y] {g : ↑C → Y} : Continuous g ↔ (∀ (n : ℕ) (j : Topology.RelCWComplex.cell C n), Continuous fun (y : ↑(Metric.closedBall 0 1)) => g ⟨↑(Topology.RelCWComplex.map n j) ↑y, ⋯⟩) ∧ Continuous fun (d : ↑D) => g ⟨↑d, ⋯⟩

A map out of a relative CW complex is continuous exactly when it is continuous on the base and along the characteristic map of every cell.

theorem TauCeti.continuous_prod_complex_iff {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {Z : Type u_1} {Y : Type u_2} [TopologicalSpace Z] [LocallyCompactSpace Z] [TopologicalSpace Y] {g : Z × ↑C → Y} : Continuous g ↔ (∀ (n : ℕ) (j : Topology.RelCWComplex.cell C n), Continuous fun (p : Z × ↑(Metric.closedBall 0 1)) => g (p.1, ⟨↑(Topology.RelCWComplex.map n j) ↑p.2, ⋯⟩)) ∧ Continuous fun (p : Z × ↑D) => g (p.1, ⟨↑p.2, ⋯⟩)

Continuity criterion for maps out of Z × C. For a locally compact space Z, a map out of Z × C is continuous exactly when it is continuous on Z × D and on the product of Z with every closed cell, the latter read through the characteristic maps. For Z = I this builds homotopies out of a CW complex cell by cell.