Quadratic forms and almost complex structures

Let Q be a real quadratic form and J an almost complex structure. If Q(v) + Q(Jv) is positive for every nonzero v, then every subspace on which Q is nonpositive is totally real. It therefore has dimension at most the complex dimension determined by J. Applying this to the maximal negative-definite subspace provided by Mathlib's QuadraticForm.exists_finrank_eq_sigNeg_and_negDef bounds the negative index of inertia of Q.

This is the linear-algebraic index estimate behind the Morse-theoretic consequence of strict Levi positivity. No compatibility between J and an inner product is required. The totally-real criterion and the half-dimension bounds for an arbitrary linear endomorphism are in TauCeti.LinearAlgebra.TotallyReal.QuadraticForm.

Main declarations

• QuadraticForm.finrank_le_complexFinrank_of_add_comp_posDef: every such nonpositive subspace has at most the complex dimension of the ambient space.
• QuadraticForm.sigNeg_le_complexFinrank_of_add_comp_posDef: the negative index of inertia has the same bound.

References

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

theorem QuadraticForm.finrank_le_complexFinrank_of_add_comp_posDef {E : Type u_1} [AddCommGroup E] [Module ℝ E] (Q : QuadraticForm ℝ E) {W : Submodule ℝ E} [FiniteDimensional ℝ E] (J : TauCeti.AlmostComplexStructure E) (hQJ : QuadraticMap.PosDef (Q + QuadraticMap.comp Q J.toLinearMap)) (hW : ∀ v ∈ W, Q v ≤ 0) : Module.finrank ℝ ↥W ≤ J.complexFinrank

Every subspace on which Q is nonpositive has dimension at most the complex dimension defined by J when Q(v) + Q(Jv) is positive away from zero.

theorem QuadraticForm.sigNeg_le_complexFinrank_of_add_comp_posDef {E : Type u_1} [AddCommGroup E] [Module ℝ E] (Q : QuadraticForm ℝ E) (J : TauCeti.AlmostComplexStructure E) (hQJ : QuadraticMap.PosDef (Q + QuadraticMap.comp Q J.toLinearMap)) : sigNeg Q ≤ J.complexFinrank

If Q(v) + Q(Jv) is positive for every nonzero v, then the negative index of inertia of Q is at most the complex dimension defined by J.