Lifting from zero-set strong deformation retracts

Let A ⊆ Y be the zero set of a continuous u : Y → I and a strong deformation retract of Y. A map with homotopy lifting for Y has the right lifting property against the inclusion A → Y: a compatible lift on A extends to Y, with its prescribed values retained exactly.

Writing h for the deformation, the homotopy (t, y) ↦ h (1 - min 1 (t / u y), y) runs from the retraction to y by time u y. Its continuity at A follows from the compactness argument ContinuousMap.continuous_apply_prodMk_of_fixed. Evaluating an ordinary homotopy lift at time u y gives the extension. No regular lifting function or separation hypothesis is needed.

References

• A. Strøm, Note on cofibrations II, Math. Scand. 22 (1968), 130–142.
• J. P. May, A Concise Course in Algebraic Topology, Chapters 6 and 7.

theorem TauCeti.HasHomotopyLiftingProperty.zeroSetSDR_liftingInclusion {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {Y : Type w} [TopologicalSpace Y] (hp : HasHomotopyLiftingProperty p Y) {A : Set Y} (u : C(Y, ↑unitInterval)) (hu : ∀ (y : Y), u y = 0 ↔ y ∈ A) (r : C(Y, ↑A)) (hr : (ContinuousMap.id Y).HomotopicRel ((ContinuousMap.subtypeVal A).comp r) A) (f : C(↑A, E)) (g : C(Y, B)) (hfg : ∀ (a : ↑A), p (f a) = g ↑a) : ∃ (ℓ : C(Y, E)), p ∘ ⇑ℓ = ⇑g ∧ ∀ (a : ↑A), ℓ ↑a = f a

Fixed-data relative lifting. Let A ⊆ Y be the zero set of a continuous u : Y → I and a strong deformation retract of Y, with retraction r. Then a map p with homotopy lifting for Y lifts every commutative square from the inclusion A → Y to p: given f : A → E and g : Y → B with p ∘ f = g on A, there is a lift ℓ : Y → E of g restricting to f on A.