Homotoping a map off a point of a higher-dimensional chart

Let D be a closed subset of a finite-dimensional real normed space E, let Y be a Hausdorff space, and let φ be a chart of Y with values in a finite-dimensional real normed space F whose target contains a ball B = ball c r. If dim E < dim F, then every map f : D → Y is homotopic, relative to the points that f sends outside φ⁻¹(B), to a map that misses a point of φ⁻¹(B).

This is the key lemma behind cellular approximation, where D is a cube or a disk, Y is a complex Z ∪ eⁿ with a cell attached, and φ is the inverse of the characteristic map on the open cell. Hatcher's proof approximates f by a map that is linear on the simplices of a fine subdivision. Here the approximation is differentiable instead:

• by the Tietze extension theorem, φ ∘ f restricted to the closed set of points sent into φ⁻¹(closedBall c (r / 2)) extends to a continuous map E → F, which Mathlib approximates uniformly within r / 8 by a differentiable map G : E → F (Continuous.exists_contDiff_approx);
• since dim E < dim F, the complement of the range of G is dense (Differentiable.dense_compl_range_of_finrank_lt_finrank), so some point p of ball c (r / 8) is not a value of G;
• a bump function (ContDiffBump) equal to 1 on closedBall c (r / 4) and supported in ball c (r / 2) interpolates between φ ∘ f and G. The interpolated map agrees with G, hence avoids p, where φ ∘ f lies in closedBall c (r / 4), and moves φ ∘ f by less than r / 8 elsewhere, hence also avoids p there;
• the straight-line homotopy in the chart from φ ∘ f to the interpolated map stays in ball c r and is stationary wherever the bump function vanishes, so it glues with the constant homotopy outside the chart (ContinuousMap.exists_homotopyRel_of_segment_subset_target).

Main results

• ContinuousMap.exists_homotopyRel_of_segment_subset_target: a map can be moved along straight lines in a chart, relative to the points that do not move, provided the closure of the moving points stays in the chart.
• ContinuousMap.exists_homotopyRel_notMem_range: a map from a closed subset of a space of smaller dimension is homotopic, relative to the preimage of the complement of φ⁻¹(B), to a map missing a point of φ⁻¹(B) and still sending the points sent into the chart into the chart.

References

• A. Hatcher, Algebraic Topology, Section 4.1, Lemma 4.10.

theorem ContinuousMap.exists_homotopyRel_of_segment_subset_target {X : Type u_1} {Y : Type u_2} {F : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (f : C(X, Y)) (φ : OpenPartialHomeomorph Y F) {w : X → F} (hw : ContinuousOn w (⇑f ⁻¹' φ.source)) (hclosure : closure {x : X | f x ∈ φ.source ∧ w x ≠ ↑φ (f x)} ⊆ ⇑f ⁻¹' φ.source) (hseg : ∀ (x : X), f x ∈ φ.source → segment ℝ (↑φ (f x)) (w x) ⊆ φ.target) {S : Set X} (hS : ∀ x ∈ S, f x ∈ φ.source → w x = ↑φ (f x)) : ∃ (g : C(X, Y)), (∀ (x : X), f x ∈ φ.source → g x = ↑φ.symm (w x)) ∧ (∀ (x : X), f x ∉ φ.source → g x = f x) ∧ Nonempty (f.HomotopyRel g S)

Straight-line homotopy inside a chart. Let φ be a chart of Y with values in a real topological vector space, and let w assign a new chart value, continuously, to each point that f sends into the chart, so that the segment from φ (f x) to w x stays in the target. If the closure of the set of points that actually move stays inside f ⁻¹' φ.source, then f is homotopic, relative to any set of points that do not move, to the map equal to φ.symm ∘ w on f ⁻¹' φ.source and to f elsewhere.

theorem ContinuousMap.exists_homotopyRel_notMem_range {E : Type u_1} {F : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace Y] [T2Space Y] {D : Set E} (f : C(↑D, Y)) (hD : IsClosed D) (hEF : Module.finrank ℝ E < Module.finrank ℝ F) (φ : OpenPartialHomeomorph Y F) {c : F} {r : ℝ} (hr : 0 < r) (hφ : Metric.ball c r ⊆ φ.target) : ∃ (g : C(↑D, Y)), Nonempty (f.HomotopyRel g (⇑f ⁻¹' ↑φ.symm '' Metric.ball c r)ᶜ) ∧ (∀ (x : ↑D), f x ∈ φ.source → g x ∈ φ.source) ∧ ∃ p ∈ Metric.ball c r, ↑φ.symm p ∉ Set.range ⇑g

Homotoping a map off a point of a higher-dimensional chart (Hatcher, Lemma 4.10). Let D be a closed subset of E, and let φ be a chart of the Hausdorff space Y into F whose target contains ball c r. If dim E < dim F, then every map f : D → Y is homotopic, relative to the points that f does not send into φ.symm '' ball c r, to a map g missing the point φ.symm p for some p ∈ ball c r. The map g sends the points that f sends into the chart into the chart.