Compressing maps of low-dimensional compacta into skeleta

Let C be a relative CW complex in a Hausdorff space X, and write Xᵏ = skeletonLT C (k + 1) for its k-skeleton. Let K be a compact subset of a finite-dimensional real normed space E. This file proves that maps K → C into the complex can be pushed off the cells of dimension greater than dim E, by homotopies of maps into the complex:

• If dim E < k and f : K → C lands in Xᵏ, then for every k-cell j, f is homotopic, relative to the points not sent into the open cell j, to a map sending the points that f sends into the open cell j into its frontier (TauCeti.exists_homotopicRel_cellFrontier). This is Hatcher's Lemma 4.10 together with the radial push from the proof of Theorem 4.8.
• Doing this for the finitely many k-cells that the compact image of f meets compresses f into Xᵏ⁻¹, relative to the points already sent there (TauCeti.exists_homotopicRel_skeletonLT).
• Since the image of f lies in some finite skeleton, every map f : K → C into the complex is homotopic, relative to the points sent into Xⁿ with dim E ≤ n, to a map into Xⁿ (TauCeti.exists_homotopicRel_skeletonLT_finrank). Applied to a closed i-ball with i ≤ n, it homotopes every map of pairs (Dⁱ, Sⁱ⁻¹) → (C, Xⁿ) relative to Sⁱ⁻¹ into Xⁿ; this is the compression property behind Hatcher's Corollary 4.12, that the pair (C, Xⁿ) is n-connected.
• In dimensions zero and one, this says that every point of C is joined to Xⁿ, and that paths in C between points of Xⁿ compress into Xⁿ, relative to their endpoints (TauCeti.exists_joined_skeletonLT, TauCeti.exists_path_homotopic_skeletonLT, TauCeti.joined_skeletonLT_iff).

These are the steps of the cellular approximation theorem that concern a single cell of the domain; the theorem itself (TauCeti.exists_isCellular_homotopicRel) follows from them by induction over the skeleta of the domain using the homotopy extension property.

To push a map off a k-cell, read the open cell, which is open in Xᵏ, as a chart through the inverse of its characteristic map (TauCeti.openCellChart). ContinuousMap.exists_homotopyRel_notMem_range homotopes the map off one point p of the open cell, and, the image being compact, off a neighbourhood of p. The radial deformation of the closed unit ball away from p onto the unit sphere (Convex.exists_homotopyRel_frontier), read through the characteristic map (TauCeti.cellDeformation), is a homotopy of Xᵏ that is supported in the open cell and ends by pushing the rest of the cell onto its frontier.

References

• A. Hatcher, Algebraic Topology, Section 4.1, Lemma 4.10, Theorem 4.8 and Corollary 4.12.

theorem TauCeti.exists_homotopicRel_cellFrontier {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {k : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsCompact K) (hk : Module.finrank ℝ E < k) (j : Topology.RelCWComplex.cell C k) (f : C(↑K, ↑C)) (hf : ∀ (x : ↑K), ↑(f x) ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(k + 1))) : ∃ (g : C(↑K, ↑C)), f.HomotopicRel g {x : ↑K | ↑(f x) ∈ Topology.RelCWComplex.openCell k j}ᶜ ∧ ∀ (x : ↑K), ↑(f x) ∈ Topology.RelCWComplex.openCell k j → ↑(g x) ∈ Topology.RelCWComplex.cellFrontier k j

Pushing a map off a cell of higher dimension (Hatcher, Lemma 4.10 together with the radial push from the proof of Theorem 4.8). Let K be a compact subset of a real normed space of dimension less than k, and let f : K → C land in the k-skeleton skeletonLT C (k + 1). For every k-cell j, f is homotopic as a map into C, relative to the points that f does not send into the open cell j, to a map sending the points that f sends into the open cell j into its frontier.

theorem TauCeti.exists_homotopicRel_skeletonLT {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {k : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsCompact K) (hk : Module.finrank ℝ E < k) (f : C(↑K, ↑C)) (hf : ∀ (x : ↑K), ↑(f x) ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(k + 1))) : ∃ (g : C(↑K, ↑C)), f.HomotopicRel g {x : ↑K | ↑(f x) ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑k)} ∧ ∀ (x : ↑K), ↑(g x) ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑k)

Compressing a map of a low-dimensional compactum into the next lower skeleton. Let K be a compact subset of a real normed space of dimension less than k. Every map f : K → C landing in the k-skeleton skeletonLT C (k + 1) is homotopic as a map into C, relative to the points that f sends into the (k-1)-skeleton skeletonLT C k, to a map into skeletonLT C k.

theorem TauCeti.exists_homotopicRel_skeletonLT_finrank {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsCompact K) {n : ℕ} (hn : Module.finrank ℝ E ≤ n) (f : C(↑K, ↑C)) : ∃ (g : C(↑K, ↑C)), f.HomotopicRel g {x : ↑K | ↑(f x) ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))} ∧ ∀ (x : ↑K), ↑(g x) ∈ ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))

Compressing a map of a compactum into a skeleton of at least its dimension, the compression step of Hatcher's Corollary 4.12. Let K be a compact subset of a real normed space of dimension at most n. Every map f : K → C into the complex is homotopic as a map into C, relative to the points that f sends into the n-skeleton skeletonLT C (n + 1), to a map into skeletonLT C (n + 1).

theorem TauCeti.exists_joined_skeletonLT {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {A : Set X} (hA : ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1)) = A) (hAC : A ⊆ C) (x : ↑C) : ∃ (a : ↑A), Joined (Set.inclusion hAC a) x

Points of C are joined to the n-skeleton. If A is the n-skeleton skeletonLT C (n + 1) of a relative CW complex C, then every point of C is joined by a path in C to a point of A.

theorem TauCeti.exists_path_homotopic_skeletonLT {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {A : Set X} (hn : 0 < n) (hA : ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1)) = A) (hAC : A ⊆ C) {a b : ↑A} (γ : Path (Set.inclusion hAC a) (Set.inclusion hAC b)) : ∃ (γ' : Path a b), (γ'.map ⋯).Homotopic γ

Paths in C between points of the n-skeleton compress into it up to homotopy, for n ≥ 1. If A is the n-skeleton skeletonLT C (n + 1) of a relative CW complex C, then every path in C between two points of A is homotopic in C, relative to its endpoints, to a path in A. For n = 1 this says that the inclusion of the 1-skeleton is surjective on fundamental groups.

theorem TauCeti.joined_skeletonLT_iff {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {A : Set X} (hn : 0 < n) (hA : ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1)) = A) (hAC : A ⊆ C) {a b : ↑A} : Joined (Set.inclusion hAC a) (Set.inclusion hAC b) ↔ Joined a b

Paths in C between points of the n-skeleton compress into it, for n ≥ 1. If A is the n-skeleton skeletonLT C (n + 1) of a relative CW complex C, then two points of A are joined by a path in A exactly when they are joined by a path in C.