Milnor's handle retraction in Morse charts

Passing a critical level c of a Morse function f attaches one cell at each critical point on the level. In a normalized Morse chart ψ of index λ around such a point,

f = c - Σ_{j < λ} yⱼ² + Σ_{j ≥ λ} yⱼ²,

and the cell is the disc {‖y‖² ≤ ε, yⱼ = 0 for j ≥ λ} of the negative coordinates. Milnor (Morse Theory, Theorem 3.2) retracts the sublevel {F ≤ c - ε} of a function F lowered near the critical points onto {f ≤ c - ε} with these cells attached, by a deformation which in each chart only shrinks the positive coordinates. The quadratic model of this deformation is TauCeti.quadraticHandleDeformation; this file reads it in finitely many charts with disjoint sources and glues it to the identity outside them.

The result, TauCeti.exists_inter_sublevel_union_cells_deformation, applies to any set X ⊆ M whose points outside the balls ‖ψ x‖ ≤ ρ of the charts lie in {f ≤ c - ε}, and which is preserved inside these balls by scaling the positive coordinates by factors in [0, 1]. For such X, the intersection of X with {f ≤ c - ε} and the cells is a strong deformation retract of X. The charts and width supplied by TauCeti.IsMorse.exists_admissible_morseCharts satisfy the hypotheses on the charts with ρ = √(2ε).

The positive and negative coordinates of a chart are separated by EuclideanSpace.sumComplEquivProd, which turns the chart into one with values in the product Eᵤ × Eₛ on which TauCeti.quadraticHandleDeformation is defined. The deformation moves no point outside the compact preimages of the balls, which makes the gluing continuous.

Main results

• TauCeti.exists_inter_sublevel_union_cells_deformation: Milnor's retraction of X onto its intersection with the lower sublevel and the cells of disjoint Morse charts.

References

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

theorem TauCeti.exists_inter_sublevel_union_cells_deformation {M : Type u_1} {ι : Type u_2} [TopologicalSpace M] {n : ℕ} [T2Space M] [Finite ι] (ψ : ι → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (hψ : Pairwise (Function.onFun Disjoint fun (i : ι) => (ψ i).source)) (k : ι → ℕ) {f : M → ℝ} {c ε ρ : ℝ} (hρ : ∀ (i : ι), Metric.closedBall 0 ρ ⊆ (ψ i).target) (hf : ∀ (i : ι), ∀ y ∈ (ψ i).source, f y = c + ∑ j : Fin n, (if ↑j < k i then -1 else 1) * (↑(ψ i) y).ofLp j ^ 2) {X : Set M} (hXout : ∀ x ∈ X, (∀ (i : ι), x ∈ (ψ i).source → ρ < ‖↑(ψ i) x‖) → f x ≤ c - ε) (hXscale : ∀ (i : ι), ∀ x ∈ X ∩ (ψ i).source, ‖↑(ψ i) x‖ ≤ ρ → ∀ s ∈ Set.Icc 0 1, ↑(ψ i).symm (WithLp.toLp 2 fun (j : Fin n) => if ↑j < k i then (↑(ψ i) x).ofLp j else s * (↑(ψ i) x).ofLp j) ∈ X) : ∃ (r : C(↑X, ↑(X ∩ ({x : M | f x ≤ c - ε} ∪ ⋃ (i : ι), (ψ i).source ∩ ↑(ψ i) ⁻¹' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ^ 2 ≤ ε ∧ ∀ (j : Fin n), k i ≤ ↑j → y.ofLp j = 0})))), (∀ (x : ↑(X ∩ ({x : M | f x ≤ c - ε} ∪ ⋃ (i : ι), (ψ i).source ∩ ↑(ψ i) ⁻¹' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ^ 2 ≤ ε ∧ ∀ (j : Fin n), k i ≤ ↑j → y.ofLp j = 0}))), r ((ContinuousMap.inclusion ⋯) x) = x) ∧ Nonempty (((ContinuousMap.inclusion ⋯).comp r).HomotopyRel (ContinuousMap.id ↑X) {x : ↑X | ↑x ∈ {x : M | f x ≤ c - ε} ∪ ⋃ (i : ι), (ψ i).source ∩ ↑(ψ i) ⁻¹' {y : EuclideanSpace ℝ (Fin n) | ‖y‖ ^ 2 ≤ ε ∧ ∀ (j : Fin n), k i ≤ ↑j → y.ofLp j = 0}})

Milnor's handle retraction in Morse charts. Let ψ i be charts of M with pairwise disjoint sources, each containing the closed ball of radius ρ about 0 in its target, in which f = c - Σ_{j < k i} yⱼ² + Σ_{j ≥ k i} yⱼ². The cell of the chart ψ i is the disc {‖y‖² ≤ ε, yⱼ = 0 for j ≥ k i} of the first k i coordinates, read in M. Let X ⊆ M be a set such that

• every point of X outside the balls ‖ψ i x‖ ≤ ρ lies in the sublevel {f ≤ c - ε};
• inside these balls, X is preserved by scaling the coordinates yⱼ, j ≥ k i, by factors in [0, 1].

Then X ∩ ({f ≤ c - ε} ∪ ⋃ cells) 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 it pointwise. In Milnor's proof of cell attachment, X is the sublevel {F ≤ c - ε} of the function F obtained by lowering f near the critical points, and the conclusion retracts it onto {f ≤ c - ε} with one cell attached at each critical point.