Definiteness and the signature of a quadratic form

This file characterizes positive and negative semidefiniteness by the vanishing of the opposite index of inertia. It also characterizes positive-definiteness by the negative index and the radical. These are convenient consequences of Sylvester's law of inertia which complement Mathlib's definitions of QuadraticMap.PosDef, sigPos, and sigNeg.

It also proves that restriction to a subspace cannot increase either index of inertia, that quotienting a quadratic form by its radical preserves both indices, and that multiplication by a positive scalar preserves both indices while multiplication by a negative scalar exchanges them. Finally, both indices are additive under orthogonal products.

Main results

• QuadraticForm.forall_nonneg_iff_sigNeg_eq_zero: nonnegativity is characterized by vanishing negative index of inertia.
• QuadraticForm.forall_nonpos_iff_sigPos_eq_zero: nonpositivity is characterized by vanishing positive index of inertia.
• QuadraticForm.sigPos_restrict_le: restriction to a subspace cannot increase the positive index of inertia.
• QuadraticForm.sigNeg_restrict_le: restriction to a subspace cannot increase the negative index of inertia.
• QuadraticForm.sigPos_smul_of_pos and QuadraticForm.sigNeg_smul_of_pos: positive scaling preserves both indices.
• QuadraticForm.sigPos_smul_of_neg and QuadraticForm.sigNeg_smul_of_neg: negative scaling exchanges the two indices.
• QuadraticForm.sigPos_lift_radical: quotienting by the radical preserves the positive index of inertia.
• QuadraticForm.sigNeg_lift_radical: quotienting by the radical preserves the negative index of inertia.
• QuadraticForm.sigPos_prod and QuadraticForm.sigNeg_prod: the indices of inertia are additive under orthogonal products.
• QuadraticForm.posDef_iff_sigNeg_eq_zero_and_radical_eq_bot: positive-definiteness is characterized by vanishing negative index and trivial radical.
• QuadraticForm.sigPos_add_sigNeg_of_nondegenerate: the two indices of inertia of a nondegenerate quadratic form add up to the dimension.

References

• W. Ebeling, Lattices and Codes, Chapter 1.

@[simp]

theorem QuadraticForm.posDef_smul_iff_of_pos {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] (Q : QuadraticForm K M) {a : K} (ha : 0 < a) : QuadraticMap.PosDef (a • Q) ↔ QuadraticMap.PosDef Q

Multiplication by a positive scalar preserves positive-definiteness. Thus a quadratic form is positive-definite if and only if its positive scalar multiple is.

@[simp]

theorem QuadraticForm.sigPos_smul_of_pos {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) {a : K} (ha : 0 < a) : sigPos (a • Q) = sigPos Q

Multiplication by a positive scalar preserves the positive index of inertia.

@[simp]

theorem QuadraticForm.sigNeg_smul_of_pos {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) {a : K} (ha : 0 < a) : sigNeg (a • Q) = sigNeg Q

Multiplication by a positive scalar preserves the negative index of inertia.

@[simp]

theorem QuadraticForm.sigPos_smul_of_neg {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) {a : K} (ha : a < 0) : sigPos (a • Q) = sigNeg Q

Multiplication by a negative scalar exchanges the positive and negative indices of inertia.

@[simp]

theorem QuadraticForm.sigNeg_smul_of_neg {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) {a : K} (ha : a < 0) : sigNeg (a • Q) = sigPos Q

Multiplication by a negative scalar exchanges the negative and positive indices of inertia.

theorem QuadraticForm.forall_nonneg_iff_sigNeg_eq_zero {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) : (∀ (x : M), 0 ≤ Q x) ↔ sigNeg Q = 0

A quadratic form is nonnegative exactly when its negative index of inertia vanishes.

theorem QuadraticForm.forall_nonpos_iff_sigPos_eq_zero {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) : (∀ (x : M), Q x ≤ 0) ↔ sigPos Q = 0

A quadratic form is nonpositive exactly when its positive index of inertia vanishes.

theorem QuadraticForm.sigPos_restrict_le {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) (W : Subspace K M) : sigPos (QuadraticMap.restrict Q W) ≤ sigPos Q

Restricting a quadratic form to a subspace cannot increase its positive index.

theorem QuadraticForm.sigNeg_restrict_le {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) (W : Subspace K M) : sigNeg (QuadraticMap.restrict Q W) ≤ sigNeg Q

Restricting a quadratic form to a subspace cannot increase its negative index.

@[simp]

theorem QuadraticForm.sigPos_prod {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] {M' : Type u_3} [AddCommGroup M'] [Module K M'] [FiniteDimensional K M'] (Q : QuadraticForm K M) (Q' : QuadraticForm K M') : sigPos (QuadraticMap.prod Q Q') = sigPos Q + sigPos Q'

The positive index of inertia is additive under orthogonal products.

@[simp]

theorem QuadraticForm.sigNeg_prod {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] {M' : Type u_3} [AddCommGroup M'] [Module K M'] [FiniteDimensional K M'] (Q : QuadraticForm K M) (Q' : QuadraticForm K M') : sigNeg (QuadraticMap.prod Q Q') = sigNeg Q + sigNeg Q'

The negative index of inertia is additive under orthogonal products.

theorem QuadraticForm.sigPos_lift_radical {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] [LinearOrder K] [IsStrictOrderedRing K] [FiniteDimensional K M] (Q : QuadraticForm K M) : sigPos (QuadraticMap.lift Q (QuadraticMap.radical Q) ⋯) = sigPos Q

Quotienting a quadratic form by its radical preserves its positive index of inertia.

theorem QuadraticForm.sigPos_lift_of_eq_radical {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] [LinearOrder K] [IsStrictOrderedRing K] [FiniteDimensional K M] (Q : QuadraticForm K M) (N : Subspace K M) (hN : N = QuadraticMap.radical Q) : sigPos (QuadraticMap.lift Q N ⋯) = sigPos Q

Lifting by a subspace known to be the radical preserves the positive index of inertia.

theorem QuadraticForm.sigNeg_lift_radical {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] [LinearOrder K] [IsStrictOrderedRing K] [FiniteDimensional K M] (Q : QuadraticForm K M) : sigNeg (QuadraticMap.lift Q (QuadraticMap.radical Q) ⋯) = sigNeg Q

Quotienting a quadratic form by its radical preserves its negative index of inertia.

theorem QuadraticForm.sigNeg_lift_of_eq_radical {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] [LinearOrder K] [IsStrictOrderedRing K] [FiniteDimensional K M] (Q : QuadraticForm K M) (N : Subspace K M) (hN : N = QuadraticMap.radical Q) : sigNeg (QuadraticMap.lift Q N ⋯) = sigNeg Q

Lifting by a subspace known to be the radical preserves the negative index of inertia.

theorem QuadraticForm.posDef_iff_sigNeg_eq_zero_and_radical_eq_bot {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] [LinearOrder K] [IsStrictOrderedRing K] [FiniteDimensional K M] (Q : QuadraticForm K M) : QuadraticMap.PosDef Q ↔ sigNeg Q = 0 ∧ QuadraticMap.radical Q = ⊥

A quadratic form is positive-definite exactly when its negative index vanishes and its radical is trivial.

theorem QuadraticForm.sigPos_add_sigNeg_of_nondegenerate {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] [LinearOrder K] [IsStrictOrderedRing K] [FiniteDimensional K M] (Q : QuadraticForm K M) (hQ : QuadraticMap.Nondegenerate) : sigPos Q + sigNeg Q = Module.finrank K M

The positive and negative indices of inertia of a nondegenerate quadratic form add up to the dimension of the space.

theorem LinearMap.BilinForm.isPosSemidef_iff_sigNeg_eq_zero {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (B : LinearMap.BilinForm K M) (hB : B.IsSymm) : B.IsPosSemidef ↔ sigNeg (BilinMap.toQuadraticMap B) = 0

A symmetric bilinear form is positive-semidefinite if and only if the negative index of its associated quadratic form vanishes.

theorem LinearMap.BilinForm.posDef_toQuadraticMap_iff_isPosSemidef_and_nondegenerate {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (B : LinearMap.BilinForm K M) (hB : B.IsSymm) : (BilinMap.toQuadraticMap B).PosDef ↔ B.IsPosSemidef ∧ B.Nondegenerate

The quadratic form of a symmetric bilinear form is positive-definite if and only if the bilinear form is positive-semidefinite and nondegenerate.

theorem LinearMap.BilinForm.posDef_toQuadraticMap_iff_finrank_ker_eq_zero_and_sigNeg_eq_zero {K : Type u_1} {M : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (B : LinearMap.BilinForm K M) (hB : B.IsSymm) : (BilinMap.toQuadraticMap B).PosDef ↔ Module.finrank K ↥(ker B) = 0 ∧ sigNeg (BilinMap.toQuadraticMap B) = 0

The quadratic form of a symmetric bilinear form is positive-definite if and only if the kernel of the bilinear form and the negative index of the quadratic form both vanish.