Nonpositive subspaces of quadratic forms are totally real

Let Q be a quadratic form over a commutative semiring whose partial order is compatible with addition, and J a linear endomorphism. If Q(v) + Q(Jv) is positive for every nonzero v, then every submodule on which Q is nonpositive is totally real for J. No almost-complex identity, finite-dimensionality, division, linear order, or inner product is required. Over such a field in finite dimension, J is then automatically injective on such a subspace, so the subspace has at most half the ambient dimension. With a linear order, the negative index of inertia of Q has the same bound, also without finite-dimensionality, where it holds trivially because Module.finrank and the negative index are both 0. The inertia bound applies the subspace bound to the maximal negative-definite subspace provided by Mathlib's QuadraticForm.exists_finrank_eq_sigNeg_and_negDef.

The complex-dimension consequences for almost complex structures are in TauCeti.Geometry.Symplectic.QuadraticForm.

Main declarations

• QuadraticForm.isTotallyReal_of_add_comp_posDef: a nonpositive submodule is totally real for a linear endomorphism J when the sum of a quadratic form and its pullback by J is positive definite.
• QuadraticForm.two_mul_finrank_le_of_add_comp_posDef: such a nonpositive subspace has at most half the ambient dimension.
• QuadraticForm.two_mul_sigNeg_le_finrank_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.isTotallyReal_of_add_comp_posDef {R : Type u_1} {E : Type u_2} [CommSemiring R] [PartialOrder R] [IsOrderedAddMonoid R] [AddCommMonoid E] [Module R E] (Q : QuadraticForm R E) {W : Submodule R E} (J : E →ₗ[R] E) (hQJ : QuadraticMap.PosDef (Q + QuadraticMap.comp Q J)) (hW : ∀ v ∈ W, Q v ≤ 0) : TauCeti.IsTotallyReal J W

A submodule on which Q is nonpositive is totally real for a linear endomorphism J if Q(v) + Q(Jv) is positive for every nonzero v.

theorem QuadraticForm.two_mul_finrank_le_of_add_comp_posDef {K : Type u_1} {E : Type u_2} [Field K] [PartialOrder K] [IsOrderedAddMonoid K] [AddCommGroup E] [Module K E] [FiniteDimensional K E] (Q : QuadraticForm K E) {W : Submodule K E} (J : E →ₗ[K] E) (hQJ : QuadraticMap.PosDef (Q + QuadraticMap.comp Q J)) (hW : ∀ v ∈ W, Q v ≤ 0) : 2 * Module.finrank K ↥W ≤ Module.finrank K E

Every subspace on which Q is nonpositive has at most half the dimension of E if Q(v) + Q(Jv) is positive for every nonzero v, for a linear endomorphism J.

theorem QuadraticForm.two_mul_sigNeg_le_finrank_of_add_comp_posDef {K : Type u_1} {E : Type u_2} [Field K] [LinearOrder K] [IsOrderedAddMonoid K] [AddCommGroup E] [Module K E] (Q : QuadraticForm K E) (J : E →ₗ[K] E) (hQJ : QuadraticMap.PosDef (Q + QuadraticMap.comp Q J)) : 2 * sigNeg Q ≤ Module.finrank K E

If Q(v) + Q(Jv) is positive for every nonzero v, for a linear endomorphism J, then twice the negative index of inertia of Q is at most the dimension of E.