Disjoint Morse charts at a critical level

Passing a critical value c of a Morse function f attaches one handle at each critical point on the level f⁻¹(c). Milnor's construction (Morse Theory, Theorem 3.2) works in normalized Morse charts around these points, in which

f = c - Σ_{i < λ} yᵢ² + Σ_{i ≥ λ} yᵢ²,

modifies f inside the ellipsoid ‖u‖² + 2‖v‖² ≤ 2ε of each chart, and attaches the cell {‖u‖² ≤ ε, v = 0}; here u collects the λ negative coordinates and v the others. Before any of this can be done, the charts and the width ε have to be chosen compatibly:

• the band f⁻¹[c - ε, c + ε] contains no critical points except those on the level f⁻¹(c);
• the charts at the distinct critical points on that level have pairwise disjoint sources;
• the image of every chart contains the closed ball of radius √(2ε) about its centre, and hence both the ellipsoid and the closed negative-coordinate disc of radius √ε.

This file proves that such choices exist when the band f⁻¹[c - δ, c + δ] is compact, for every 0 < δ. Each condition persists when ε decreases. The charts can moreover be placed inside prescribed neighbourhoods of their centres; the disjoint charts themselves come from TauCeti.exists_pairwise_disjoint_normalized_morseCharts.

Main results

• TauCeti.IsMorse.exists_admissible_morseCharts: the compatible choice of the width ε and of disjoint normalized Morse charts at all critical points on the level f⁻¹(c).

References

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

theorem TauCeti.IsMorse.exists_admissible_morseCharts {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {f : M → ℝ} [T2Space M] (hf : IsMorse I f) {c δ : ℝ} (hδ : 0 < δ) (hcompact : IsCompact (f ⁻¹' Set.Icc (c - δ) (c + δ))) {U : M → Set M} (hU : ∀ x ∈ criticalPoints I f ∩ f ⁻¹' {c}, U x ∈ nhds x) : ∃ (ε : ℝ), 0 < ε ∧ ε ≤ δ ∧ criticalPoints I f ∩ f ⁻¹' Set.Icc (c - ε) (c + ε) ⊆ f ⁻¹' {c} ∧ ∃ (ψ : ↑(criticalPoints I f ∩ f ⁻¹' {c}) → PartialDiffeomorph I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin (Module.finrank ℝ E)))) M (EuclideanSpace ℝ (Fin (Module.finrank ℝ E))) ↑⊤), Pairwise (Function.onFun Disjoint fun (p : ↑(criticalPoints I f ∩ f ⁻¹' {c})) => (ψ p).source) ∧ ∀ (p : ↑(criticalPoints I f ∩ f ⁻¹' {c})), ↑p ∈ (ψ p).source ∧ (ψ p).source ⊆ U ↑p ∧ ↑(ψ p).toPartialEquiv ↑p = 0 ∧ Metric.closedBall 0 √(2 * ε) ⊆ (ψ p).target ∧ ∀ y ∈ (ψ p).source, f y = c + ∑ i : Fin (Module.finrank ℝ E), (if ↑i < manifoldMorseIndex I f ↑p then -1 else 1) * (↑(ψ p).toPartialEquiv y).ofLp i ^ 2

Admissible Morse charts at a critical level. Let f be a Morse function on a Hausdorff manifold whose band f⁻¹[c - δ, c + δ] is compact, for some 0 < δ. Then there are a width 0 < ε ≤ δ and normalized Morse charts ψ p, indexed by the critical points p on the level f⁻¹(c), such that

• the only critical points in the band f⁻¹[c - ε, c + ε] are those on the level f⁻¹(c);
• the chart sources are pairwise disjoint, and each lies in a prescribed neighbourhood U p;
• ψ p p = 0, and f = c - Σ_{i < λ} (ψ p)ᵢ² + Σ_{i ≥ λ} (ψ p)ᵢ² on the source of ψ p, where λ is the Morse index of f at p;
• the target of each chart contains the closed ball of radius √(2ε) about 0.

The last condition places Milnor's ellipsoid ‖u‖² + 2‖v‖² ≤ 2ε inside every chart. All of these conditions persist when ε is decreased.