The Levi form of a real bilinear form on a complex vector space

Let V be a complex vector space and B a real bilinear form on its underlying real space. The Levi form of B is the sesquilinear form

B.leviForm v w = (B v w + B (I • v) (I • w) + I * (B (I • v) w - B v (I • w))) / 4,

conjugate-linear in v and complex-linear in w. It is the (1,1)-part of B: on a coordinate basis e_j of V, with I • e_j the imaginary coordinate directions, write B_{x_j y_k} = B (e_j) (I • e_k) and similarly for the other entries. Then the entry B.leviForm (e_j) (e_k) is (B_{x_j x_k} + B_{y_j y_k} + I (B_{y_j x_k} - B_{x_j y_k})) / 4, so for the (symmetric) real Hessian B of a function f the entry B.leviForm (e_k) (e_j) is the Wirtinger derivative ∂²f / ∂z_j ∂(conj z_k). The real part of its diagonal is one quarter of B v v + B (I • v) (I • v), and for symmetric B the diagonal is this real number.

The Levi form forgets the part of B which anticommutes with multiplication by I. This is why it transforms well under holomorphic maps: the second derivative of a holomorphic map is complex bilinear, and its contribution to a real Hessian is killed by the Levi form.

Main definitions

• LinearMap.BilinForm.leviForm: the Levi form of a real bilinear form.

Main results

• LinearMap.BilinForm.re_leviForm_apply, LinearMap.BilinForm.im_leviForm_apply: the real and imaginary parts of the Levi form.
• LinearMap.BilinForm.leviForm_apply_self: for symmetric B, the diagonal value is the real number (B v v + B (I • v) (I • v)) / 4.
• LinearMap.BilinForm.isSymm_leviForm: the Levi form of a symmetric form is Hermitian.
• LinearMap.BilinForm.leviForm_add, LinearMap.BilinForm.leviForm_smul: the Levi form is real linear in B.
• LinearMap.BilinForm.leviForm_compl₁₂_apply: pullback along a complex-linear map.
• LinearMap.BilinForm.leviForm_eq_zero_iff: the Levi form vanishes exactly on the forms which anticommute with multiplication by I, such as real parts of complex bilinear forms.
• LinearMap.BilinForm.finrank_add_finrank_le_of_re_leviForm_pos: if the Levi form is positive on a complex subspace P, every real subspace on which B is nonpositive has dimension at most dim_ℝ V - dim_ℂ P.
• LinearMap.BilinForm.sigNeg_add_finrank_le_of_re_leviForm_pos: if the Levi form of B is positive definite on a complex subspace P of the n-dimensional space V, then the negative index of inertia of B is at most 2n - dim_ℂ P. In particular, if the Levi form has at least n - q positive directions, the negative index of B is at most n + q.

References

• R. Hain, Notes on the Morse theory of complex manifolds.
• L. Hörmander, An introduction to complex analysis in several variables, Chapter II.

noncomputable def LinearMap.BilinForm.leviForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (B : LinearMap.BilinForm ℝ V) : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ

The Levi form of a real bilinear form B on a complex vector space: the sesquilinear form (B v w + B (I • v) (I • w) + I * (B (I • v) w - B v (I • w))) / 4, conjugate-linear in v and complex-linear in w. It is the (1,1)-part of B; for symmetric B its diagonal is one quarter of B v v + B (I • v) (I • v).

theorem LinearMap.BilinForm.leviForm_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (B : LinearMap.BilinForm ℝ V) (v w : V) : (B.leviForm v) w = 4⁻¹ * (↑((B v) w + (B (Complex.I • v)) (Complex.I • w)) + Complex.I * ↑((B (Complex.I • v)) w - (B v) (Complex.I • w)))

The defining formula of the Levi form.

@[simp]

theorem LinearMap.BilinForm.re_leviForm_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (B : LinearMap.BilinForm ℝ V) (v w : V) : ((B.leviForm v) w).re = ((B v) w + (B (Complex.I • v)) (Complex.I • w)) / 4

The real part of the Levi form is the I-invariant part of B, divided by four.

@[simp]

theorem LinearMap.BilinForm.im_leviForm_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (B : LinearMap.BilinForm ℝ V) (v w : V) : ((B.leviForm v) w).im = ((B (Complex.I • v)) w - (B v) (Complex.I • w)) / 4

The imaginary part of the Levi form.

theorem LinearMap.BilinForm.leviForm_apply_self {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] {B : LinearMap.BilinForm ℝ V} (hB : B.IsSymm) (v : V) : (B.leviForm v) v = ↑(((B v) v + (B (Complex.I • v)) (Complex.I • v)) / 4)

The diagonal of the Levi form of a symmetric form is the real number (B v v + B (I • v) (I • v)) / 4.

theorem LinearMap.BilinForm.isSymm_leviForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] {B : LinearMap.BilinForm ℝ V} (hB : B.IsSymm) : B.leviForm.IsSymm

The Levi form of a symmetric form is Hermitian.

@[simp]

theorem LinearMap.BilinForm.leviForm_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] : leviForm 0 = 0

The Levi form is real linear in the bilinear form.

@[simp]

theorem LinearMap.BilinForm.leviForm_add {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (B B' : LinearMap.BilinForm ℝ V) : (B + B').leviForm = B.leviForm + B'.leviForm

@[simp]

theorem LinearMap.BilinForm.leviForm_neg {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (B : LinearMap.BilinForm ℝ V) : (-B).leviForm = -B.leviForm

@[simp]

theorem LinearMap.BilinForm.leviForm_sub {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (B B' : LinearMap.BilinForm ℝ V) : (B - B').leviForm = B.leviForm - B'.leviForm

@[simp]

theorem LinearMap.BilinForm.leviForm_smul {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (B : LinearMap.BilinForm ℝ V) (r : ℝ) : (r • B).leviForm = ↑r • B.leviForm

@[simp]

theorem LinearMap.BilinForm.leviForm_compl₁₂_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] [AddCommGroup W] [Module ℝ W] [Module ℂ W] [IsScalarTower ℝ ℂ W] (B : LinearMap.BilinForm ℝ V) (g : W →ₗ[ℂ] V) (v w : W) : ((leviForm (compl₁₂ B (↑ℝ g) (↑ℝ g))) v) w = (B.leviForm (g v)) (g w)

Pullback along a complex-linear map. The Levi form of B (g ·) (g ·) is the Levi form of B evaluated on the images under g.

theorem LinearMap.BilinForm.leviForm_eq_zero_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (B : LinearMap.BilinForm ℝ V) : B.leviForm = 0 ↔ ∀ (v w : V), (B (Complex.I • v)) (Complex.I • w) = -(B v) w

The Levi form of B vanishes exactly when B anticommutes with multiplication by I, that is, when B (I • v) (I • w) = -B v w. Real parts of complex bilinear forms are of this kind.

theorem LinearMap.BilinForm.finrank_add_finrank_le_of_re_leviForm_pos {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (B : LinearMap.BilinForm ℝ V) [FiniteDimensional ℂ V] {P : Submodule ℂ V} (hP : ∀ v ∈ P, v ≠ 0 → 0 < ((B.leviForm v) v).re) {W : Submodule ℝ V} (hW : ∀ v ∈ W, (B v) v ≤ 0) : Module.finrank ℝ ↥W + Module.finrank ℂ ↥P ≤ Module.finrank ℝ V

Real index bound from a complex positive subspace. If the Levi form of B is positive definite on a complex subspace P, then every real subspace on which B is nonpositive has dimension at most dim_ℝ V - dim_ℂ P.

theorem LinearMap.BilinForm.sigNeg_add_finrank_le_of_re_leviForm_pos {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module ℂ V] [IsScalarTower ℝ ℂ V] (B : LinearMap.BilinForm ℝ V) [FiniteDimensional ℂ V] {P : Submodule ℂ V} (hP : ∀ v ∈ P, v ≠ 0 → 0 < ((B.leviForm v) v).re) : sigNeg (BilinMap.toQuadraticMap B) + Module.finrank ℂ ↥P ≤ Module.finrank ℝ V

Negative inertia bound from a complex positive subspace. If the Levi form of B is positive definite on a complex subspace P, then the negative index of inertia of B is at most dim_ℝ V - dim_ℂ P.