The parametric Morse lemma in a trivial bundle

A smooth family of functions with a critical zero section and a strongly nondegenerate vertical Hessian admits local coordinates preserving the base parameter. The coordinate change fixes the zero section and transforms the function into its vertical Hessian quadratic form. Both the coordinate change and its local inverse are jointly smooth in base and fiber.

The construction follows the operator-square-root proof of the Morse--Palais lemma, as formalized in TauCeti.Analysis.Calculus.Morse.NormalForm: apply its canonical congruence to the integral average of the vertical Hessian, then invert the map (b, v) ↦ (b, R (b, v) v). The Hessian convention is the second derivative itself, so the quadratic formula has a factor 1 / 2.

The fibre coordinate is canonical: TauCeti.parametricMorseCoord f (b, v) = R (b, v) v, where R (b, v) is the canonical congruence TauCeti.morseCongruence of the averaged vertical Hessian with the vertical Hessian at (b, 0). Because no choice enters, it is natural for fibrewise linear changes of coordinates: if g (b, v) = f (b, e b v) for linear equivalences e b depending continuously on b, then near the zero section parametricMorseCoord g (b, v) = (e b)⁻¹ (parametricMorseCoord f (b, e b v)) (TauCeti.eventually_parametricMorseCoord_comp). It also depends only on the germ of f along the zero section (Filter.EventuallyEq.parametricMorseCoord) and reads f only along fibres, so if f' (σ b, T b v) = f (b, v) near the zero section, for any change of parameter σ and fibre isomorphisms T b depending continuously on b, then parametricMorseCoord f' (σ b, T b v) = T b (parametricMorseCoord f (b, v)) near the zero section (TauCeti.eventually_parametricMorseCoord_transition). Read in two trivializations of a vector bundle, the canonical coordinates of a function therefore agree near the zero section. This is the compatibility with bundle transitions needed to patch the local normal forms of a Morse–Bott function along its critical submanifold; the patching itself is not done here.

Main declarations

• TauCeti.parametricMorseCoord: the canonical fibre coordinate.
• TauCeti.parametricMorseCoord_congr_of_eqOn: it only depends on the family near the segment in the fibre.
• TauCeti.eventually_eq_add_parametricMorseCoord: the family is its vertical Hessian quadratic form in this coordinate.
• TauCeti.eventually_contDiffAt_parametricMorseCoord and TauCeti.hasFDerivAt_parametricMorseCoord: it is C^n for a C^{n+2} family, with derivative the fibre projection on the zero section.
• TauCeti.eventually_parametricMorseCoord_comp: naturality for fibrewise linear changes of coordinates.
• Filter.EventuallyEq.parametricMorseCoord: the coordinate only depends on the germ of the family along the zero section.
• TauCeti.eventually_parametricMorseCoord_transition: compatibility with changes of trivialization, allowing a change of parameter and only a local relation between the families.
• TauCeti.exists_parametric_morse_normal_form and TauCeti.exists_parametric_morse_chart: the resulting coordinate change and local chart on a product neighbourhood, given by the canonical coordinate.

References

• R. S. Palais, The Morse lemma for Banach spaces, Bull. Amer. Math. Soc. 75 (1969), 968--971.
• R. S. Palais, Morse theory on Hilbert manifolds, Topology 2 (1963), 299--340, Section 2.

noncomputable def TauCeti.parametricMorseCoord {P : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : P × E → ℝ) (z : P × E) : E

The canonical parametric Morse coordinate of a family f (b, v): the fibre vector R (b, v) v, where R (b, v) is the canonical congruence TauCeti.morseCongruence comparing the averaged vertical Hessian along the segment from (b, 0) to (b, v) with the vertical Hessian at (b, 0). For a C^2 family whose zero section is critical near a and whose vertical Hessian H b at (b, 0) is invertible at b = a, near (a, 0) it satisfies f (b, v) = f (b, 0) + 2⁻¹ * H b (parametricMorseCoord f (b, v)) (parametricMorseCoord f (b, v)) (TauCeti.eventually_eq_add_parametricMorseCoord). Under the same regularity and invertibility hypotheses, the coordinate is unchanged by fibrewise linear changes of coordinates (TauCeti.eventually_parametricMorseCoord_comp).

theorem TauCeti.parametricMorseCoord_def {P : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : P × E → ℝ) (z : P × E) : parametricMorseCoord f z = (morseCongruence (fderiv ℝ (fderiv ℝ fun (v : E) => f (z.1, v)) 0) (hessianAverage (fun (v : E) => f (z.1, v)) 0 z.2)) z.2

The canonical parametric Morse coordinate applies the canonical congruence of the averaged vertical Hessian with the vertical Hessian at (b, 0) to the fibre vector.

@[simp]

theorem TauCeti.parametricMorseCoord_mk_zero {P : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : P × E → ℝ) (b : P) : parametricMorseCoord f (b, 0) = 0

The canonical parametric Morse coordinate vanishes on the zero section.

theorem TauCeti.parametricMorseCoord_congr_of_eqOn {P : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : P × E → ℝ} {z : P × E} {V : Set E} (hV : IsOpen V) (hV₀ : StarConvex ℝ 0 V) (hfg : Set.EqOn (fun (v : E) => f (z.1, v)) (fun (v : E) => g (z.1, v)) V) (hz : z.2 ∈ V) : parametricMorseCoord f z = parametricMorseCoord g z

The canonical parametric Morse coordinate only depends on the family near the segment in the fibre from 0 to z.2: families whose slices over z.1 agree on an open set star-convex about 0 and containing z.2 have the same coordinate at z.

theorem TauCeti.eventually_contDiffAt_parametricMorseCoord {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : P × E → ℝ} {a : P} {n : ℕ∞} (hf : ContDiff ℝ (↑n + 2) f) (hH : (fderiv ℝ (fderiv ℝ fun (v : E) => f (a, v)) 0).IsInvertible) : ∀ᶠ (z : P × E) in nhds (a, 0), ContDiffAt ℝ (↑n) (parametricMorseCoord f) z

Near a point of the zero section with invertible vertical Hessian, the canonical parametric Morse coordinate of a C^{n+2} family is C^n.

theorem TauCeti.hasFDerivAt_parametricMorseCoord {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : P × E → ℝ} {a : P} (hf : ContDiff ℝ 2 f) (hH : (fderiv ℝ (fderiv ℝ fun (v : E) => f (a, v)) 0).IsInvertible) : HasFDerivAt (parametricMorseCoord f) (ContinuousLinearMap.snd ℝ P E) (a, 0)

At a point of the zero section with invertible vertical Hessian, the derivative of the canonical parametric Morse coordinate of a C^2 family is the projection to the fibre.

theorem TauCeti.eventually_eq_add_parametricMorseCoord {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : P × E → ℝ} {a : P} (hf : ContDiff ℝ 2 f) (hcrit : ∀ᶠ (b : P) in nhds a, fderiv ℝ (fun (v : E) => f (b, v)) 0 = 0) (hH : (fderiv ℝ (fderiv ℝ fun (v : E) => f (a, v)) 0).IsInvertible) : ∀ᶠ (z : P × E) in nhds (a, 0), f z = f (z.1, 0) + 2⁻¹ * ((fderiv ℝ (fderiv ℝ fun (v : E) => f (z.1, v)) 0) (parametricMorseCoord f z)) (parametricMorseCoord f z)

The parametric Morse normal form in the canonical coordinate. Near a point (a, 0) of a critical zero section with invertible vertical Hessian, a C^2 family f is its vertical Hessian quadratic form at (b, 0) evaluated on the canonical parametric Morse coordinate.

theorem TauCeti.eventually_parametricMorseCoord_comp {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : P × E → ℝ} {a : P} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [CompleteSpace E'] (hf : ContDiff ℝ 2 f) (hH : (fderiv ℝ (fderiv ℝ fun (v : E) => f (a, v)) 0).IsInvertible) {e : P → E' ≃L[ℝ] E} (he : ContinuousAt (fun (b : P) => ↑(e b)) a) : ∀ᶠ (z : P × E') in nhds (a, 0), parametricMorseCoord (fun (z : P × E') => f (z.1, (e z.1) z.2)) z = (e z.1).symm (parametricMorseCoord f (z.1, (e z.1) z.2))

The canonical parametric Morse coordinate is natural for fibrewise linear changes of coordinates. Let e b : E' ≃L[ℝ] E be linear equivalences depending continuously on b at a, and let g (b, v) = f (b, e b v). Near (a, 0) the canonical coordinate of g is that of f read through e b: parametricMorseCoord g (b, v) = (e b)⁻¹ (parametricMorseCoord f (b, e b v)).

Applied to the coordinate changes of a vector bundle, this says that the canonical coordinates of a function read in two trivializations agree near the zero section, so that they define a single fibre-preserving coordinate change there.

theorem Filter.EventuallyEq.parametricMorseCoord {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a : P} {f₁ f₂ : P × E → ℝ} (h : f₁ =ᶠ[nhds (a, 0)] f₂) : TauCeti.parametricMorseCoord f₁ =ᶠ[nhds (a, 0)] TauCeti.parametricMorseCoord f₂

The canonical parametric Morse coordinate only depends on the germ of the family along the zero section. If two families agree near (a, 0), so do their canonical coordinates.

theorem TauCeti.parametricMorseCoord_comp_prodMap {P : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P' : Type u_3} (f : P' × E → ℝ) (σ : P → P') (b : P) (v : E) : parametricMorseCoord (fun (z : P × E) => f (σ z.1, z.2)) (b, v) = parametricMorseCoord f (σ b, v)

The canonical parametric Morse coordinate only reads the family along fibres. Changing the parameter of a family by any map σ changes its canonical coordinate in the same way.

theorem TauCeti.eventually_parametricMorseCoord_transition {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : P × E → ℝ} {a : P} {P' : Type u_3} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [CompleteSpace E'] {f' : P' × E' → ℝ} {σ : P → P'} {T : P → E ≃L[ℝ] E'} (hf : ContDiff ℝ 2 f) (hH : (fderiv ℝ (fderiv ℝ fun (v : E) => f (a, v)) 0).IsInvertible) (hT : ContinuousAt (fun (b : P) => ↑(T b)) a) (hcomp : ∀ᶠ (z : P × E) in nhds (a, 0), f' (σ z.1, (T z.1) z.2) = f z) : ∀ᶠ (z : P × E) in nhds (a, 0), parametricMorseCoord f' (σ z.1, (T z.1) z.2) = (T z.1) (parametricMorseCoord f z)

The canonical parametric Morse coordinate under a change of trivialization. Let a C^2 family f have invertible vertical Hessian at (a, 0), and let f' be the same family in other coordinates near the zero section: f' (σ b, T b v) = f (b, v) for (b, v) near (a, 0), where σ is any change of parameter and T b : E ≃L[ℝ] E' are linear isomorphisms of the fibres depending continuously on b at a. No regularity of f' or σ is assumed. Then near (a, 0) the canonical coordinates correspond: parametricMorseCoord f' (σ b, T b v) = T b (parametricMorseCoord f (b, v)).

theorem TauCeti.exists_parametric_morse_normal_form {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : P × E → ℝ} {a : P} {n : ℕ∞} (hf : ContDiff ℝ (↑n + 2) f) (hcrit : ∀ᶠ (b : P) in nhds a, fderiv ℝ (fun (v : E) => f (b, v)) 0 = 0) (hH : (fderiv ℝ (fderiv ℝ fun (v : E) => f (a, v)) 0).IsInvertible) : ∃ (U : Set P) (V : Set E), IsOpen U ∧ IsOpen V ∧ a ∈ U ∧ 0 ∈ V ∧ ContDiffOn ℝ (↑n) (fun (z : P × E) => (z.1, parametricMorseCoord f z)) (U ×ˢ V) ∧ HasFDerivAt (fun (z : P × E) => (z.1, parametricMorseCoord f z)) (ContinuousLinearMap.id ℝ (P × E)) (a, 0) ∧ ∀ z ∈ U ×ˢ V, f z = f (z.1, 0) + 2⁻¹ * ((fderiv ℝ (fderiv ℝ fun (v : E) => f (z.1, v)) 0) (parametricMorseCoord f z)) (parametricMorseCoord f z)

Parametric Morse normal form. A jointly C^{n+2} family with a critical zero section near a and invertible vertical Hessian at (a, 0) has a jointly C^n fiber coordinate change (b, v) ↦ (b, parametricMorseCoord f (b, v)) on a product neighborhood. It preserves the parameter, fixes the zero section (TauCeti.parametricMorseCoord_mk_zero), and has identity derivative at (a, 0). The reference quadratic form is the vertical Hessian at each (b, 0). The base space need not be complete for this forward coordinate construction.

theorem TauCeti.exists_parametric_morse_chart {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : P × E → ℝ} {a : P} {n : ℕ∞} [CompleteSpace P] (hf : ContDiff ℝ (↑n + 2) f) (hcrit : ∀ᶠ (b : P) in nhds a, fderiv ℝ (fun (v : E) => f (b, v)) 0 = 0) (hH : (fderiv ℝ (fderiv ℝ fun (v : E) => f (a, v)) 0).IsInvertible) (hn : n ≠ 0) : ∃ (ψ : OpenPartialHomeomorph (P × E) (P × E)) (U : Set P) (V : Set E), IsOpen U ∧ IsOpen V ∧ a ∈ U ∧ 0 ∈ V ∧ ψ.source = U ×ˢ V ∧ (∀ (z : P × E), ↑ψ z = (z.1, parametricMorseCoord f z)) ∧ (∀ z ∈ ψ.target, (↑ψ.symm z).1 = z.1) ∧ ContDiffOn ℝ (↑n) (↑ψ) ψ.source ∧ ContDiffOn ℝ (↑n) (↑ψ.symm) ψ.target ∧ ∀ z ∈ ψ.source, f z = f (z.1, 0) + 2⁻¹ * ((fderiv ℝ (fderiv ℝ fun (v : E) => f (z.1, v)) 0) (↑ψ z).2) (↑ψ z).2

The parametric Morse lemma, as a local chart. The chart has a product source containing (a, 0) and is given by the canonical coordinate (b, v) ↦ (b, parametricMorseCoord f (b, v)), so it preserves the base parameter and fixes the zero section; its inverse preserves the base parameter too. Its quadratic equation uses the vertical Hessian on that same zero section. The base and the fiber are Banach spaces, so the ordinary inverse function theorem applies to their product.