The homotopy extension property

A subset A of a topological space X has the homotopy extension property when a homotopy of maps out of A can be extended over X as soon as its initial map extends: given f : C(X, Y) and H : C(I × A, Y) with H (0, a) = f a for every a ∈ A, there is a homotopy G : C(I × X, Y) with G (0, x) = f x and G (t, a) = H (t, a). In this situation the inclusion of A into X is a cofibration, and it is a closed cofibration as soon as X is Hausdorff, because the property then forces A to be closed.

For closed A the property is equivalent to a purely geometric statement: the subspace {0} × X ∪ I × A of the cylinder I × X is a retract of the whole cylinder. This is how the property is verified in practice, and it is also what frees it from the universe the target space Y is taken in: the definition below quantifies over targets in the universe of X, and TauCeti.HasHomotopyExtensionProperty.exists_extension_of_isClosed upgrades a closed subset with that property to one that extends homotopies with values in a space in any universe.

Main declarations

• TauCeti.cylinderExtensionDomain: the subspace {0} × X ∪ I × A of the cylinder I × X, the domain of the initial data of a homotopy extension problem.
• TauCeti.HasHomotopyExtensionProperty: the homotopy extension property of a subset, together with TauCeti.hasHomotopyExtensionProperty_iff and TauCeti.HasHomotopyExtensionProperty.exists_extension restating it.
• TauCeti.hasHomotopyExtensionProperty_iff_exists_retraction: a closed subset has the homotopy extension property exactly when {0} × X ∪ I × A is a retract of I × X.
• TauCeti.HasHomotopyExtensionProperty.exists_extension_of_isClosed and TauCeti.HasHomotopyExtensionProperty.exists_homotopy_of_restrict: for a closed subset, extension of homotopies with values in a space in an arbitrary universe, in terms of raw maps and of Mathlib's bundled homotopies.
• IsClopen.hasHomotopyExtensionProperty: a clopen subset has the homotopy extension property.
• TauCeti.HasHomotopyExtensionProperty.isClosed: in a Hausdorff space the property forces the subset to be closed, so the inclusion is a closed cofibration.
• TauCeti.HasHomotopyExtensionProperty.image and TauCeti.HasHomotopyExtensionProperty.image_of_isClosed: transport of the property along a homeomorphism, inside one universe and, for a closed subset, across universes.
• TauCeti.HasHomotopyExtensionProperty.homotopicRel_of_retracing: a homotopy followed by a homotopy which retraces it at the points of a subset with the homotopy extension property can be replaced by a homotopy relative to that subset.
• TauCeti.HasHomotopyExtensionProperty.exists_homotopy_apply_eq_of_trans_refl: a homotopy which at the points of such a subset runs through a given homotopy and then stays put can be replaced by one which is exactly the given homotopy there.

References

• A. Hatcher, Algebraic Topology, Chapter 0, the section "The Homotopy Extension Property": the retraction criterion and the closedness of a subset with the property in a Hausdorff space are the unnumbered discussion opening that section.
• G. W. Whitehead, Elements of Homotopy Theory, Chapter I.

def TauCeti.cylinderExtensionDomain {X : Type u} (A : Set X) : Set (↑unitInterval × X)

The subspace {0} × X ∪ I × A of the cylinder I × X: the bottom of the cylinder together with the part of the cylinder lying over A. For closed A, a homotopy extension problem for A ⊆ X is exactly the problem of extending a map defined on this subspace over the whole cylinder; the closedness is what lets the two pieces of initial data be glued into a single continuous map on the union.

@[simp]

theorem TauCeti.mem_cylinderExtensionDomain_iff {X : Type u} {A : Set X} {p : ↑unitInterval × X} : p ∈ cylinderExtensionDomain A ↔ p.1 = 0 ∨ p.2 ∈ A

theorem TauCeti.zero_mem_cylinderExtensionDomain {X : Type u} {A : Set X} (x : X) : (0, x) ∈ cylinderExtensionDomain A

theorem TauCeti.mem_cylinderExtensionDomain_of_mem {X : Type u} {A : Set X} {t : ↑unitInterval} {x : X} (hx : x ∈ A) : (t, x) ∈ cylinderExtensionDomain A

theorem TauCeti.isClosed_cylinderExtensionDomain {X : Type u} {A : Set X} [TopologicalSpace X] (hA : IsClosed A) : IsClosed (cylinderExtensionDomain A)

def TauCeti.HasHomotopyExtensionProperty {X : Type u} [TopologicalSpace X] (A : Set X) : Prop

A subset A of X has the homotopy extension property when every homotopy of maps out of A whose initial map extends to X is itself the restriction of a homotopy of maps out of X.

Only targets Y in the universe of X are quantified over here. For a closed subset this is no restriction: TauCeti.HasHomotopyExtensionProperty.exists_extension_of_isClosed then extends homotopies with values in a space in an arbitrary universe.

theorem TauCeti.hasHomotopyExtensionProperty_iff {X : Type u} {A : Set X} [TopologicalSpace X] : HasHomotopyExtensionProperty A ↔ ∀ {Y : Type u} [inst : TopologicalSpace Y] (f : C(X, Y)) (H : C(↑unitInterval × ↑A, Y)), (∀ (a : ↑A), H (0, a) = f ↑a) → ∃ (G : C(↑unitInterval × X, Y)), (∀ (x : X), G (0, x) = f x) ∧ ∀ (t : ↑unitInterval) (a : ↑A), G (t, ↑a) = H (t, a)

Unfolding of TauCeti.HasHomotopyExtensionProperty, so that the property can be proved and used in modules that only import this one.

theorem TauCeti.hasHomotopyExtensionProperty_empty {X : Type u} [TopologicalSpace X] : HasHomotopyExtensionProperty ∅

The empty subset has the homotopy extension property: a homotopy out of ∅ imposes nothing, and the constant homotopy extends the initial map.

theorem TauCeti.HasHomotopyExtensionProperty.exists_extension {X : Type u} {A : Set X} [TopologicalSpace X] (h : HasHomotopyExtensionProperty A) {Y : Type u} [TopologicalSpace Y] (f : C(X, Y)) (H : C(↑unitInterval × ↑A, Y)) (hH : ∀ (a : ↑A), H (0, a) = f ↑a) : ∃ (G : C(↑unitInterval × X, Y)), (∀ (x : X), G (0, x) = f x) ∧ ∀ (t : ↑unitInterval) (a : ↑A), G (t, ↑a) = H (t, a)

The defining consequence of the homotopy extension property: a homotopy out of A whose initial map extends to X extends to a homotopy out of X.

theorem TauCeti.exists_homotopy_extension_of_retraction {X : Type u} {A : Set X} [TopologicalSpace X] {Y : Type v} [TopologicalSpace Y] (hA : IsClosed A) {r : C(↑unitInterval × X, ↑unitInterval × X)} (hr : ∀ (p : ↑unitInterval × X), r p ∈ cylinderExtensionDomain A) (hr' : ∀ p ∈ cylinderExtensionDomain A, r p = p) (f : C(X, Y)) (H : C(↑unitInterval × ↑A, Y)) (hH : ∀ (a : ↑A), H (0, a) = f ↑a) : ∃ (G : C(↑unitInterval × X, Y)), (∀ (x : X), G (0, x) = f x) ∧ ∀ (t : ↑unitInterval) (a : ↑A), G (t, ↑a) = H (t, a)

A retraction of the cylinder I × X onto {0} × X ∪ I × A solves every homotopy extension problem for a closed subset A ⊆ X, with values in a space in any universe.

theorem TauCeti.hasHomotopyExtensionProperty_of_retraction {X : Type u} {A : Set X} [TopologicalSpace X] (hA : IsClosed A) {r : C(↑unitInterval × X, ↑unitInterval × X)} (hr : ∀ (p : ↑unitInterval × X), r p ∈ cylinderExtensionDomain A) (hr' : ∀ p ∈ cylinderExtensionDomain A, r p = p) : HasHomotopyExtensionProperty A

A closed subset onto whose cylinder extension domain the cylinder retracts has the homotopy extension property.

theorem IsClopen.hasHomotopyExtensionProperty {X : Type u} {A : Set X} [TopologicalSpace X] (hA : IsClopen A) : TauCeti.HasHomotopyExtensionProperty A

A clopen subset has the homotopy extension property: the cylinder retracts onto {0} × X ∪ I × A by fixing the part over A and collapsing the part over the complement of A to the bottom of the cylinder.

theorem TauCeti.HasHomotopyExtensionProperty.exists_retraction {X : Type u} {A : Set X} [TopologicalSpace X] (h : HasHomotopyExtensionProperty A) : ∃ (r : C(↑unitInterval × X, ↑unitInterval × X)), (∀ (p : ↑unitInterval × X), r p ∈ cylinderExtensionDomain A) ∧ ∀ p ∈ cylinderExtensionDomain A, r p = p

Solving the universal homotopy extension problem, the one whose target is the subspace {0} × X ∪ I × A itself, produces a retraction of the cylinder onto that subspace.

theorem TauCeti.hasHomotopyExtensionProperty_iff_exists_retraction {X : Type u} {A : Set X} [TopologicalSpace X] (hA : IsClosed A) : HasHomotopyExtensionProperty A ↔ ∃ (r : C(↑unitInterval × X, ↑unitInterval × X)), (∀ (p : ↑unitInterval × X), r p ∈ cylinderExtensionDomain A) ∧ ∀ p ∈ cylinderExtensionDomain A, r p = p

A closed subset has the homotopy extension property exactly when the subspace {0} × X ∪ I × A is a retract of the cylinder I × X.

theorem TauCeti.HasHomotopyExtensionProperty.exists_extension_of_isClosed {X : Type u} {A : Set X} [TopologicalSpace X] (hA : IsClosed A) (h : HasHomotopyExtensionProperty A) {Y : Type v} [TopologicalSpace Y] (f : C(X, Y)) (H : C(↑unitInterval × ↑A, Y)) (hH : ∀ (a : ↑A), H (0, a) = f ↑a) : ∃ (G : C(↑unitInterval × X, Y)), (∀ (x : X), G (0, x) = f x) ∧ ∀ (t : ↑unitInterval) (a : ↑A), G (t, ↑a) = H (t, a)

For a closed subset, the homotopy extension property extends homotopies with values in a space in an arbitrary universe, not only in the universe of X. The closedness hypothesis is what routes the argument through the retraction characterisation, which is universe-free.

theorem TauCeti.HasHomotopyExtensionProperty.exists_homotopy_of_restrict {X : Type u} {A : Set X} [TopologicalSpace X] (hA : IsClosed A) (h : HasHomotopyExtensionProperty A) {Y : Type v} [TopologicalSpace Y] (f : C(X, Y)) {g : C(↑A, Y)} (H : (ContinuousMap.restrict A f).Homotopy g) : ∃ (f' : C(X, Y)) (G : f.Homotopy f'), ∀ (t : ↑unitInterval) (a : ↑A), G (t, ↑a) = H (t, a)

For a closed subset, the homotopy extension property in terms of bundled homotopies: a homotopy starting at the restriction of f : C(X, Y) to A is the restriction of a homotopy starting at f. As in TauCeti.HasHomotopyExtensionProperty.exists_extension_of_isClosed, closedness lets Y live in any universe.

theorem TauCeti.HasHomotopyExtensionProperty.isClosed {X : Type u} {A : Set X} [TopologicalSpace X] [T2Space X] (h : HasHomotopyExtensionProperty A) : IsClosed A

In a Hausdorff space, a subset with the homotopy extension property is closed, so the inclusion of such a subset is a closed cofibration.

theorem TauCeti.HasHomotopyExtensionProperty.image {X : Type u} {A : Set X} [TopologicalSpace X] {X' : Type u} [TopologicalSpace X'] (h : HasHomotopyExtensionProperty A) (e : X ≃ₜ X') : HasHomotopyExtensionProperty (⇑e '' A)

The homotopy extension property transports along a homeomorphism onto a space in the same universe, with no hypothesis on A: a homotopy extension problem for e '' A is carried back along e to one for A, and its solution carried forward again.

theorem TauCeti.HasHomotopyExtensionProperty.image_of_isClosed {X : Type u} {A : Set X} [TopologicalSpace X] {X' : Type u'} [TopologicalSpace X'] (h : HasHomotopyExtensionProperty A) (e : X ≃ₜ X') (hA : IsClosed A) : HasHomotopyExtensionProperty (⇑e '' A)

For a closed subset, the homotopy extension property transports along a homeomorphism onto a space in an arbitrary universe. Closedness enters because the cross-universe transport goes through the retraction characterisation; for a homeomorphism inside one universe, TauCeti.HasHomotopyExtensionProperty.image needs no hypothesis on A.

theorem TauCeti.HasHomotopyExtensionProperty.homotopicRel_of_retracing {X : Type u} {A : Set X} [TopologicalSpace X] {Y : Type u} [TopologicalSpace Y] {f₀ f₁ f₂ : C(X, Y)} (hA : HasHomotopyExtensionProperty A) (F : f₀.Homotopy f₁) (G : f₁.Homotopy f₂) (hG : ∀ (t : ↑unitInterval), ∀ x ∈ A, G (t, x) = F (unitInterval.symm t, x)) : f₀.HomotopicRel f₂ A

A homotopy which retraces itself on A can be made stationary on A. Let F be a homotopy from f₀ to f₁, and G a homotopy from f₁ to f₂ which, at every point of a subset A with the homotopy extension property, runs backwards along F. Then f₀ and f₂ are homotopic relative to A.

theorem TauCeti.HasHomotopyExtensionProperty.exists_homotopy_apply_eq_of_trans_refl {X : Type u} {A : Set X} [TopologicalSpace X] {Y : Type u} [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (hA : HasHomotopyExtensionProperty A) (F : f₀.Homotopy f₁) (G : (f₀.comp (ContinuousMap.subtypeVal A)).Homotopy (f₁.comp (ContinuousMap.subtypeVal A))) (hF : ∀ (t : ↑unitInterval) (a : ↑A), F (t, ↑a) = (G.trans (ContinuousMap.Homotopy.refl (f₁.comp (ContinuousMap.subtypeVal A)))) (t, a)) : ∃ (F' : f₀.Homotopy f₁), ∀ (t : ↑unitInterval) (a : ↑A), F' (t, ↑a) = G (t, a)

Removing a stationary tail on A. Let F be a homotopy from f₀ to f₁, and G a homotopy between the restrictions of f₀ and f₁ to a subset A with the homotopy extension property. If at every point of A the homotopy F runs through G at double speed and then stays put, that is, F is G.trans (Homotopy.refl _) on A, then some homotopy from f₀ to f₁ is exactly G on A.