The cellular approximation theorem

Let C and C' be relative CW complexes with bases D and E. This file proves that every map f : C → C' sending D into E is homotopic, relative to D, to a cellular map: one sending the skeleton skeletonLT C n into skeletonLT C' n for every n (TauCeti.exists_isCellular_homotopicRel). For CW complexes, with empty bases, every map is homotopic to a cellular map (TauCeti.exists_isCellular_homotopic). Constructions defined only for cellular maps, such as induced maps of cellular chain complexes, therefore apply to every map of CW complexes up to homotopy.

The proof is Hatcher's. Suppose f already sends skeletonLT C n into skeletonLT C' n. Through the characteristic map of an n-cell of C, f is a map of a closed n-ball sending its boundary sphere into skeletonLT C' n. Since the ball has dimension n, TauCeti.exists_homotopicRel_skeletonLT_finrank homotopes it, relative to its boundary, into skeletonLT C' (n + 1). These homotopies are the restrictions of a homotopy of f relative to skeletonLT C n (TauCeti.exists_homotopicRel_cellMap), which gives the inductive step TauCeti.exists_homotopicRel_mapsTo_skeletonLT_succ. Performing the successive homotopies one after the other (TauCeti.exists_homotopicRel_forall_mapsTo_skeletonLT) gives a single homotopy to a cellular map.

Main results

• TauCeti.exists_homotopicRel_mapsTo_skeletonLT_succ: the inductive step, a map sending skeletonLT C n into skeletonLT C' n is homotopic relative to skeletonLT C n to one that also sends skeletonLT C (n + 1) into skeletonLT C' (n + 1).
• TauCeti.exists_isCellular_homotopicRel: the cellular approximation theorem for relative CW complexes.
• TauCeti.exists_isCellular_homotopic: the cellular approximation theorem for CW complexes.

References

• A. Hatcher, Algebraic Topology, Section 4.1, Theorem 4.8.
• G. W. Whitehead, Elements of Homotopy Theory, Chapter II, Section 4.

theorem TauCeti.exists_homotopicRel_mapsTo_skeletonLT_succ {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {Y : Type v} [TopologicalSpace Y] [T2Space Y] {C' E : Set Y} [Topology.RelCWComplex C' E] (n : ℕ) (f : C(↑C, ↑C')) (hf : Set.MapsTo ⇑f {x : ↑C | ↑x ∈ Topology.RelCWComplex.skeletonLT C ↑n} {y : ↑C' | ↑y ∈ Topology.RelCWComplex.skeletonLT C' ↑n}) : ∃ (g : C(↑C, ↑C')), f.HomotopicRel g {x : ↑C | ↑x ∈ Topology.RelCWComplex.skeletonLT C ↑n} ∧ Set.MapsTo ⇑g {x : ↑C | ↑x ∈ Topology.RelCWComplex.skeletonLT C ↑(n + 1)} {y : ↑C' | ↑y ∈ Topology.RelCWComplex.skeletonLT C' ↑(n + 1)}

The inductive step of cellular approximation. A map f : C → C' sending the skeleton skeletonLT C n into skeletonLT C' n is homotopic, relative to skeletonLT C n, to a map that also sends skeletonLT C (n + 1) into skeletonLT C' (n + 1).

theorem TauCeti.exists_isCellular_homotopicRel {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {C D : Set X} [Topology.RelCWComplex C D] {C' E : Set Y} [Topology.RelCWComplex C' E] (f : ↧↑C ⟶ ↧↑C') (hf : Set.MapsTo ⇑(CategoryTheory.ConcreteCategory.hom f) {x : ↑C | ↑x ∈ D} {y : ↑C' | ↑y ∈ E}) : ∃ (g : ↧↑C ⟶ ↧↑C'), IsCellular C C' g ∧ (TopCat.Hom.hom f).HomotopicRel (TopCat.Hom.hom g) {x : ↑C | ↑x ∈ D}

The cellular approximation theorem (Hatcher, Theorem 4.8). Every map f : C → C' of relative CW complexes sending the base D into the base E is homotopic, relative to D, to a cellular map.

theorem TauCeti.exists_isCellular_homotopic {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {C : Set X} [Topology.CWComplex C] {C' : Set Y} [Topology.CWComplex C'] (f : ↧↑C ⟶ ↧↑C') : ∃ (g : ↧↑C ⟶ ↧↑C'), IsCellular C C' g ∧ (TopCat.Hom.hom f).Homotopic (TopCat.Hom.hom g)

The cellular approximation theorem for CW complexes (Hatcher, Theorem 4.8). Every map of CW complexes is homotopic to a cellular map.