Deforming singular cubes into a subspace

Let A be a subset of a space X and let n ∈ ℕ∞. Suppose that A is compressible in X below dimension n, in the sense of Hatcher's compression lemma: every singular cube c : Iᵐ → X with m < n sending the boundary of the cube into A is homotopic, relative to that boundary, to a cube with values in A. For m = 0 the boundary is empty, so this says that every point of X is joined by a path to a point of A.

This file shows that the singular cubes of X then deform coherently, into A below dimension n: there is a TauCeti.SubspaceCubeDeformation A n, a homotopy of each singular cube c starting at c, ending at a cube with values in A when the dimension of c is less than n, such that

• the homotopy of a face of c is the restriction of the homotopy of c to that face;
• the homotopy of a cube not depending on a coordinate does not depend on it either;
• the homotopy of a cube with values in A is constant.

For n = ⊤ every singular cube deforms into A. Conversely such a deformation compresses every cube of dimension less than n whose boundary lies in A, relative to the boundary, so it exists exactly when A is compressible in X below dimension n (TauCeti.nonempty_subspaceCubeDeformation_iff). By the compression lemma for disks, A is compressible below dimension n as soon as every point of X is joined by a path to A and the relative homotopy sets π_{k+1}(X, A, a) are trivial for every k + 1 < n and every a ∈ A (TauCeti.nonempty_subspaceCubeDeformation_of_relHomotopyGroup). For n = ⊤ this is the case for the bottom face of the mapping cylinder of a weak homotopy equivalence.

The three properties above are what the prism operators of the homotopies need to deform the normalized cubical chains of X by a map chain homotopic to the identity, in the same way as TauCeti.BasedCubeDeformation retracts them onto the based cubes. For n = ⊤ this retracts them onto the chains of A; applied to the mapping cylinder, this is the input for the invariance of singular homology under weak homotopy equivalences (Hatcher, Proposition 4.21). For finite n it shows that the relative homology of (X, A) vanishes below degree n.

Construction

The homotopies are built by induction on the dimension of the cubes. The homotopy of a cube with values in A is constant, and that of a degenerate cube is read off one of its faces. For any other (m + 1)-cube c, the homotopies of the faces of c agree where two faces meet, so they glue to a homotopy of the restriction of c to the boundary of the cube, and the homotopy extension property of the boundary (TauCeti.hasHomotopyExtensionProperty_cubeBoundary) extends it to a homotopy of c. If m + 1 < n, the boundary homotopy has reached its end, with values in A, by some time a; at that time the extension is a cube with boundary in A, which is then compressed into A relative to the boundary. To leave room for these compressions, the homotopies of cubes of dimension k < n are stationary from the time (k + 1) / (k + 2) on. The gluing of the face homotopies, the homotopies of degenerate cubes and the coherence of each new dimension come from TauCeti.CoherentCubeHomotopies.

Main definitions and results

• TauCeti.SubspaceCubeDeformation: a coherent deformation of all singular cubes, into A below dimension n.
• TauCeti.subspaceCubeDeformation: such a deformation when A is compressible in X below dimension n.
• TauCeti.SubspaceCubeDeformation.homotopicRel: such a deformation deforms each cube with boundary in A relative to the boundary.
• TauCeti.nonempty_subspaceCubeDeformation_iff: such a deformation exists exactly when A is compressible in X below dimension n.
• TauCeti.SingularCube.exists_homotopicRel_range_subset_of_subsingleton: a singular cube with boundary in A compresses into A when the relative homotopy sets in its dimension vanish.
• TauCeti.nonempty_subspaceCubeDeformation_of_relHomotopyGroup: the deformation exists when the relative homotopy sets vanish below dimension n.

References

• S. Eilenberg, Singular homology theory, Ann. of Math. (2) 45 (1944), 407–447, for the deformation of singular chains into the subcomplex of a subspace.
• A. Hatcher, Algebraic Topology, Section 4.1, Lemma 4.6 (the compression lemma) and Proposition 4.21 (a weak homotopy equivalence induces isomorphisms on homology).
• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II, for singular cubes and their degeneracies.

Extending the deformation over a single cube

Deforming all cubes of one dimension

The deformation

structure TauCeti.SubspaceCubeDeformation {X : Type u_1} [TopologicalSpace X] (A : Set X) (n : ℕ∞) : Type u_1

A deformation of the singular cubes of X into A below dimension n: a homotopy of every singular cube c, with time as the first coordinate, starting at c, and ending at a cube with values in A when the dimension of c is less than n. The homotopies are compatible with faces and degeneracies, and fix the cubes that already have values in A. For n = ⊤ every cube deforms into A.

• homotopy {m : ℕ} (c : SingularCube X m) : C(↑unitInterval × (Fin m → ↑unitInterval), X)

  The homotopy deforming the singular cube c.

• homotopy_zero {m : ℕ} (c : SingularCube X m) (y : Fin m → ↑unitInterval) : (self.homotopy c) (0, y) = c y

  The homotopy of c starts at c.

• homotopy_one_mem {m : ℕ} (hm : ↑m < n) (c : SingularCube X m) (y : Fin m → ↑unitInterval) : (self.homotopy c) (1, y) ∈ A

  The homotopy of a cube of dimension less than n ends at a cube with values in A.

• homotopy_insertNth {m : ℕ} (c : SingularCube X (m + 1)) (i : Fin (m + 1)) {t : ↑unitInterval} (ht : t = 0 ∨ t = 1) (s : ↑unitInterval) (z : Fin m → ↑unitInterval) : (self.homotopy c) (s, i.insertNth t z) = (self.homotopy (SingularCube.face i t c)) (s, z)

  The homotopy of a face of c is the restriction of the homotopy of c to that face.

• isDegenerateAt_curry {m : ℕ} {c : SingularCube X m} {i : Fin m} (hc : c.IsDegenerateAt i) (s : ↑unitInterval) : SingularCube.IsDegenerateAt ((self.homotopy c).curry s) i

  If c does not depend on a coordinate, then neither does its homotopy at any time.

• homotopy_of_range_subset {m : ℕ} {c : SingularCube X m} (hc : Set.range ⇑c ⊆ A) (s : ↑unitInterval) (y : Fin m → ↑unitInterval) : (self.homotopy c) (s, y) = c y

  The homotopy of a cube with values in A is constant.

noncomputable def TauCeti.subspaceCubeDeformation {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (hA : ∀ (m : ℕ), ↑m < n → ∀ (c : SingularCube X m), Set.MapsTo (⇑c) (Cube.boundary (Fin m)) A → ∃ (c' : SingularCube X m), ContinuousMap.HomotopicRel c c' (Cube.boundary (Fin m)) ∧ Set.range ⇑c' ⊆ A) : SubspaceCubeDeformation A n

Below dimension n, the singular cubes deform into a compressible subspace. If every singular cube of X of dimension less than n with boundary in A is homotopic, relative to the boundary of the cube, to a cube with values in A, then there is a deformation of the singular cubes of X into A below dimension n, compatible with faces and degeneracies and fixing the cubes with values in A.

theorem TauCeti.SubspaceCubeDeformation.homotopicRel {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} (D : SubspaceCubeDeformation A n) {m : ℕ} {c : SingularCube X m} (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin m)) A) : ContinuousMap.HomotopicRel c ((D.homotopy c).curry 1) (Cube.boundary (Fin m))

The homotopy of a cube with boundary in A is relative to the boundary of the cube. Below dimension n it ends at a cube with values in A, so it compresses the cube into A.

theorem TauCeti.nonempty_subspaceCubeDeformation_iff {X : Type u_1} [TopologicalSpace X] {A : Set X} {n : ℕ∞} : Nonempty (SubspaceCubeDeformation A n) ↔ ∀ (m : ℕ), ↑m < n → ∀ (c : SingularCube X m), Set.MapsTo (⇑c) (Cube.boundary (Fin m)) A → ∃ (c' : SingularCube X m), ContinuousMap.HomotopicRel c c' (Cube.boundary (Fin m)) ∧ Set.range ⇑c' ⊆ A

The singular cubes of X deform into A below dimension n exactly when A is compressible in X below dimension n: when every singular cube of dimension less than n with boundary in A is homotopic, relative to the boundary of the cube, to a cube with values in A.

Compressibility from relative homotopy groups

theorem TauCeti.SingularCube.exists_homotopicRel_range_subset_of_subsingleton {X : TopCat} {A : Set ↑X} {n : ℕ} (h : ∀ (a : ↑A), Subsingleton (RelHomotopyGroup (Fin n) { pair := TopPair.ofSubset A, basepoint := a })) (c : SingularCube (↑X) (n + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (n + 1))) A) : ∃ (c' : SingularCube (↑X) (n + 1)), ContinuousMap.HomotopicRel c c' (Cube.boundary (Fin (n + 1))) ∧ Set.range ⇑c' ⊆ A

Compressing a singular cube. Let A ⊆ X be such that the relative homotopy set π_{n+1}(X, A, a) is trivial for every a ∈ A. Then every singular (n + 1)-cube of X sending the boundary of the cube into A is homotopic, relative to that boundary, to a cube with values in A.

theorem TauCeti.nonempty_subspaceCubeDeformation_of_relHomotopyGroup {n : ℕ∞} {X : TopCat} {A : Set ↑X} (h₀ : ∀ (x : ↑X), ∃ a ∈ A, Joined x a) (h : ∀ (k : ℕ), ↑(k + 1) < n → ∀ (a : ↑A), Subsingleton (RelHomotopyGroup (Fin k) { pair := TopPair.ofSubset A, basepoint := a })) : Nonempty (SubspaceCubeDeformation A n)

The singular cubes deform into A below dimension n when the relative homotopy sets vanish below n. If every point of X is joined by a path to a point of A, and the relative homotopy set π_{k+1}(X, A, a) is trivial for every k + 1 < n and every a ∈ A, then there is a deformation of the singular cubes of X into A below dimension n.