The compression criterion

Let X = (X, A, a₀) be a based pair and let n be the cardinality of the index type N. This file proves the compression criterion for the relative homotopy set π_{n+1}(X, A, a₀): a relative cube p : I × I^N → X represents the distinguished class exactly when it is homotopic, relative to the boundary of the cube I × I^N, to a map with values in A (TauCeti.RelHomotopyGroup.mk_eq_default_iff). Consequently π_{n+1}(X, A, a₀) is trivial exactly when every relative cube can be compressed into A in this way (TauCeti.RelHomotopyGroup.subsingleton_iff).

The criterion turns vanishing of relative homotopy groups into deformations of maps of pairs into the subspace. Such deformations, for maps out of a closed ball, are the hypothesis of the compression lemma (TauCeti.exists_homotopicRel_range_subset) behind Whitehead's theorem. The criterion also gives exactness of the homotopy sequence of a pair at π_{n+1}(X, a₀).

Implementation notes

• A homotopy relative to the boundary of the cube keeps the face {0} × I^N inside A and the rest of the boundary at a₀, so it is a homotopy through relative cubes. A relative cube with values in A is trivial by TauCeti.RelGenLoop.homotopic_const_of_mem_range.
• Conversely, let F : I × (I × I^N) → X be a homotopy through relative cubes from p to the constant cube, and read its first two coordinates as a point (u, s) of a square. On the edge u = 0 it is p, on the edge s = 0 it takes values in A, and on the edges u = 1 and s = 1 it is constant at a₀. Sweeping the edge u = 0 across the square to the edge s = 0, keeping the corner (0, 0) fixed and the opposite endpoint on the edges u = 1 and s = 1, gives a homotopy relative to the boundary of the cube from p to the face of F in A.

Main declarations

• TauCeti.RelGenLoop.mapsTo_prodBoundary: a relative cube is a map of pairs (I × I^N, ∂(I × I^N)) → (X, A), and TauCeti.RelGenLoop.Homotopic.homotopicWith: a homotopy through relative cubes is a homotopy through maps of pairs.
• TauCeti.RelGenLoop.Homotopic.of_homotopicRel: relative cubes homotopic relative to the boundary of the cube are homotopic through relative cubes.
• TauCeti.RelGenLoop.exists_homotopicRel_of_homotopic_const: a relative cube homotopic through relative cubes to the constant cube is homotopic, relative to the boundary of the cube, to a map into A.
• TauCeti.RelHomotopyGroup.mk_eq_default_iff: the compression criterion.
• TauCeti.RelHomotopyGroup.subsingleton_iff: π_{n+1}(X, A, a₀) is trivial exactly when every relative cube compresses into A.
• TauCeti.RelHomotopyGroup.subsingleton_of_homotopyRel: π_{n+1}(X, A, a₀) is trivial when X deforms into A relative to A.

References

• A. Hatcher, Algebraic Topology, Section 4.1, the compression criterion preceding Theorem 4.3.

theorem TauCeti.RelGenLoop.mapsTo_prodBoundary {N : Type v} {X : BasedTopPair} {p : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)} (hp : p ∈ RelGenLoop N X) : Set.MapsTo (⇑p) (Cube.prodBoundary N) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map))

A relative cube of the based pair (X, A, a₀) is a map of pairs (I × I^N, ∂(I × I^N)) → (X, A).

theorem TauCeti.RelGenLoop.Homotopic.homotopicWith {N : Type v} {X : BasedTopPair} {p q : ↑(RelGenLoop N X)} (h : Homotopic p q) : (↑p).HomotopicWith ↑q fun (f : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)) => Set.MapsTo (⇑f) (Cube.prodBoundary N) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map))

A homotopy through relative cubes is a homotopy through maps of pairs (I × I^N, ∂(I × I^N)) → (X, A).

theorem TauCeti.RelGenLoop.Homotopic.of_homotopicRel {N : Type v} {X : BasedTopPair} {p q : ↑(RelGenLoop N X)} (h : (↑p).HomotopicRel (↑q) (Cube.prodBoundary N)) : Homotopic p q

Relative cubes that are homotopic relative to the boundary of the cube I × I^N are homotopic through relative cubes.

theorem TauCeti.RelGenLoop.homotopic_const_of_homotopicRel {N : Type v} {X : BasedTopPair} {p : ↑(RelGenLoop N X)} {q : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)} (h : (↑p).HomotopicRel q (Cube.prodBoundary N)) (hq : ∀ (y : ↑unitInterval × (N → ↑unitInterval)), q y ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) : Homotopic p const

A relative cube that is homotopic, relative to the boundary of the cube I × I^N, to a map with values in A is homotopic through relative cubes to the constant cube.

theorem TauCeti.RelGenLoop.exists_homotopicRel_of_homotopic_const {N : Type v} {X : BasedTopPair} {p : ↑(RelGenLoop N X)} (h : Homotopic p const) : ∃ (q : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)), (↑p).HomotopicRel q (Cube.prodBoundary N) ∧ ∀ (y : ↑unitInterval × (N → ↑unitInterval)), q y ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)

A relative cube that is homotopic through relative cubes to the constant cube is homotopic, relative to the boundary of the cube I × I^N, to a map with values in A.

theorem TauCeti.RelHomotopyGroup.mk_eq_default_iff {N : Type v} {X : BasedTopPair} {p : ↑(RelGenLoop N X)} : mk p = default ↔ ∃ (q : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)), (↑p).HomotopicRel q (Cube.prodBoundary N) ∧ ∀ (y : ↑unitInterval × (N → ↑unitInterval)), q y ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)

The compression criterion (Hatcher, Section 4.1). A relative cube represents the distinguished class of π_{n+1}(X, A, a₀) exactly when it is homotopic, relative to the boundary of the cube I × I^N, to a map with values in A.

theorem TauCeti.RelHomotopyGroup.subsingleton_iff {N : Type v} {X : BasedTopPair} : Subsingleton (RelHomotopyGroup N X) ↔ ∀ (p : ↑(RelGenLoop N X)), ∃ (q : C(↑unitInterval × (N → ↑unitInterval), ↑TopPair.fst)), (↑p).HomotopicRel q (Cube.prodBoundary N) ∧ ∀ (y : ↑unitInterval × (N → ↑unitInterval)), q y ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)

The relative homotopy set π_{n+1}(X, A, a₀) is trivial exactly when every relative cube is homotopic, relative to the boundary of the cube I × I^N, to a map with values in A.

theorem TauCeti.RelHomotopyGroup.subsingleton_of_homotopyRel {N : Type v} {X : BasedTopPair} {g : C(↑TopPair.fst, ↑TopPair.fst)} (H : (ContinuousMap.id ↑TopPair.fst).HomotopyRel g (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map))) (hg : ∀ (x : ↑TopPair.fst), g x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map)) : Subsingleton (RelHomotopyGroup N X)

A deformation into the subspace kills the relative homotopy sets. If the identity of X is homotopic, relative to A, to a map g with values in A, then π_{n+1}(X, A, a₀) is trivial: composing a relative cube with the homotopy compresses it into A.