Signature of a quadratic form

We define the signature of a quadratic form over a linearly ordered field, and show that it can be computed from any sum-of-squares representation.

Main results and definitions

• QuadraticForm.sigPos, QuadraticForm.sigNeg: for a quadratic form Q, the maximal dimension of a subspace on which Q is positive-definite (resp. negative-definite).
• QuadraticForm.sigPos_of_equiv_weightedSumOfSquares, QuadraticForm.sigNeg_of_equiv_weightedSumOfSquares: for any isomorphism from Q to a weighted sum of squares, Q.sigPos and Q.sigNeg are the number of positive and negative weights. (This is the uniqueness part of Sylvester's law of inertia; the existence is QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared in file Mathlib.LinearAlgebra.QuadraticForm.Real.)

Acknowledgements

This file is based on work carried out by Sina Keller, Philipp Schumann, and Nicolas Trutmann in the course of their studies at ETH Zürich.

@[simp]

theorem QuadraticMap.IsometryEquiv.map_posDef_iff {R : Type u_1} {M : Type u_2} {M' : Type u_3} [AddCommGroup M] [AddCommGroup M'] [CommRing R] [LinearOrder R] [Module R M] {Q : QuadraticForm R M} [Module R M'] {Q' : QuadraticForm R M'} {V : Submodule R M} (e : IsometryEquiv Q Q') : (restrict Q' (Submodule.map (↑e.toLinearEquiv) V)).PosDef ↔ (restrict Q V).PosDef

@[simp]

theorem QuadraticMap.IsometryEquiv.map_negDef_iff {R : Type u_1} {M : Type u_2} {M' : Type u_3} [AddCommGroup M] [AddCommGroup M'] [CommRing R] [LinearOrder R] [Module R M] {Q : QuadraticForm R M} [Module R M'] {Q' : QuadraticForm R M'} {V : Submodule R M} (e : IsometryEquiv Q Q') : (restrict (-Q') (Submodule.map (↑e.toLinearEquiv) V)).PosDef ↔ (restrict (-Q) V).PosDef

noncomputable def sigPos {R : Type u_1} {M : Type u_2} [AddCommGroup M] [CommRing R] [LinearOrder R] [Module R M] (Q : QuadraticForm R M) : ℕ

For quadratic forms on finite-dimensional spaces, the maximal finrank of a positive-definite subspace of M. (Defined as 0 if M is infinite-dimensional).

Equations

• sigPos Q = {r ∈ Finset.Iic (Module.finrank R M) | ∃ (V : Submodule R M), Module.finrank R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}.max' ⋯

theorem sigPos_le_finrank {R : Type u_1} {M : Type u_2} [AddCommGroup M] [CommRing R] [LinearOrder R] [Module R M] (Q : QuadraticForm R M) : sigPos Q ≤ Module.finrank R M

theorem sigPos_isGreatest {R : Type u_1} {M : Type u_2} [AddCommGroup M] [CommRing R] [LinearOrder R] [Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R] : IsGreatest {r : ℕ | ∃ (V : Submodule R M), Module.finrank R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef} (sigPos Q)

Defining property of sigPos.

theorem exists_finrank_eq_sigPos_and_posDef {R : Type u_1} {M : Type u_2} [AddCommGroup M] [CommRing R] [LinearOrder R] [Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R] : ∃ (V : Submodule R M), Module.finrank R ↥V = sigPos Q ∧ (QuadraticMap.restrict Q V).PosDef

theorem le_sigPos_of_posDef {R : Type u_1} {M : Type u_2} [AddCommGroup M] [CommRing R] [LinearOrder R] [Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R] {V : Submodule R M} (hV : (QuadraticMap.restrict Q V).PosDef) : Module.finrank R ↥V ≤ sigPos Q

noncomputable def sigNeg {R : Type u_1} {M : Type u_2} [AddCommGroup M] [CommRing R] [LinearOrder R] [Module R M] (Q : QuadraticForm R M) : ℕ

For quadratic forms on finite-dimensional spaces, the maximal finrank of a negative-definite subspace of M. (Defined as 0 if M is infinite-dimensional).

Equations

• sigNeg Q = sigPos (-Q)

theorem sigNeg_isGreatest {R : Type u_1} {M : Type u_2} [AddCommGroup M] [CommRing R] [LinearOrder R] [Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R] : IsGreatest {r : ℕ | ∃ (V : Submodule R M), Module.finrank R ↥V = r ∧ (QuadraticMap.restrict (-Q) V).PosDef} (sigNeg Q)

Defining property of sigNeg.

theorem exists_finrank_eq_sigNeg_and_negDef {R : Type u_1} {M : Type u_2} [AddCommGroup M] [CommRing R] [LinearOrder R] [Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R] : ∃ (V : Submodule R M), Module.finrank R ↥V = sigNeg Q ∧ (QuadraticMap.restrict (-Q) V).PosDef

theorem le_sigNeg_of_negDef {R : Type u_1} {M : Type u_2} [AddCommGroup M] [CommRing R] [LinearOrder R] [Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R] {V : Submodule R M} (hV : (QuadraticMap.restrict (-Q) V).PosDef) : Module.finrank R ↥V ≤ sigNeg Q

@[simp]

theorem sigPos_neg {R : Type u_1} {M : Type u_2} [AddCommGroup M] [CommRing R] [LinearOrder R] [Module R M] {Q : QuadraticForm R M} : sigPos (-Q) = sigNeg Q

@[simp]

theorem sigNeg_neg {R : Type u_1} {M : Type u_2} [AddCommGroup M] [CommRing R] [LinearOrder R] [Module R M] {Q : QuadraticForm R M} : sigNeg (-Q) = sigPos Q

theorem QuadraticMap.Equivalent.sigPos_eq {R : Type u_1} {M : Type u_2} {M' : Type u_3} [AddCommGroup M] [AddCommGroup M'] [CommRing R] [LinearOrder R] [Module R M] {Q : QuadraticForm R M} [Module R M'] {Q' : QuadraticForm R M'} (h : Equivalent Q Q') : sigPos Q = sigPos Q'

theorem QuadraticMap.Equivalent.sigNeg_eq {R : Type u_1} {M : Type u_2} {M' : Type u_3} [AddCommGroup M] [AddCommGroup M'] [CommRing R] [LinearOrder R] [Module R M] {Q : QuadraticForm R M} [Module R M'] {Q' : QuadraticForm R M'} (h : Equivalent Q Q') : sigNeg Q = sigNeg Q'

theorem QuadraticForm.sigPos_add_finrank_le_of_nonpos {M : Type u_2} [AddCommGroup M] {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [Module 𝕜 M] {Q : QuadraticForm 𝕜 M} [FiniteDimensional 𝕜 M] {V : Subspace 𝕜 M} (hV : ∀ x ∈ V, Q x ≤ 0) : sigPos Q + Module.finrank 𝕜 ↥V ≤ Module.finrank 𝕜 M

Key lemma for Sylvester's law of inertia: the sum of sigPos Q and the dimension of any negative-semidefinite subspace is bounded above by the dimension of the whole space.

theorem QuadraticForm.sigPos_weightedSumSquares {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_5} [Fintype ι] {w : ι → 𝕜} [IsStrictOrderedRing 𝕜] : sigPos (QuadraticMap.weightedSumSquares 𝕜 w) = {i : ι | 0 < w i}.ncard

Key lemma for Sylvester's law of inertia: compute the signature of a weighted sum of squares.

theorem QuadraticForm.sigNeg_weightedSumSquares {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_5} [Fintype ι] {w : ι → 𝕜} [IsStrictOrderedRing 𝕜] : sigNeg (QuadraticMap.weightedSumSquares 𝕜 w) = {i : ι | w i < 0}.ncard

theorem QuadraticForm.sigPos_add_sigNeg_add_radical {M : Type u_2} [AddCommGroup M] {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [Module 𝕜 M] {Q : QuadraticForm 𝕜 M} [IsStrictOrderedRing 𝕜] [FiniteDimensional 𝕜 M] : sigPos Q + sigNeg Q + Module.finrank 𝕜 ↥(QuadraticMap.radical Q) = Module.finrank 𝕜 M

theorem QuadraticForm.sigPos_of_equiv_weightedSumSquares {M : Type u_2} [AddCommGroup M] {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [Module 𝕜 M] {Q : QuadraticForm 𝕜 M} {ι : Type u_5} [Fintype ι] {w : ι → 𝕜} [IsStrictOrderedRing 𝕜] (hQ : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares 𝕜 w)) : sigPos Q = {i : ι | 0 < w i}.ncard

Uniqueness part of Sylvester's law of inertia (positive part): for any weighted sum of squares equivalent to Q, the number of strictly positive weights is equal to sigPos Q.

theorem QuadraticForm.sigNeg_of_equiv_weightedSumSquares {M : Type u_2} [AddCommGroup M] {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [Module 𝕜 M] {Q : QuadraticForm 𝕜 M} {ι : Type u_5} [Fintype ι] {w : ι → 𝕜} [IsStrictOrderedRing 𝕜] (hQ : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares 𝕜 w)) : sigNeg Q = {i : ι | w i < 0}.ncard

Uniqueness part of Sylvester's law of inertia (negative part): for any weighted sum of squares equivalent to Q, the number of strictly negative weights is equal to sigNeg Q.