Homotoping maps out of a relative CW complex skeleton by skeleton

Let C be a relative CW complex with base D. Several classical theorems homotope a map f : C → Y to a map with better behaviour on each skeleton, one skeleton at a time: the cellular approximation theorem homotopes a map of CW complexes to a cellular one, and the compression lemma homotopes a map of pairs (C, D) → (Y, B) into B. This file supplies the two steps they share.

• One dimension at a time. Homotopies of the maps f ∘ Φⱼ on the closed unit ball, one for each n-cell j with characteristic map Φⱼ and each relative to the boundary sphere, are the restrictions of a single homotopy of f relative to skeletonLT C n (TauCeti.exists_homotopicRel_cellMap). The cell homotopies glue over the closed n-cells (TauCeti.exists_continuousMap_prod_skeletonLT_succ) to a homotopy on skeletonLT C (n + 1), which the homotopy extension property of that skeleton (TauCeti.hasHomotopyExtensionProperty_skeletonLT) extends over C.
• All dimensions. Let S n be sets of Y, and suppose that every map sending skeletonLT C n into S n is homotopic relative to skeletonLT C n to a map that also sends skeletonLT C (n + 1) into S (n + 1). Then every map sending the base D into S 0 is homotopic relative to D to a map sending skeletonLT C n into S n for every n (TauCeti.exists_homotopicRel_forall_mapsTo_skeletonLT). The n-th of the successive homotopies is performed during the time interval [1 - 2⁻ⁿ, 1 - 2⁻ⁿ⁻¹]. The resulting single homotopy is continuous because on skeletonLT C n all the later homotopies are stationary, so there it is a finite concatenation, and a map out of I × C is continuous as soon as it is continuous on I times every skeleton (TauCeti.exists_continuousMap_prod_complex_of_skeletonLT).

Main results

• TauCeti.exists_homotopicRel_cellMap: homotopies of the closed n-cells relative to their boundaries extend to a homotopy of the complex relative to skeletonLT C n.
• TauCeti.exists_homotopicRel_forall_mapsTo_skeletonLT: the infinite concatenation of homotopies improving a map one skeleton at a time.

References

• A. Hatcher, Algebraic Topology, Section 4.1, the proofs of Lemma 4.6 (the compression lemma) and Theorem 4.8 (cellular approximation).
• G. W. Whitehead, Elements of Homotopy Theory, Chapter II.

theorem TauCeti.exists_homotopicRel_cellMap {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {Y : Type v} [TopologicalSpace Y] (n : ℕ) (f : C(↑C, Y)) (ψ : Topology.RelCWComplex.cell C n → C(↑(Metric.closedBall 0 1), Y)) (hψ : ∀ (j : Topology.RelCWComplex.cell C n), (f.comp (cellMap j)).HomotopicRel (ψ j) {y : ↑(Metric.closedBall 0 1) | ↑y ∈ Metric.sphere 0 1}) : ∃ (g : C(↑C, Y)), f.HomotopicRel g {x : ↑C | ↑x ∈ Topology.RelCWComplex.skeletonLT C ↑n} ∧ ∀ (j : Topology.RelCWComplex.cell C n) (y : ↑(Metric.closedBall 0 1)), g ((cellMap j) y) = (ψ j) y

Homotoping a map one dimension at a time. Let f : C → Y be a map out of a relative CW complex, and for every n-cell j let f ∘ Φⱼ be homotopic, relative to the boundary sphere, to a map ψ j of the closed unit ball, where Φⱼ is the characteristic map of j. Then f is homotopic relative to skeletonLT C n to a map g with g ∘ Φⱼ = ψ j for every n-cell j.

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

Homotoping a map skeleton by skeleton. Let S n be sets of Y such that every map C → Y sending skeletonLT C n into S n is homotopic, relative to skeletonLT C n, to a map that also sends skeletonLT C (n + 1) into S (n + 1). Then every map f : C → Y sending the base D into S 0 is homotopic, relative to D, to a map sending skeletonLT C n into S n for every n.