Levi forms and inertia of the quadratic models

This file computes the Levi form and the Morse index of the model quadratic functions of complex Morse theory on a complex vector space V of dimension n.

• The Levi form of a real quadratic function z ↦ B z z is the Levi form of its polarization B.flip + B.
• For a continuous complex bilinear form q, the real part z ↦ Re (q z z) of the holomorphic quadratic form has vanishing Levi form. Multiplication by I negates its Hessian, so its positive and negative indices of inertia agree, and its radical is the kernel of the polarization q.flip + q. Hence its Morse index is the complex rank of q.flip + q; it is n when q.flip + q is nondegenerate.
• The squared norm z ↦ ‖z‖ ^ 2 of a complex inner product space is the positive Hermitian quadratic function: its Levi form is the inner product ⟪v, w⟫_ℂ, so it is strictly plurisubharmonic, and its Morse index is zero. Every positive definite Hermitian form on a finite-dimensional complex space is the inner product of some inner product space structure, so this is the general positive Hermitian quadratic function.
• For real t, the sum z ↦ t ‖z‖ ^ 2 + Re (q z z) has Levi form t ⟪·, ·⟫; in particular z ↦ ‖z‖ ^ 2 + Re (q z z) still has the inner product as Levi form. On ℂⁿ with the diagonal form q(z, z) = ∑ j, a j * z j ^ 2 (a j real), the Morse index of ‖z‖ ^ 2 + Re (q z z) is the number of j with 1 < |a j|. Choosing a, every index between 0 and n occurs for a strictly plurisubharmonic quadratic function, so the index bound λ ≤ n for strictly plurisubharmonic functions cannot be improved.
• For an orthonormal basis b of a finite-dimensional complex inner product space, the function a ‖z‖² + Re (∑ⱼ c j ⟪b j, z⟫²) has Levi form a ⟪·, ·⟫ and Morse index ∑ⱼ ([a < ‖c j‖] + [a < -‖c j‖]). In coordinates it is ∑ⱼ (a |zⱼ|² + Re (c j zⱼ²)), and each coordinate contributes the inertia of a |w|² + Re (c j w²) on ℂ, whose real eigenvalues are a ± ‖c j‖. With one coefficient c for all j, the index is n [a < ‖c‖] + n [a < -‖c‖]: for a > 0 the function is strictly plurisubharmonic, and its Morse index jumps from 0 to the complex dimension when ‖c‖ crosses a. The diagonal example on ℂⁿ above is the case of the standard basis, a = 1 and real c j.

Main results

• ContinuousLinearMap.leviForm_apply_self: the Levi form of z ↦ B z z.
• ContinuousLinearMap.hessianQuadraticForm_re_apply_self, ContinuousLinearMap.leviForm_re_apply_self: the Hessian and the Levi form of Re (q z z).
• ContinuousLinearMap.morseIndex_re_apply_self_add_finrank_ker: the Morse index of Re (q z z) plus the complex dimension of the kernel of q.flip + q is n.
• TauCeti.leviForm_norm_sq, TauCeti.morseIndex_norm_sq_complex: the Levi form of ‖z‖ ^ 2 is the inner product, and its Morse index is zero.
• ContinuousLinearMap.hessianQuadraticForm_mul_norm_sq_add_re_apply_self, ContinuousLinearMap.leviForm_mul_norm_sq_add_re_apply_self: the Hessian and the Levi form of a ‖z‖ ^ 2 + Re (q z z); the Levi form is a ⟪·, ·⟫.
• TauCeti.leviForm_euclidean_norm_sq_add_sum_re_sq, TauCeti.morseIndex_euclidean_norm_sq_add_sum_re_sq: on ℂⁿ, the Levi form of ‖z‖ ^ 2 + ∑ j, a j * Re (z j ^ 2) is the standard inner product and its Morse index is the number of j with 1 < |a j|.
• OrthonormalBasis.hessianQuadraticForm_mul_norm_sq_add_re_sum_mul_inner_sq, OrthonormalBasis.leviForm_mul_norm_sq_add_re_sum_mul_inner_sq, OrthonormalBasis.morseIndex_mul_norm_sq_add_re_sum_mul_inner_sq: the Hessian, the Levi form and the Morse index of a ‖z‖² + Re (∑ⱼ c j ⟪b j, z⟫²) for an orthonormal basis b.
• OrthonormalBasis.morseIndex_mul_norm_sq_add_re_mul_sum_inner_sq: the Morse index of a ‖z‖² + Re (c ∑ⱼ ⟪b j, z⟫²).

References

• J. Milnor, Morse Theory, Princeton University Press, 1963, §7.
• R. Hain, Notes on the Morse theory of complex manifolds.

Real quadratic functions

@[simp]

theorem ContinuousLinearMap.leviForm_apply_self {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (B : V →L[ℝ] V →L[ℝ] ℝ) (x : V) : TauCeti.leviForm (fun (z : V) => (B z) z) x = (B.flip + B).toBilinForm.leviForm

The Levi form of the real quadratic function z ↦ B z z is the Levi form of the polarization B.flip + B, at every point.

The real part of a holomorphic quadratic form

theorem ContinuousLinearMap.hessianQuadraticForm_re_apply_self {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (q : V →L[ℂ] V →L[ℂ] ℂ) (x v : V) : (TauCeti.hessianQuadraticForm (fun (z : V) => ((q z) z).re) x) v = 2 * ((q v) v).re

The Hessian quadratic form of the real part of the holomorphic quadratic form q z z is v ↦ 2 * Re (q v v), at every point.

@[simp]

theorem ContinuousLinearMap.leviForm_re_apply_self {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (q : V →L[ℂ] V →L[ℂ] ℂ) (x : V) : TauCeti.leviForm (fun (z : V) => ((q z) z).re) x = 0

The real part of a holomorphic quadratic form has vanishing Levi form.

theorem ContinuousLinearMap.morseIndex_re_apply_self_eq_sigPos {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (q : V →L[ℂ] V →L[ℂ] ℂ) (x : V) : TauCeti.morseIndex (fun (z : V) => ((q z) z).re) x = sigPos (TauCeti.hessianQuadraticForm (fun (z : V) => ((q z) z).re) x)

The real part of a holomorphic quadratic form has equal positive and negative indices of inertia: multiplication by I negates its Hessian.

theorem ContinuousLinearMap.radical_hessianQuadraticForm_re_apply_self {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (q : V →L[ℂ] V →L[ℂ] ℂ) (x : V) : QuadraticMap.radical (TauCeti.hessianQuadraticForm (fun (z : V) => ((q z) z).re) x) = Submodule.restrictScalars ℝ (↑(q.flip + q)).ker

The radical of the Hessian of the real part of a holomorphic quadratic form is the kernel of the polarization q.flip + q.

theorem ContinuousLinearMap.morseIndex_re_apply_self_add_finrank_ker {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (q : V →L[ℂ] V →L[ℂ] ℂ) [FiniteDimensional ℂ V] (x : V) : TauCeti.morseIndex (fun (z : V) => ((q z) z).re) x + Module.finrank ℂ ↥(↑(q.flip + q)).ker = Module.finrank ℂ V

The inertia of the real part of a holomorphic quadratic form. The Morse index of z ↦ Re (q z z) is the complex rank of the polarization q.flip + q: together with the complex dimension of its kernel it adds up to the complex dimension of V.

theorem ContinuousLinearMap.morseIndex_re_apply_self_of_ker_eq_bot {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (q : V →L[ℂ] V →L[ℂ] ℂ) [FiniteDimensional ℂ V] (hq : (↑(q.flip + q)).ker = ⊥) (x : V) : TauCeti.morseIndex (fun (z : V) => ((q z) z).re) x = Module.finrank ℂ V

If the polarization q.flip + q of a complex bilinear form is injective, the real part of the holomorphic quadratic form q z z has Morse index equal to the complex dimension of V.

The squared norm and its holomorphic perturbations

@[simp]

theorem TauCeti.leviForm_norm_sq {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) : leviForm (fun (z : E) => ‖z‖ ^ 2) x = innerₛₗ ℂ

The Levi form of the squared norm of a complex inner product space is the inner product. In particular the squared norm is strictly plurisubharmonic.

theorem TauCeti.hessianQuadraticForm_norm_sq_complex {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x v : E) : (hessianQuadraticForm (fun (z : E) => ‖z‖ ^ 2) x) v = 2 * ‖v‖ ^ 2

The Hessian quadratic form of the squared norm of a complex inner product space is v ↦ 2 * ‖v‖ ^ 2.

@[simp]

theorem TauCeti.morseIndex_norm_sq_complex {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (x : E) : morseIndex (fun (z : E) => ‖z‖ ^ 2) x = 0

The squared norm of a finite-dimensional complex inner product space has Morse index zero at every point.

@[simp]

theorem ContinuousLinearMap.leviForm_mul_norm_sq_add_re_apply_self {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (q : E →L[ℂ] E →L[ℂ] ℂ) (a : ℝ) (x : E) : TauCeti.leviForm (fun (z : E) => a * ‖z‖ ^ 2 + ((q z) z).re) x = ↑a • innerₛₗ ℂ

Adding the real part of a holomorphic quadratic form to a real multiple a ‖z‖ ^ 2 of the squared norm does not change the Levi form: it is still a times the inner product.

@[simp]

theorem ContinuousLinearMap.leviForm_norm_sq_add_re_apply_self {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (q : E →L[ℂ] E →L[ℂ] ℂ) (x : E) : TauCeti.leviForm (fun (z : E) => ‖z‖ ^ 2 + ((q z) z).re) x = innerₛₗ ℂ

Adding the real part of a holomorphic quadratic form to the squared norm does not change the Levi form: it is still the inner product. In particular ‖z‖ ^ 2 + Re (q z z) is strictly plurisubharmonic.

theorem ContinuousLinearMap.hessianQuadraticForm_mul_norm_sq_add_re_apply_self {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (q : E →L[ℂ] E →L[ℂ] ℂ) (a : ℝ) (x v : E) : (TauCeti.hessianQuadraticForm (fun (z : E) => a * ‖z‖ ^ 2 + ((q z) z).re) x) v = 2 * a * ‖v‖ ^ 2 + 2 * ((q v) v).re

The Hessian quadratic form of z ↦ a ‖z‖ ^ 2 + Re (q z z) is v ↦ 2 a ‖v‖ ^ 2 + 2 Re (q v v), at every point.

Hermitian plus holomorphic quadratic functions in an orthonormal basis

theorem OrthonormalBasis.hessianQuadraticForm_mul_norm_sq_add_re_sum_mul_inner_sq {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Fintype ι] (b : OrthonormalBasis ι ℂ E) (a : ℝ) (c : ι → ℂ) (x v : E) : (TauCeti.hessianQuadraticForm (fun (z : E) => a * ‖z‖ ^ 2 + (∑ j : ι, c j * inner ℂ (b j) z ^ 2).re) x) v = 2 * (a * ‖v‖ ^ 2 + (∑ j : ι, c j * inner ℂ (b j) v ^ 2).re)

The Hessian of a Hermitian plus holomorphic quadratic function. For an orthonormal basis b, the Hessian quadratic form of a ‖z‖² + Re (∑ⱼ c j ⟪b j, z⟫²) is v ↦ 2 (a ‖v‖² + Re (∑ⱼ c j ⟪b j, v⟫²)) at every point.

theorem OrthonormalBasis.leviForm_mul_norm_sq_add_re_sum_mul_inner_sq {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Fintype ι] (b : OrthonormalBasis ι ℂ E) (a : ℝ) (c : ι → ℂ) (x : E) : TauCeti.leviForm (fun (z : E) => a * ‖z‖ ^ 2 + (∑ j : ι, c j * inner ℂ (b j) z ^ 2).re) x = ↑a • innerₛₗ ℂ

The Levi form of a Hermitian plus holomorphic quadratic function. For an orthonormal basis b, the Levi form of a ‖z‖² + Re (∑ⱼ c j ⟪b j, z⟫²) is a ⟪·, ·⟫ at every point: the holomorphic part does not contribute.

theorem OrthonormalBasis.morseIndex_mul_norm_sq_add_re_sum_mul_inner_sq {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Fintype ι] (b : OrthonormalBasis ι ℂ E) (a : ℝ) (c : ι → ℂ) (x : E) : TauCeti.morseIndex (fun (z : E) => a * ‖z‖ ^ 2 + (∑ j : ι, c j * inner ℂ (b j) z ^ 2).re) x = ∑ j : ι, ((if a < ‖c j‖ then 1 else 0) + if a < -‖c j‖ then 1 else 0)

The Morse index of a Hermitian plus holomorphic quadratic function. For an orthonormal basis b, the Morse index of a ‖z‖² + Re (∑ⱼ c j ⟪b j, z⟫²) counts, for each j, one negative direction if a < ‖c j‖ and a second one if a < -‖c j‖.

By the Autonne-Takagi factorization, on a finite-dimensional space every holomorphic quadratic form q z z is ∑ⱼ c j ⟪b j, z⟫² with c j ≥ 0 for some orthonormal basis b, so this computes the inertia of every function a ‖z‖² + Re (q z z).

theorem OrthonormalBasis.morseIndex_mul_norm_sq_add_re_mul_sum_inner_sq {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Fintype ι] (b : OrthonormalBasis ι ℂ E) (a : ℝ) (c : ℂ) (x : E) : TauCeti.morseIndex (fun (z : E) => a * ‖z‖ ^ 2 + (c * ∑ j : ι, inner ℂ (b j) z ^ 2).re) x = (if a < ‖c‖ then Module.finrank ℂ E else 0) + if a < -‖c‖ then Module.finrank ℂ E else 0

The Morse index of a Hermitian plus holomorphic quadratic function with one coefficient. For an orthonormal basis b of a complex inner product space of complex dimension n, the Morse index of a ‖z‖² + Re (c ∑ⱼ ⟪b j, z⟫²) is n if -‖c‖ ≤ a < ‖c‖, it is 2 n if a < -‖c‖, and it is 0 if ‖c‖ ≤ a.

In particular, for a = 0 and c ≠ 0, the real part of the nondegenerate holomorphic quadratic form c ∑ⱼ ⟪b j, z⟫² has Morse index n. For a = 1, the strictly plurisubharmonic function ‖z‖² + Re (c ∑ⱼ ⟪b j, z⟫²) has Morse index n if 1 < ‖c‖, and 0 otherwise.

A diagonal example on ℂⁿ

@[simp]

theorem TauCeti.leviForm_euclidean_norm_sq_add_sum_re_sq {ι : Type u_2} [Fintype ι] (a : ι → ℝ) (x : EuclideanSpace ℂ ι) : leviForm (fun (z : EuclideanSpace ℂ ι) => ‖z‖ ^ 2 + ∑ j : ι, a j * (z.ofLp j ^ 2).re) x = innerₛₗ ℂ

On ℂⁿ, the Levi form of z ↦ ‖z‖ ^ 2 + ∑ j, a j * Re (z j ^ 2) is the standard Hermitian inner product, for all real a j.

theorem TauCeti.hessianQuadraticForm_euclidean_norm_sq_add_sum_re_sq {ι : Type u_2} [Fintype ι] (a : ι → ℝ) (x v : EuclideanSpace ℂ ι) : (hessianQuadraticForm (fun (z : EuclideanSpace ℂ ι) => ‖z‖ ^ 2 + ∑ j : ι, a j * (z.ofLp j ^ 2).re) x) v = ∑ j : ι, (2 * (1 + a j) * (v.ofLp j).re ^ 2 + 2 * (1 - a j) * (v.ofLp j).im ^ 2)

On ℂⁿ, in the coordinates z j = x j + I y j, the Hessian quadratic form of z ↦ ‖z‖ ^ 2 + ∑ j, a j * Re (z j ^ 2) is ∑ j, (2 (1 + a j) x j ^ 2 + 2 (1 - a j) y j ^ 2).

theorem TauCeti.morseIndex_euclidean_norm_sq_add_sum_re_sq {ι : Type u_2} [Fintype ι] (a : ι → ℝ) (x : EuclideanSpace ℂ ι) : morseIndex (fun (z : EuclideanSpace ℂ ι) => ‖z‖ ^ 2 + ∑ j : ι, a j * (z.ofLp j ^ 2).re) x = {j : ι | 1 < |a j|}.ncard

Explicit inertia of a strictly plurisubharmonic quadratic function. On ℂⁿ, the function z ↦ ‖z‖ ^ 2 + ∑ j, a j * Re (z j ^ 2), whose Levi form is the standard Hermitian inner product (TauCeti.leviForm_euclidean_norm_sq_add_sum_re_sq), has Morse index equal to the number of j with 1 < |a j|, at every point.