Maps of disk pairs and relative homotopy groups

The relative homotopy set π_{n+1}(Y, B, b) = TauCeti.RelHomotopyGroup (Fin n) _ is built from relative cubes: maps I × Iⁿ → Y sending the face {0} × Iⁿ into B and the rest of the boundary of the cube to b. The cells of a CW complex are instead attached along maps of pairs (Dⁿ⁺¹, Sⁿ) → (Y, B) that need not be constant on any part of the sphere. This file connects the two, and so states the compression lemma in its usual form (Hatcher, Lemma 4.6): if π_n(Y, B, b) = 0 for every b ∈ B and every n such that a relative CW complex (C, D) has n-cells, then every map (C, D) → (Y, B) is homotopic relative to D to a map into B (TauCeti.exists_homotopicRel_range_subset_of_relHomotopyGroup).

• A map of pairs g : (I × Iⁿ, ∂(I × Iⁿ)) → (Y, B) is homotopic, through maps of pairs, to a relative cube (TauCeti.exists_homotopicWith_relGenLoop). The open box {1} × Iⁿ ∪ I × ∂Iⁿ contracts to the centre of its top face; along the face {0} × Iⁿ, whose boundary lies in the open box, this contraction extends to a homotopy into B because ∂Iⁿ has the homotopy extension property in Iⁿ. The resulting homotopy of g on the boundary of the cube extends over the cube because that boundary has the homotopy extension property too (TauCeti.hasHomotopyExtensionProperty_prodBoundary).
• If π_{n+1}(Y, B, b) is trivial for every b ∈ B, every map of pairs (Dⁿ⁺¹, Sⁿ) → (Y, B) is homotopic relative to Sⁿ to a map into B (TauCeti.exists_homotopicRel_range_subset_of_subsingleton). Here Dⁿ⁺¹ and Sⁿ are the closed unit ball and the unit sphere of the sup norm on Fin (n + 1) → ℝ, the domains of the characteristic maps of Topology.RelCWComplex; they are the cube I × Iⁿ and its boundary. By the previous item and the triviality of the resulting relative cube, the map is homotopic through maps of pairs to a constant map with value in B, and sweeping that homotopy across the ball (ContinuousMap.HomotopicWith.exists_homotopicRel_range_subset) gives a homotopy relative to the sphere.

The hypothesis of the compression lemma for 0-cells is that every point of Y is joined by a path to a point of B, which is what π_0(Y, B, b) = 0 means; relative homotopy sets are only defined here in positive degrees.

Main declarations

• TauCeti.exists_homotopicWith_relGenLoop: a map of pairs out of the cube I × Iⁿ is homotopic through maps of pairs to a relative cube.
• TauCeti.exists_homotopyWith_relGenLoop_of_openBox: the same, by a homotopy that follows a prescribed contraction of the open box {1} × Iⁿ ∪ I × ∂Iⁿ, so that maps sharing a face of the cube can be deformed compatibly.
• TauCeti.exists_homotopicRel_range_subset_of_subsingleton: maps of disk pairs compress into B when the relative homotopy sets vanish.
• TauCeti.exists_homotopicRel_range_subset_of_relHomotopyGroup: the compression lemma, with its hypotheses on relative homotopy sets.

References

• A. Hatcher, Algebraic Topology, Section 4.1, Lemma 4.6 (the compression lemma) and the compression criterion preceding Theorem 4.3.

Deforming a map of pairs into a relative cube

theorem TauCeti.exists_homotopyWith_relGenLoop_of_openBox {N : Type v} [Finite N] {Y : TopCat} {B : Set ↑Y} (R : ↑unitInterval → ↑unitInterval × (N → ↑unitInterval) → ↑unitInterval × (N → ↑unitInterval)) (hR : Continuous fun (q : ↑unitInterval × ↑unitInterval × (N → ↑unitInterval)) => R q.1 q.2) (hR₀ : ∀ (z : ↑unitInterval × (N → ↑unitInterval)), R 0 z = z) (hRJ : ∀ {z : ↑unitInterval × (N → ↑unitInterval)}, z.1 = 1 ∨ z.2 ∈ Cube.boundary N → ∀ (t : ↑unitInterval), R t z ∈ Cube.prodBoundary N) {v : ↑unitInterval × (N → ↑unitInterval)} (hR₁ : ∀ {z : ↑unitInterval × (N → ↑unitInterval)}, z.1 = 1 ∨ z.2 ∈ Cube.boundary N → R 1 z = v) (g : C(↑unitInterval × (N → ↑unitInterval), ↑Y)) (hg : Set.MapsTo (⇑g) (Cube.prodBoundary N) B) : ∃ (b : ↑B), ↑b = g v ∧ ∃ (p : ↑(RelGenLoop N { pair := TopPair.ofSubset B, basepoint := b })) (G : g.HomotopyWith ↑p fun (f : C(↑unitInterval × (N → ↑unitInterval), ↑Y)) => Set.MapsTo (⇑f) (Cube.prodBoundary N) B), ∀ (t : ↑unitInterval) {z : ↑unitInterval × (N → ↑unitInterval)}, z.1 = 1 ∨ z.2 ∈ Cube.boundary N → G.toContinuousMap (t, z) = g (R t z)

A map of pairs is homotopic to a relative cube along a contraction of the open box. Let R be a deformation of the open box {1} × I^N ∪ I × ∂I^N of I × I^N inside the boundary of the cube, starting at the identity and ending at the constant map to a point v. Every map of pairs g : (I × I^N, ∂(I × I^N)) → (Y, B) is homotopic, through maps of pairs, to a relative cube at g v, by a homotopy that is g ∘ R t on the open box at every time t.

theorem TauCeti.exists_homotopicWith_relGenLoop {N : Type v} [Finite N] {Y : TopCat} {B : Set ↑Y} (g : C(↑unitInterval × (N → ↑unitInterval), ↑Y)) (hg : Set.MapsTo (⇑g) (Cube.prodBoundary N) B) : ∃ (b : ↑B), ↑b = g (1, cubeCenter) ∧ ∃ (p : ↑(RelGenLoop N { pair := TopPair.ofSubset B, basepoint := b })), g.HomotopicWith ↑p fun (f : C(↑unitInterval × (N → ↑unitInterval), ↑Y)) => Set.MapsTo (⇑f) (Cube.prodBoundary N) B

A map of pairs (I × I^N, ∂(I × I^N)) → (Y, B) is homotopic, through maps of pairs, to a relative cube. Its basepoint b ∈ B is the value of the given map at the centre of the face {1} × I^N.

Compressing maps of disk pairs

theorem TauCeti.exists_homotopicRel_range_subset_of_subsingleton {Y : TopCat} {B : Set ↑Y} {n : ℕ} (h : ∀ (b : ↑B), Subsingleton (RelHomotopyGroup (Fin n) { pair := TopPair.ofSubset B, basepoint := b })) (g : C(↑(Metric.closedBall 0 1), ↑Y)) (hg : Set.MapsTo ⇑g {x : ↑(Metric.closedBall 0 1) | ↑x ∈ Metric.sphere 0 1} B) : ∃ (g' : C(↑(Metric.closedBall 0 1), ↑Y)), g.HomotopicRel g' {x : ↑(Metric.closedBall 0 1) | ↑x ∈ Metric.sphere 0 1} ∧ Set.range ⇑g' ⊆ B

Compressing a map of disk pairs. Let B ⊆ Y be such that the relative homotopy set π_{n+1}(Y, B, b) is trivial for every b ∈ B. Then every map from the closed unit ball of the sup norm on Fin (n + 1) → ℝ to Y sending the unit sphere into B is homotopic, relative to the unit sphere, to a map with values in B.

The compression lemma

theorem TauCeti.exists_homotopicRel_range_subset_of_relHomotopyGroup {Y : TopCat} {B : Set ↑Y} {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] (h₀ : Nonempty (Topology.RelCWComplex.cell C 0) → ∀ (y : ↑Y), ∃ b ∈ B, Joined y b) (h : ∀ (n : ℕ), Nonempty (Topology.RelCWComplex.cell C (n + 1)) → ∀ (b : ↑B), Subsingleton (RelHomotopyGroup (Fin n) { pair := TopPair.ofSubset B, basepoint := b })) (f : C(↑C, ↑Y)) (hf : Set.MapsTo ⇑f {x : ↑C | ↑x ∈ D} B) : ∃ (g : C(↑C, ↑Y)), f.HomotopicRel g {x : ↑C | ↑x ∈ D} ∧ Set.range ⇑g ⊆ B

The compression lemma in terms of relative homotopy groups (Hatcher, Lemma 4.6). Let C be a relative CW complex with base D, and let B ⊆ Y. Suppose that every point of Y is joined by a path to a point of B if C has 0-cells, and that the relative homotopy set π_{n+1}(Y, B, b) is trivial for every b ∈ B if C has (n + 1)-cells. Then every map f : C → Y sending D into B is homotopic, relative to D, to a map into B.