Milnor's retraction of a handle onto a lower sublevel with a cell attached

Near a nondegenerate critical point of index λ with critical value c, a Morse function has the form f = c - ‖u‖² + ‖v‖², where u ∈ Eᵤ runs over the λ negative directions and v ∈ Eₛ over the positive ones; these are the unstable and stable directions of the negative gradient flow. Passing the critical level attaches the λ-cell e = {‖u‖² ≤ ε, v = 0} to the lower sublevel {f ≤ c - ε}. In the quadratic model, the union of the lower sublevel and the cell is TauCeti.quadraticSublevelUnionCell ε, consisting of the points (u, v) with -‖u‖² + ‖v‖² ≤ -ε or with ‖u‖² ≤ ε and v = 0. Equivalently, it is the set of points with ‖v‖ ≤ √(‖u‖² - ε) (TauCeti.mem_quadraticSublevelUnionCell_iff_norm_le), using that the real square root of a negative number is 0.

This file constructs Milnor's deformation r_t of the quadratic model onto that set. The end map TauCeti.quadraticHandleRetraction ε keeps u and retracts v radially onto the closed ball of radius √(‖u‖² - ε); its fixed points are exactly the points of TauCeti.quadraticSublevelUnionCell ε. The homotopy TauCeti.quadraticHandleDeformation ε moves v along the segment from this retraction back to v, and fixes TauCeti.quadraticSublevelUnionCell ε throughout. In Milnor's three cases: points with ‖u‖² ≤ ε move along (u, t v) and end on the cell, points with ε ≤ ‖u‖² ≤ ‖v‖² + ε end on the level -‖u‖² + ‖v‖² = -ε, and points of the lower sublevel stay fixed.

At every time the deformation multiplies v by a scalar in [0, 1], namely (1 - t) min 1 (√(‖u‖² - ε) / ‖v‖) + t (TauCeti.quadraticHandleDeformation_apply_eq_smul, TauCeti.exists_quadraticHandleDeformation_apply_eq_smul). This scalar depends only on ‖u‖ and ‖v‖, which is what lets the deformation run fibrewise in a sum of normed vector bundles. Hence it preserves every set whose fibres {v | (u, v) ∈ X} are star-shaped about the origin, and X ∩ quadraticSublevelUnionCell ε is a strong deformation retract of each such X (TauCeti.exists_inter_quadraticSublevelUnionCell_deformation). Such sets include every sublevel of a function which, for fixed u, does not decrease when v is scaled up; Milnor applies the deformation to the sublevel {F ≤ c - ε} of a function F = f - μ(‖u‖² + 2‖v‖²) modified near the critical point; that sublevel is {f ≤ c - ε} together with a handle around the cell.

Main declarations

• TauCeti.quadraticSublevelUnionCell: the lower quadratic sublevel together with the cell.
• TauCeti.quadraticHandleRetraction: the retraction onto TauCeti.quadraticSublevelUnionCell ε, with TauCeti.quadraticHandleRetraction_mem and TauCeti.quadraticHandleRetraction_eq_self_iff.
• TauCeti.quadraticHandleDeformation: the deformation from the retraction to the identity, relative to TauCeti.quadraticSublevelUnionCell ε.
• TauCeti.quadraticHandleDeformation_mem_of_starConvex: the deformation preserves sets with star-shaped fibres.
• TauCeti.exists_inter_quadraticSublevelUnionCell_deformation: the strong deformation retraction of such a set onto its intersection with TauCeti.quadraticSublevelUnionCell ε.

References

• J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton University Press, 1963, proof of Theorem 3.2.

The lower sublevel with the cell attached

def TauCeti.quadraticSublevelUnionCell {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] (ε : ℝ) : Set (Eᵤ × Eₛ)

The lower sublevel {-‖u‖² + ‖v‖² ≤ -ε} of the quadratic model -‖u‖² + ‖v‖² of a Morse function at a critical point, together with the cell {‖u‖² ≤ ε, v = 0} of radius √ε in the negative directions u.

@[simp]

theorem TauCeti.mem_quadraticSublevelUnionCell {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {z : Eᵤ × Eₛ} : z ∈ quadraticSublevelUnionCell ε ↔ -‖z.1‖ ^ 2 + ‖z.2‖ ^ 2 ≤ -ε ∨ ‖z.1‖ ^ 2 ≤ ε ∧ z.2 = 0

theorem TauCeti.mem_quadraticSublevelUnionCell_iff_norm_le {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {z : Eᵤ × Eₛ} : z ∈ quadraticSublevelUnionCell ε ↔ ‖z.2‖ ≤ √(‖z.1‖ ^ 2 - ε)

A point lies in the lower quadratic sublevel with the cell attached exactly when its positive component has norm at most √(‖u‖² - ε).

The retraction

noncomputable def TauCeti.quadraticHandleRetraction {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] [NormedSpace ℝ Eₛ] (ε : ℝ) : C(Eᵤ × Eₛ, Eᵤ × Eₛ)

Milnor's retraction of the quadratic model onto TauCeti.quadraticSublevelUnionCell ε: it keeps u and retracts v radially onto the closed ball of radius √(‖u‖² - ε).

@[simp]

theorem TauCeti.quadraticHandleRetraction_apply {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] [NormedSpace ℝ Eₛ] (ε : ℝ) (z : Eᵤ × Eₛ) : (quadraticHandleRetraction ε) z = (z.1, radialRetraction (√(‖z.1‖ ^ 2 - ε)) z.2)

theorem TauCeti.quadraticHandleRetraction_mem {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] [NormedSpace ℝ Eₛ] (ε : ℝ) (z : Eᵤ × Eₛ) : (quadraticHandleRetraction ε) z ∈ quadraticSublevelUnionCell ε

The retraction takes values in the lower quadratic sublevel with the cell attached.

theorem TauCeti.quadraticHandleRetraction_eq_self_iff {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {z : Eᵤ × Eₛ} [NormedSpace ℝ Eₛ] : (quadraticHandleRetraction ε) z = z ↔ z ∈ quadraticSublevelUnionCell ε

The fixed points of the retraction are exactly the points of the lower quadratic sublevel with the cell attached.

The deformation

noncomputable def TauCeti.quadraticHandleDeformation {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] [NormedSpace ℝ Eₛ] (ε : ℝ) : (quadraticHandleRetraction ε).HomotopyRel (ContinuousMap.id (Eᵤ × Eₛ)) (quadraticSublevelUnionCell ε)

Milnor's deformation of the quadratic model onto TauCeti.quadraticSublevelUnionCell ε: at time t it keeps u and replaces v by (1 - t) r(v) + t v, where r(v) is the radial retraction of v onto the closed ball of radius √(‖u‖² - ε). It is a homotopy from TauCeti.quadraticHandleRetraction ε to the identity which fixes TauCeti.quadraticSublevelUnionCell ε.

@[simp]

theorem TauCeti.quadraticHandleDeformation_apply {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] [NormedSpace ℝ Eₛ] (ε : ℝ) (t : ↑unitInterval) (z : Eᵤ × Eₛ) : (quadraticHandleDeformation ε) (t, z) = (z.1, (1 - ↑t) • radialRetraction (√(‖z.1‖ ^ 2 - ε)) z.2 + ↑t • z.2)

theorem TauCeti.quadraticHandleDeformation_apply_eq_smul {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] [NormedSpace ℝ Eₛ] (ε : ℝ) (t : ↑unitInterval) (z : Eᵤ × Eₛ) : (quadraticHandleDeformation ε) (t, z) = (z.1, ((1 - ↑t) * min 1 (√(‖z.1‖ ^ 2 - ε) / ‖z.2‖) + ↑t) • z.2)

At time t the deformation multiplies v by (1 - t) min 1 (√(‖u‖² - ε) / ‖v‖) + t.

theorem TauCeti.mem_Icc_quadraticHandleDeformation_scalar {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] (ε : ℝ) (t : ↑unitInterval) (z : Eᵤ × Eₛ) : (1 - ↑t) * min 1 (√(‖z.1‖ ^ 2 - ε) / ‖z.2‖) + ↑t ∈ Set.Icc 0 1

The scalar (1 - t) min 1 (√(‖u‖² - ε) / ‖v‖) + t by which the deformation multiplies v lies in [0, 1].

theorem TauCeti.exists_quadraticHandleDeformation_apply_eq_smul {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] [NormedSpace ℝ Eₛ] (ε : ℝ) (t : ↑unitInterval) (z : Eᵤ × Eₛ) : ∃ s ∈ Set.Icc 0 1, (quadraticHandleDeformation ε) (t, z) = (z.1, s • z.2)

At every time, the deformation keeps u and multiplies v by a scalar in [0, 1].

theorem TauCeti.norm_snd_quadraticHandleDeformation_apply_le {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] [NormedSpace ℝ Eₛ] (ε : ℝ) (t : ↑unitInterval) (z : Eᵤ × Eₛ) : ‖((quadraticHandleDeformation ε) (t, z)).2‖ ≤ ‖z.2‖

The deformation never increases the norm of the positive component v.

theorem TauCeti.quadraticHandleDeformation_mem_of_starConvex {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {z : Eᵤ × Eₛ} [NormedSpace ℝ Eₛ] {X : Set (Eᵤ × Eₛ)} (hX : ∀ (u : Eᵤ), StarConvex ℝ 0 {v : Eₛ | (u, v) ∈ X}) (ε : ℝ) (t : ↑unitInterval) (hz : z ∈ X) : (quadraticHandleDeformation ε) (t, z) ∈ X

The deformation preserves every set whose fibres {v | (u, v) ∈ X} are star-shaped about the origin.

theorem TauCeti.exists_inter_quadraticSublevelUnionCell_deformation {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] [NormedSpace ℝ Eₛ] {X : Set (Eᵤ × Eₛ)} (hX : ∀ (u : Eᵤ), StarConvex ℝ 0 {v : Eₛ | (u, v) ∈ X}) (ε : ℝ) : ∃ (r : C(↑X, ↑(X ∩ quadraticSublevelUnionCell ε))), (∀ (x : ↑(X ∩ quadraticSublevelUnionCell ε)), r ((ContinuousMap.inclusion ⋯) x) = x) ∧ Nonempty (((ContinuousMap.inclusion ⋯).comp r).HomotopyRel (ContinuousMap.id ↑X) {x : ↑X | ↑x ∈ quadraticSublevelUnionCell ε})

Milnor's handle retraction. If every fibre {v | (u, v) ∈ X} of X is star-shaped about the origin, then X ∩ quadraticSublevelUnionCell ε is a strong deformation retract of X: there is a retraction of X onto it, and a homotopy in X from this retraction to the identity which fixes X ∩ quadraticSublevelUnionCell ε. Both are restrictions of TauCeti.quadraticHandleRetraction ε and TauCeti.quadraticHandleDeformation ε.