NDR pairs

An NDR pair (neighbourhood deformation retract pair) (X, A) consists of a subset A ⊆ X presented by explicit data: a control function u : X → I whose zero set is exactly A, and a deformation H : I × X → X starting at the identity, fixing A pointwise, and carrying every point with u x < 1 into A at time 1.

For an NDR pair, the bottom-and-sides subspace J = {0} × X ∪ I × A of the cylinder I × X (TauCeti.cylinderExtensionDomain A) is again the zero set of an explicit control function, (t, x) ↦ t * u x, and is a strong deformation retract of the cylinder by the explicit deformation (s, t, x) ↦ (t - s * min t (u x), H (s * min 1 (t / u x), x)). At time 1 every point of the cylinder lands in J, including the corner case u x = t = 1. Consequently A has the homotopy extension property, and the pair (I × X, J) satisfies the hypotheses of the fixed-data relative lifting theorem for Hurewicz fibrations (TauCeti.HasHomotopyLiftingProperty.zeroSetSDR_liftingInclusion).

Continuity of the deformation along the zero set, where the formula divides by zero, rests on the compactness argument ContinuousMap.continuous_apply_prodMk_of_fixed.

Conversely, a closed subset with the homotopy extension property carries NDR data (Strøm): if r retracts the cylinder onto J, its second coordinate is a deformation, and x ↦ ⨆ t, t - (r (t, x)).1, the largest amount by which r lowers a point over x, is a control function (TauCeti.NDRPair.ofRetraction). So the closed cofibrations are exactly the subsets admitting NDR data (TauCeti.nonempty_ndrPair_iff). NDR pairs (X, A) and (Y, B) have a product (X × Y, A × Y ∪ X × B) (TauCeti.NDRPair.prod, following Steenrod and May), with control the minimum of the two controls; this gives Strøm's product theorem for closed cofibrations.

NDR data usually comes from a neighbourhood U of A that deformation retracts onto A relative to A, together with a function f : X → I vanishing exactly on A and less than one only on U. TauCeti.NDRPair.ofHomotopyRel cuts the deformation off where 3 / 4 ≤ f, so that it extends by the identity to all of X, and takes min 1 (2 f) as control function.

Main declarations

• TauCeti.NDRPair A: NDR data for A ⊆ X.
• TauCeti.NDRPair.cylinderControl: the control function (t, x) ↦ t * u x of J.
• TauCeti.NDRPair.cylinderDeformation: the deformation of the cylinder onto J, with TauCeti.NDRPair.cylinderDeformation_one_mem.
• TauCeti.NDRPair.cylinderRetraction, TauCeti.NDRPair.cylinderHomotopyRel: the resulting strong deformation retraction of the cylinder onto J.
• TauCeti.NDRPair.hasHomotopyExtensionProperty: the subset of an NDR pair has the homotopy extension property.
• TauCeti.NDRPair.restrict: NDR data restricted to a subspace which its deformation keeps invariant.
• TauCeti.NDRPair.ofRetraction, TauCeti.nonempty_ndrPair_iff: Strøm's theorem, NDR data for a closed subset from a retraction of the cylinder, so that a subset admits NDR data exactly when it is closed and has the homotopy extension property.
• TauCeti.NDRPair.prod: the product of two NDR pairs.
• TauCeti.NDRPair.ofHomotopyRel: NDR data from a deformation of a neighbourhood U ⊇ A onto A, relative to A, and a function vanishing exactly on A that is less than one only on U.

References

• N. E. Steenrod, A convenient category of topological spaces, Michigan Math. J. 14 (1967), 133–152, Section 6, for NDR pairs and their products.
• J. P. May, A Concise Course in Algebraic Topology, Chapter 6, Section 4, for the product of NDR pairs.
• A. Strøm, Note on cofibrations II, Math. Scand. 22 (1968), 130–142, for the control function of a closed cofibration and for products.

structure TauCeti.NDRPair {X : Type u} [TopologicalSpace X] (A : Set X) : Type u

NDR data for a subset A ⊆ X: a control function u : X → I vanishing exactly on A, and a deformation H : I × X → X of the identity which fixes A pointwise and carries every point with u x < 1 into A at time 1.

• control : C(X, ↑unitInterval)

  The control function, vanishing exactly on A.

• control_eq_zero_iff (x : X) : self.control x = 0 ↔ x ∈ A
• deformation : C(↑unitInterval × X, X)

  The deformation of X, starting at the identity and fixing A.

• deformation_zero (x : X) : self.deformation (0, x) = x
• deformation_of_mem (t : ↑unitInterval) {x : X} (hx : x ∈ A) : self.deformation (t, x) = x
• deformation_one_mem {x : X} (hx : self.control x < 1) : self.deformation (1, x) ∈ A

theorem TauCeti.NDRPair.isClosed {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) : IsClosed A

The subset of an NDR pair is closed, being the zero set of its control function.

def TauCeti.NDRPair.cylinderControl {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) : C(↑unitInterval × X, ↑unitInterval)

The control function (t, x) ↦ t * u x of the bottom-and-sides subspace {0} × X ∪ I × A of the cylinder.

@[simp]

theorem TauCeti.NDRPair.cylinderControl_apply {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) (z : ↑unitInterval × X) : N.cylinderControl z = z.1 * N.control z.2

theorem TauCeti.NDRPair.cylinderControl_eq_zero_iff {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) (z : ↑unitInterval × X) : N.cylinderControl z = 0 ↔ z ∈ cylinderExtensionDomain A

The control function of the cylinder vanishes exactly on {0} × X ∪ I × A.

noncomputable def TauCeti.NDRPair.cylinderDeformation {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) : C(↑unitInterval × ↑unitInterval × X, ↑unitInterval × X)

The deformation of the cylinder I × X onto {0} × X ∪ I × A: at time s it sends (t, x) to (t - s * min t (u x), H (s * min 1 (t / u x), x)). For t > 0 the height is t * (1 - s * min 1 (u x / t)).

@[simp]

theorem TauCeti.NDRPair.coe_cylinderDeformation_fst {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) (s t : ↑unitInterval) (x : X) : ↑(N.cylinderDeformation (s, t, x)).1 = ↑t - ↑s * min ↑t ↑(N.control x)

@[simp]

theorem TauCeti.NDRPair.cylinderDeformation_snd {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) (s t : ↑unitInterval) (x : X) : (N.cylinderDeformation (s, t, x)).2 = N.deformation (s * Set.projIcc 0 1 ⋯ (↑t / ↑(N.control x)), x)

@[simp]

theorem TauCeti.NDRPair.cylinderDeformation_zero {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) (z : ↑unitInterval × X) : N.cylinderDeformation (0, z) = z

At time 0 the cylinder deformation is the identity.

@[simp]

theorem TauCeti.NDRPair.cylinderDeformation_of_mem {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) (s : ↑unitInterval) {z : ↑unitInterval × X} (hz : z ∈ cylinderExtensionDomain A) : N.cylinderDeformation (s, z) = z

The cylinder deformation fixes {0} × X ∪ I × A pointwise.

theorem TauCeti.NDRPair.cylinderDeformation_one_mem {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) (z : ↑unitInterval × X) : N.cylinderDeformation (1, z) ∈ cylinderExtensionDomain A

At time 1 the cylinder deformation lands in {0} × X ∪ I × A. Where t ≤ u x it reaches the bottom of the cylinder; otherwise u x < t ≤ 1, so H (1, x) lies in A. This includes the corner case u x = t = 1, which reaches the bottom.

noncomputable def TauCeti.NDRPair.cylinderRetraction {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) : C(↑unitInterval × X, ↑(cylinderExtensionDomain A))

The retraction of the cylinder I × X onto {0} × X ∪ I × A, the end of the cylinder deformation.

@[simp]

theorem TauCeti.NDRPair.coe_cylinderRetraction_apply {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) (z : ↑unitInterval × X) : ↑(N.cylinderRetraction z) = N.cylinderDeformation (1, z)

@[simp]

theorem TauCeti.NDRPair.cylinderRetraction_apply_coe {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) (z : ↑(cylinderExtensionDomain A)) : N.cylinderRetraction ↑z = z

The cylinder retraction fixes the points of {0} × X ∪ I × A.

noncomputable def TauCeti.NDRPair.cylinderHomotopyRel {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) : (ContinuousMap.id (↑unitInterval × X)).HomotopyRel ((ContinuousMap.subtypeVal (cylinderExtensionDomain A)).comp N.cylinderRetraction) (cylinderExtensionDomain A)

The cylinder deformation is a strong deformation retraction of I × X onto {0} × X ∪ I × A: a homotopy relative to that subspace from the identity to the retraction.

@[simp]

theorem TauCeti.NDRPair.cylinderHomotopyRel_apply {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) (w : ↑unitInterval × ↑unitInterval × X) : N.cylinderHomotopyRel w = N.cylinderDeformation w

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

The subset of an NDR pair has the homotopy extension property: the cylinder retracts onto {0} × X ∪ I × A.

def TauCeti.NDRPair.restrict {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) {Y : Set X} (hY : ∀ (t : ↑unitInterval), ∀ y ∈ Y, N.deformation (t, y) ∈ Y) : NDRPair (Subtype.val ⁻¹' A)

NDR data restricted to an invariant subspace. If the deformation of NDR data for A ⊆ X maps a subset Y into itself at all times, then the restrictions of the control function and of the deformation to Y are NDR data for the trace Y ∩ A of A on Y.

@[simp]

theorem TauCeti.NDRPair.restrict_control_apply {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) {Y : Set X} (hY : ∀ (t : ↑unitInterval), ∀ y ∈ Y, N.deformation (t, y) ∈ Y) (y : ↑Y) : (N.restrict hY).control y = N.control ↑y

The control function of NDRPair.restrict is the restriction of the control function.

@[simp]

theorem TauCeti.NDRPair.coe_restrict_deformation_apply {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) {Y : Set X} (hY : ∀ (t : ↑unitInterval), ∀ y ∈ Y, N.deformation (t, y) ∈ Y) (t : ↑unitInterval) (y : ↑Y) : ↑((N.restrict hY).deformation (t, y)) = N.deformation (t, ↑y)

The deformation of NDRPair.restrict is the restriction of the deformation.

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

Strøm's theorem. A retraction r of the cylinder I × X onto {0} × X ∪ I × A, for a closed subset A, gives NDR data for A: the deformation is the second coordinate of r, and the control function is x ↦ ⨆ t, t - (r (t, x)).1, the largest amount by which r lowers a point of the cylinder over x.

@[simp]

theorem TauCeti.NDRPair.coe_ofRetraction_control {X : Type u} [TopologicalSpace X] {A : Set X} {r : C(↑unitInterval × X, ↑unitInterval × X)} (hr : ∀ (p : ↑unitInterval × X), r p ∈ cylinderExtensionDomain A) (hr' : ∀ p ∈ cylinderExtensionDomain A, r p = p) (hA : IsClosed A) (x : X) : ↑((ofRetraction hr hr' hA).control x) = ⨆ (t : ↑unitInterval), ↑t - ↑(r (t, x)).1

The control function of ofRetraction is x ↦ ⨆ t, t - (r (t, x)).1.

@[simp]

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

The deformation of ofRetraction is the second coordinate of the retraction.

noncomputable def TauCeti.NDRPair.ofHomotopyRel {X : Type u} [TopologicalSpace X] {A U : Set X} (hAU : A ⊆ U) {r : C(↑U, ↑A)} (D : (ContinuousMap.id ↑U).HomotopyRel ((ContinuousMap.inclusion hAU).comp r) {x : ↑U | ↑x ∈ A}) (f : C(X, ↑unitInterval)) (hf : ∀ (x : X), f x = 0 ↔ x ∈ A) (hfU : ∀ (x : X), f x < 1 → x ∈ U) : NDRPair A

NDR data from a deformation of a neighbourhood. Let D be a homotopy, relative to A, from the identity of a set U ⊇ A to a retraction onto A, and let f : X → I vanish exactly on A with {f < 1} ⊆ U. Cutting D off by the time factor max 0 (min 1 (3 - 4 f)) gives NDR data for A, with control function min 1 (2 f). The deformation runs in full where f ≤ 1 / 2 and moves no point where 3 / 4 ≤ f. The set U need not be open.

@[simp]

theorem TauCeti.NDRPair.coe_ofHomotopyRel_control {X : Type u} [TopologicalSpace X] {A U : Set X} {hAU : A ⊆ U} {r : C(↑U, ↑A)} (D : (ContinuousMap.id ↑U).HomotopyRel ((ContinuousMap.inclusion hAU).comp r) {x : ↑U | ↑x ∈ A}) (f : C(X, ↑unitInterval)) (hf : ∀ (x : X), f x = 0 ↔ x ∈ A) (hfU : ∀ (x : X), f x < 1 → x ∈ U) (x : X) : ↑((ofHomotopyRel hAU D f hf hfU).control x) = min 1 (2 * ↑(f x))

The control function of ofHomotopyRel is min 1 (2 f).

theorem TauCeti.NDRPair.ofHomotopyRel_deformation_of_mem {X : Type u} [TopologicalSpace X] {A U : Set X} {hAU : A ⊆ U} {r : C(↑U, ↑A)} (D : (ContinuousMap.id ↑U).HomotopyRel ((ContinuousMap.inclusion hAU).comp r) {x : ↑U | ↑x ∈ A}) (f : C(X, ↑unitInterval)) (hf : ∀ (x : X), f x = 0 ↔ x ∈ A) (hfU : ∀ (x : X), f x < 1 → x ∈ U) (t : ↑unitInterval) {x : X} (hx : x ∈ U) : (ofHomotopyRel hAU D f hf hfU).deformation (t, x) = ↑(D (t * Set.projIcc 0 1 ⋯ (3 - 4 * ↑(f x)), ⟨x, hx⟩))

At a point of U, the deformation of ofHomotopyRel follows D with time scaled by max 0 (min 1 (3 - 4 f)).

theorem TauCeti.NDRPair.ofHomotopyRel_deformation_of_notMem {X : Type u} [TopologicalSpace X] {A U : Set X} {hAU : A ⊆ U} {r : C(↑U, ↑A)} (D : (ContinuousMap.id ↑U).HomotopyRel ((ContinuousMap.inclusion hAU).comp r) {x : ↑U | ↑x ∈ A}) (f : C(X, ↑unitInterval)) (hf : ∀ (x : X), f x = 0 ↔ x ∈ A) (hfU : ∀ (x : X), f x < 1 → x ∈ U) (t : ↑unitInterval) {x : X} (hx : x ∉ U) : (ofHomotopyRel hAU D f hf hfU).deformation (t, x) = x

Off U, the deformation of ofHomotopyRel does not move the point.

theorem TauCeti.NDRPair.ofHomotopyRel_deformation_of_le_half {X : Type u} [TopologicalSpace X] {A U : Set X} {hAU : A ⊆ U} {r : C(↑U, ↑A)} (D : (ContinuousMap.id ↑U).HomotopyRel ((ContinuousMap.inclusion hAU).comp r) {x : ↑U | ↑x ∈ A}) (f : C(X, ↑unitInterval)) (hf : ∀ (x : X), f x = 0 ↔ x ∈ A) (hfU : ∀ (x : X), f x < 1 → x ∈ U) (t : ↑unitInterval) {x : X} (hx : ↑(f x) ≤ 1 / 2) : (ofHomotopyRel hAU D f hf hfU).deformation (t, x) = ↑(D (t, ⟨x, ⋯⟩))

Where f ≤ 1 / 2, the deformation of ofHomotopyRel is D itself.

theorem TauCeti.NDRPair.ofHomotopyRel_deformation_of_three_quarters_le {X : Type u} [TopologicalSpace X] {A U : Set X} {hAU : A ⊆ U} {r : C(↑U, ↑A)} (D : (ContinuousMap.id ↑U).HomotopyRel ((ContinuousMap.inclusion hAU).comp r) {x : ↑U | ↑x ∈ A}) (f : C(X, ↑unitInterval)) (hf : ∀ (x : X), f x = 0 ↔ x ∈ A) (hfU : ∀ (x : X), f x < 1 → x ∈ U) (t : ↑unitInterval) {x : X} (hx : 3 / 4 ≤ ↑(f x)) : (ofHomotopyRel hAU D f hf hfU).deformation (t, x) = x

Where 3 / 4 ≤ f, the deformation of ofHomotopyRel does not move the point.

noncomputable def TauCeti.NDRPair.prod {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) {Y : Type v} [TopologicalSpace Y] {B : Set Y} (M : NDRPair B) : NDRPair (A ×ˢ Set.univ ∪ Set.univ ×ˢ B)

The product of NDR pairs. If (X, A) and (Y, B) are NDR pairs with controls u, v and deformations H, K, then so is (X × Y, A × Y ∪ X × B), with control (x, y) ↦ min (u x) (v y) and deformation (t, x, y) ↦ (H (t * min 1 (v y / u x), x), K (t * min 1 (u x / v y), y)): the factor with the smaller control value runs at full speed, and the other one in proportion.

@[simp]

theorem TauCeti.NDRPair.prod_control_apply {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) {Y : Type v} [TopologicalSpace Y] {B : Set Y} (M : NDRPair B) (p : X × Y) : (N.prod M).control p = min (N.control p.1) (M.control p.2)

The control function of the product of NDR pairs is the minimum of the two controls.

theorem TauCeti.NDRPair.prod_deformation_apply {X : Type u} [TopologicalSpace X] {A : Set X} (N : NDRPair A) {Y : Type v} [TopologicalSpace Y] {B : Set Y} (M : NDRPair B) (t : ↑unitInterval) (x : X) (y : Y) : (N.prod M).deformation (t, x, y) = (N.deformation (t * Set.projIcc 0 1 ⋯ (↑(M.control y) / ↑(N.control x)), x), M.deformation (t * Set.projIcc 0 1 ⋯ (↑(N.control x) / ↑(M.control y)), y))

The deformation of the product of NDR pairs runs the factor with the smaller control value at full speed, and the other one in proportion.

theorem TauCeti.nonempty_ndrPair_iff {X : Type u} [TopologicalSpace X] {A : Set X} : Nonempty (NDRPair A) ↔ IsClosed A ∧ HasHomotopyExtensionProperty A

Strøm's characterization of closed cofibrations: a subset admits NDR data exactly when it is closed and has the homotopy extension property.