Milnor's handle in the quadratic model is a product of discs

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. Milnor lowers f near the critical point to F = f - μ(‖u‖² + 2‖v‖²), where μ is a nonincreasing cutoff equal to 2ε near 0 and vanishing on [2ε, ∞). The modified function has the same upper sublevel {F ≤ c + ε} = {f ≤ c + ε} and no critical points in the band F⁻¹[c - ε, c + ε], so {f ≤ c + ε} is diffeomorphic to the sublevel {F ≤ c - ε}. That sublevel is the lower sublevel {f ≤ c - ε} together with the handle

H = {-ε ≤ -‖u‖² + ‖v‖², -‖u‖² + ‖v‖² - μ(‖u‖² + 2‖v‖²) ≤ -ε, ‖u‖² + 2‖v‖² ≤ 2ε}

(TauCeti.quadraticHandle ε μ): every point of {F ≤ c - ε} above the level f = c - ε lies in it (TauCeti.mem_quadraticHandle_or_eq_of_le). It meets the lower sublevel in its attaching region H ∩ {-‖u‖² + ‖v‖² = -ε}.

This file identifies the handle with the product D^λ × D^(m-λ) of closed unit discs, carrying the attaching region onto ∂D^λ × D^(m-λ). The identification is explicit: TauCeti.quadraticHandleMap rescales the two components,

(u, v) ↦ ((‖v‖² + ε)^(-1/2) • u, (‖u‖² + μ(‖u‖² + 2‖v‖²) - ε)^(-1/2) • v).

So the squared norms of the two components of the image are s / (t + ε) and t / (s + μ(s + 2t) - ε), where s = ‖u‖² and t = ‖v‖². On each line s = σ (t + ε) of constant first coordinate σ ∈ [0, 1], the second coordinate increases strictly with t from 0 on the core v = 0 to 1 on the top F = c - ε of the handle, because μ is nonincreasing. So the map is a bijection from the handle onto the product of the closed unit balls (TauCeti.bijOn_quadraticHandleMap), and since the handle is compact in finite dimensions it is a homeomorphism (TauCeti.quadraticHandleHomeomorph). The first component has norm 1 exactly on the attaching region (TauCeti.norm_fst_quadraticHandleMap_eq_one_iff) and the second exactly on the top of the handle (TauCeti.norm_snd_quadraticHandleMap_eq_one_iff); the second vanishes exactly on the core v = 0 (TauCeti.quadraticHandleMap_snd_eq_zero_iff).

The cutoff is assumed continuous, nonincreasing, larger than ε at ε, and positive exactly on (-∞, 2ε); the last condition makes the handle end where the cutoff does.

Main declarations

• TauCeti.quadraticHandle: Milnor's handle in the quadratic model.
• TauCeti.quadraticHandleMap: the rescaling which straightens it.
• TauCeti.bijOn_quadraticHandleMap: the rescaling maps the handle bijectively onto the product of the closed unit balls.
• TauCeti.quadraticHandleHomeomorph: the homeomorphism of the handle with D^λ × D^(m-λ).

References

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

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

Milnor's handle in the quadratic model -‖u‖² + ‖v‖² of a Morse function at a critical point: the points of the ellipsoid ‖u‖² + 2‖v‖² ≤ 2ε lying on or above the level -ε of the model and on or below the level -ε of the lowered model -‖u‖² + ‖v‖² - μ(‖u‖² + 2‖v‖²).

@[simp]

theorem TauCeti.mem_quadraticHandle {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} {z : Eᵤ × Eₛ} : z ∈ quadraticHandle ε μ ↔ -ε ≤ -‖z.1‖ ^ 2 + ‖z.2‖ ^ 2 ∧ -‖z.1‖ ^ 2 + ‖z.2‖ ^ 2 - μ (‖z.1‖ ^ 2 + 2 * ‖z.2‖ ^ 2) ≤ -ε ∧ ‖z.1‖ ^ 2 + 2 * ‖z.2‖ ^ 2 ≤ 2 * ε

theorem TauCeti.mem_quadraticHandle_or_eq_of_le {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} {z : Eᵤ × Eₛ} (hμ₀ : ∀ (r : ℝ), 2 * ε ≤ r → μ r = 0) (h₁ : -ε ≤ -‖z.1‖ ^ 2 + ‖z.2‖ ^ 2) (h₂ : -‖z.1‖ ^ 2 + ‖z.2‖ ^ 2 - μ (‖z.1‖ ^ 2 + 2 * ‖z.2‖ ^ 2) ≤ -ε) : z ∈ quadraticHandle ε μ ∨ -‖z.1‖ ^ 2 + ‖z.2‖ ^ 2 = -ε

Where the cutoff vanishes on [2ε, ∞), a point on or above the level -ε of the model and on or below the level -ε of the lowered model lies in the handle or on the level -ε of the model. So the handle is what the lowering adds to the lower sublevel of the model.

noncomputable def TauCeti.quadraticHandleMap {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (ε : ℝ) (μ : ℝ → ℝ) (z : Eᵤ × Eₛ) : Eᵤ × Eₛ

The rescaling (u, v) ↦ ((‖v‖² + ε)^(-1/2) • u, (‖u‖² + μ(‖u‖² + 2‖v‖²) - ε)^(-1/2) • v) which identifies Milnor's handle TauCeti.quadraticHandle ε μ with the product of the closed unit balls (TauCeti.bijOn_quadraticHandleMap).

theorem TauCeti.quadraticHandleMap_apply {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (z : Eᵤ × Eₛ) : quadraticHandleMap ε μ z = ((√(‖z.2‖ ^ 2 + ε))⁻¹ • z.1, (√(‖z.1‖ ^ 2 + μ (‖z.1‖ ^ 2 + 2 * ‖z.2‖ ^ 2) - ε))⁻¹ • z.2)

The handle in the coordinates s = ‖u‖², t = ‖v‖²

The handle and the rescaling only depend on s = ‖u‖² and t = ‖v‖². In these coordinates the handle is the region -ε ≤ -s + t, -s + t - μ(s + 2t) ≤ -ε, s + 2t ≤ 2ε, and the squared norms of the components of the rescaling are s / (t + ε) and t / (s + μ(s + 2t) - ε).

The rescaling as a homeomorphism

theorem TauCeti.norm_fst_quadraticHandleMap_sq {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hε : 0 < ε) (z : Eᵤ × Eₛ) : ‖(quadraticHandleMap ε μ z).1‖ ^ 2 = ‖z.1‖ ^ 2 / (‖z.2‖ ^ 2 + ε)

The squared norm of the first component of the rescaling is ‖u‖² / (‖v‖² + ε).

theorem TauCeti.norm_snd_quadraticHandleMap_sq {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} {z : Eᵤ × Eₛ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hμa : Antitone μ) (hμε : ε < μ ε) (hz : z ∈ quadraticHandle ε μ) : ‖(quadraticHandleMap ε μ z).2‖ ^ 2 = ‖z.2‖ ^ 2 / (‖z.1‖ ^ 2 + μ (‖z.1‖ ^ 2 + 2 * ‖z.2‖ ^ 2) - ε)

The squared norm of the second component of the rescaling is ‖v‖² / (‖u‖² + μ(‖u‖² + 2‖v‖²) - ε).

theorem TauCeti.mapsTo_quadraticHandleMap {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hε : 0 < ε) (hμa : Antitone μ) (hμε : ε < μ ε) : Set.MapsTo (quadraticHandleMap ε μ) (quadraticHandle ε μ) (Metric.closedBall 0 1 ×ˢ Metric.closedBall 0 1)

The rescaling maps the handle into the product of the closed unit balls.

theorem TauCeti.injOn_quadraticHandleMap {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hε : 0 < ε) (hμa : Antitone μ) (hμε : ε < μ ε) (hμ_pos : ∀ r < 2 * ε, 0 < μ r) : Set.InjOn (quadraticHandleMap ε μ) (quadraticHandle ε μ)

The rescaling is injective on the handle.

theorem TauCeti.surjOn_quadraticHandleMap {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hε : 0 < ε) (hμa : Antitone μ) (hμε : ε < μ ε) (hμ : Continuous μ) (hμ₀ : ∀ (r : ℝ), 2 * ε ≤ r → μ r = 0) : Set.SurjOn (quadraticHandleMap ε μ) (quadraticHandle ε μ) (Metric.closedBall 0 1 ×ˢ Metric.closedBall 0 1)

The rescaling maps the handle onto the product of the closed unit balls. Given (a, b), the coordinates s and t of a preimage are found on the line s = ‖a‖² (t + ε), and the preimage is (√(t + ε) • a, √(s + μ(s + 2t) - ε) • b).

theorem TauCeti.bijOn_quadraticHandleMap {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hε : 0 < ε) (hμa : Antitone μ) (hμε : ε < μ ε) (hμ : Continuous μ) (hμ₀ : ∀ (r : ℝ), 2 * ε ≤ r → μ r = 0) (hμ_pos : ∀ r < 2 * ε, 0 < μ r) : Set.BijOn (quadraticHandleMap ε μ) (quadraticHandle ε μ) (Metric.closedBall 0 1 ×ˢ Metric.closedBall 0 1)

Milnor's handle is a product of discs. The rescaling TauCeti.quadraticHandleMap maps the handle bijectively onto the product of the closed unit balls of Eᵤ and Eₛ.

theorem TauCeti.continuousOn_quadraticHandleMap {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hε : 0 < ε) (hμa : Antitone μ) (hμε : ε < μ ε) (hμ : Continuous μ) : ContinuousOn (quadraticHandleMap ε μ) (quadraticHandle ε μ)

The rescaling is continuous on the handle.

theorem TauCeti.isClosed_quadraticHandle {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} (hμ : Continuous μ) : IsClosed (quadraticHandle ε μ)

The handle is closed.

theorem TauCeti.isCompact_quadraticHandle {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] [FiniteDimensional ℝ Eᵤ] [FiniteDimensional ℝ Eₛ] (hμ : Continuous μ) : IsCompact (quadraticHandle ε μ)

In finite dimensions the handle is compact: it is closed and lies in the ellipsoid ‖u‖² + 2‖v‖² ≤ 2ε.

noncomputable def TauCeti.quadraticHandleHomeomorph {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hε : 0 < ε) (hμa : Antitone μ) (hμε : ε < μ ε) [FiniteDimensional ℝ Eᵤ] [FiniteDimensional ℝ Eₛ] (hμ : Continuous μ) (hμ₀ : ∀ (r : ℝ), 2 * ε ≤ r → μ r = 0) (hμ_pos : ∀ r < 2 * ε, 0 < μ r) : ↑(quadraticHandle ε μ) ≃ₜ ↑(Metric.closedBall 0 1) × ↑(Metric.closedBall 0 1)

Milnor's handle is a product of discs: the homeomorphism TauCeti.quadraticHandleMap from the handle onto the product of the closed unit balls of Eᵤ and Eₛ, that is onto D^λ × D^(m-λ). The first component has norm 1 exactly on the attaching region (TauCeti.norm_fst_quadraticHandleMap_eq_one_iff).

@[simp]

theorem TauCeti.coe_fst_quadraticHandleHomeomorph {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hε : 0 < ε) (hμa : Antitone μ) (hμε : ε < μ ε) [FiniteDimensional ℝ Eᵤ] [FiniteDimensional ℝ Eₛ] (hμ : Continuous μ) (hμ₀ : ∀ (r : ℝ), 2 * ε ≤ r → μ r = 0) (hμ_pos : ∀ r < 2 * ε, 0 < μ r) (z : ↑(quadraticHandle ε μ)) : ↑((quadraticHandleHomeomorph hε hμa hμε hμ hμ₀ hμ_pos) z).1 = (quadraticHandleMap ε μ ↑z).1

@[simp]

theorem TauCeti.coe_snd_quadraticHandleHomeomorph {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hε : 0 < ε) (hμa : Antitone μ) (hμε : ε < μ ε) [FiniteDimensional ℝ Eᵤ] [FiniteDimensional ℝ Eₛ] (hμ : Continuous μ) (hμ₀ : ∀ (r : ℝ), 2 * ε ≤ r → μ r = 0) (hμ_pos : ∀ r < 2 * ε, 0 < μ r) (z : ↑(quadraticHandle ε μ)) : ↑((quadraticHandleHomeomorph hε hμa hμε hμ hμ₀ hμ_pos) z).2 = (quadraticHandleMap ε μ ↑z).2

theorem TauCeti.norm_fst_quadraticHandleMap_eq_one_iff {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hε : 0 < ε) (z : Eᵤ × Eₛ) : ‖(quadraticHandleMap ε μ z).1‖ = 1 ↔ -‖z.1‖ ^ 2 + ‖z.2‖ ^ 2 = -ε

The attaching region. On the handle, the first component of the rescaling has norm 1 exactly on the level -‖u‖² + ‖v‖² = -ε, where the handle meets the lower sublevel.

theorem TauCeti.norm_snd_quadraticHandleMap_eq_one_iff {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} {z : Eᵤ × Eₛ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hμa : Antitone μ) (hμε : ε < μ ε) (hz : z ∈ quadraticHandle ε μ) : ‖(quadraticHandleMap ε μ z).2‖ = 1 ↔ -‖z.1‖ ^ 2 + ‖z.2‖ ^ 2 - μ (‖z.1‖ ^ 2 + 2 * ‖z.2‖ ^ 2) = -ε

The top of the handle. On the handle, the second component of the rescaling has norm 1 exactly on the level -‖u‖² + ‖v‖² - μ(‖u‖² + 2‖v‖²) = -ε of the lowered model.

theorem TauCeti.quadraticHandleMap_snd_eq_zero_iff {Eᵤ : Type u_1} {Eₛ : Type u_2} [NormedAddCommGroup Eᵤ] [NormedAddCommGroup Eₛ] {ε : ℝ} {μ : ℝ → ℝ} {z : Eᵤ × Eₛ} [NormedSpace ℝ Eᵤ] [NormedSpace ℝ Eₛ] (hμa : Antitone μ) (hμε : ε < μ ε) (hz : z ∈ quadraticHandle ε μ) : (quadraticHandleMap ε μ z).2 = 0 ↔ z.2 = 0

The core of the handle. On the handle, the second component of the rescaling vanishes exactly on the core v = 0, which contains the cell {‖u‖² ≤ ε, v = 0}.