Classification of real quadratic forms by their signature

Mathlib proves the two halves of Sylvester's law of inertia separately: every real quadratic form on a finite-dimensional space is equivalent to a weighted sum of squares with weights 1, 0 and -1, and the numbers of positive and of negative weights are the invariants sigPos and sigNeg. This file combines them into the classification itself: two real quadratic forms are isometric exactly when their dimensions and their two indices of inertia agree. For a nondegenerate form the two indices already determine the dimension, so a regular real form is classified by its signature alone.

The file also supplies the normal form realizing a prescribed signature, the orthogonal sum of p copies of ⟨1⟩ and q copies of ⟨-1⟩, and shows that every regular real form is isometric to the normal form of its own signature.

Without any finite-dimensionality assumption, a real quadratic form is anisotropic exactly when it is positive or negative definite. This identifies the algebraic condition used in compactness criteria for real orthogonal groups with the usual order-theoretic notion of definiteness.

Main results

• QuadraticForm.anisotropic_iff_posDef_or_negDef: real anisotropic forms are exactly the positive and negative definite forms, including forms on the zero space.
• QuadraticForm.anisotropic_iff_sigNeg_eq_zero_or_sigPos_eq_zero: a real form with trivial radical on a finite-dimensional space is anisotropic exactly when one of its two indices of inertia vanishes.
• QuadraticMap.anisotropic_weightedSumSquares_iff: a real diagonal form is anisotropic exactly when its coefficients are all positive or all negative.
• QuadraticMap.map_inv_sqrt_smul_eq_one: a vector of positive quadratic value can be normalized to value one by inverse-square-root scaling. This normalization feeds the reflection-pair construction for compact real Clifford forms.
• QuadraticMap.map_inv_sqrt_abs_smul_eq_one_or_neg_one: a vector of nonzero quadratic value can be normalized to value 1 or -1.
• QuadraticMap.exists_isOrtho_of_mul_pos: two orthogonal vectors whose values are nonzero of the same sign rescale to orthogonal vectors with the same value 1 or -1.
• QuadraticForm.sigPos_weightedSumSquares_signType and QuadraticForm.sigNeg_weightedSumSquares_signType: the two indices of inertia of a sign-weighted sum of squares count the weights 1 and the weights -1.
• QuadraticForm.equivalent_iff_finrank_eq_and_sigPos_eq_and_sigNeg_eq: two real quadratic forms on finite-dimensional spaces are isometric exactly when their dimensions and both indices of inertia agree.
• QuadraticForm.equivalent_iff_sigPos_eq_and_sigNeg_eq: two nondegenerate real quadratic forms are isometric exactly when their signatures agree.
• QuadraticForm.realSignatureForm: the normal form of signature (p, q).
• QuadraticForm.sigPos_realSignatureForm, QuadraticForm.sigNeg_realSignatureForm and QuadraticForm.nondegenerate_realSignatureForm: every signature is realized by a regular form.
• QuadraticForm.equivalent_realSignatureForm: a regular real quadratic form is isometric to the normal form of its signature.
• QuadraticForm.equivalent_weightedSumSquares_ite_lt_sigNeg: the same normal form on the coordinate space, with the sigNeg Q negative squares first.
• QuadraticForm.exists_nondegenerate_and_sigPos_eq_and_sigNeg_eq: every signature (p, n - p) is realized by a regular form on the coordinate space ℝⁿ.
• QuadraticForm.equivalent_realSignatureForm_iff_sigPos_eq_and_sigNeg_eq: a regular real form is isometric to a prescribed normal form exactly when it has the prescribed signature.
• QuadraticForm.equivalent_realSignatureForm_iff: distinct signatures give non-isometric normal forms.

References

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

@[simp]

theorem QuadraticMap.map_inv_sqrt_smul_eq_one {M : Type u_1} [AddCommMonoid M] [Module ℝ M] {Q : QuadraticForm ℝ M} {v : M} (hpos : 0 < Q v) : Q ((√(Q v))⁻¹ • v) = 1

Scaling a vector by the inverse square root of its positive quadratic value gives value one.

theorem QuadraticMap.map_inv_sqrt_abs_smul {M : Type u_1} [AddCommMonoid M] [Module ℝ M] (Q : QuadraticForm ℝ M) (v : M) : Q ((√|Q v|)⁻¹ • v) = Q v / |Q v|

Scaling a vector by the inverse square root of the absolute value of its quadratic value gives value Q v / |Q v|, which is 1, -1 or 0 according to the sign of Q v.

theorem QuadraticMap.map_inv_sqrt_abs_smul_eq_one_or_neg_one {M : Type u_1} [AddCommMonoid M] [Module ℝ M] {Q : QuadraticForm ℝ M} {v : M} (hv : Q v ≠ 0) : Q ((√|Q v|)⁻¹ • v) = 1 ∨ Q ((√|Q v|)⁻¹ • v) = -1

Scaling a vector of nonzero quadratic value by the inverse square root of the absolute value of that quadratic value gives value 1 or -1.

theorem QuadraticMap.exists_isOrtho_of_mul_pos {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {e f : M} (hef : IsOrtho Q e f) (h : 0 < Q e * Q f) : ∃ (e' : M) (f' : M), (Q e' = 1 ∨ Q e' = -1) ∧ Q f' = Q e' ∧ IsOrtho Q e' f'

Two orthogonal vectors whose quadratic values are nonzero of the same sign rescale to two orthogonal vectors with the same quadratic value 1 or -1.

theorem QuadraticForm.anisotropic_iff_posDef_or_negDef {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) : QuadraticMap.Anisotropic Q ↔ QuadraticMap.PosDef Q ∨ QuadraticMap.PosDef (-Q)

A real quadratic form is anisotropic if and only if it is positive or negative definite. No finite-dimensionality assumption is needed; on the zero space both alternatives hold.

theorem QuadraticForm.anisotropic_iff_sigNeg_eq_zero_or_sigPos_eq_zero {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} (hQ : QuadraticMap.radical Q = ⊥) : QuadraticMap.Anisotropic Q ↔ sigNeg Q = 0 ∨ sigPos Q = 0

A real quadratic form with trivial radical on a finite-dimensional space is anisotropic if and only if one of its two indices of inertia vanishes: an indefinite regular real form is isotropic.

theorem QuadraticMap.anisotropic_weightedSumSquares_iff {ι : Type u_2} [Fintype ι] (b : ι → ℝ) : (weightedSumSquares ℝ b).Anisotropic ↔ (∀ (i : ι), 0 < b i) ∨ ∀ (i : ι), b i < 0

A real diagonal form ⟨b₁, …, bₙ⟩ is anisotropic exactly when its coefficients are all positive or all negative. No nonvanishing hypothesis is needed: a zero coefficient makes the corresponding basis vector isotropic and rules out both alternatives.

theorem QuadraticForm.sigPos_weightedSumSquares_signType {ι : Type u_1} [Fintype ι] (u : ι → SignType) : sigPos (QuadraticMap.weightedSumSquares ℝ fun (i : ι) => ↑(u i)) = {i : ι | u i = 1}.ncard

The positive index of inertia of a sign-weighted sum of squares counts the weights 1.

theorem QuadraticForm.sigNeg_weightedSumSquares_signType {ι : Type u_1} [Fintype ι] (u : ι → SignType) : sigNeg (QuadraticMap.weightedSumSquares ℝ fun (i : ι) => ↑(u i)) = {i : ι | u i = -1}.ncard

The negative index of inertia of a sign-weighted sum of squares counts the weights -1.

theorem QuadraticForm.equivalent_iff_finrank_eq_and_sigPos_eq_and_sigNeg_eq {M : Type u_1} {M' : Type u_2} [AddCommGroup M] [Module ℝ M] [AddCommGroup M'] [Module ℝ M'] [FiniteDimensional ℝ M] [FiniteDimensional ℝ M'] (Q : QuadraticForm ℝ M) (Q' : QuadraticForm ℝ M') : QuadraticMap.Equivalent Q Q' ↔ Module.finrank ℝ M = Module.finrank ℝ M' ∧ sigPos Q = sigPos Q' ∧ sigNeg Q = sigNeg Q'

Sylvester's law of inertia, classification form: two real quadratic forms on finite-dimensional spaces are isometric exactly when their dimensions agree and both indices of inertia agree. The dimension is a genuine third condition: it records the number of zero weights in a diagonalization, which the two indices do not see.

theorem QuadraticForm.equivalent_iff_sigPos_eq_and_sigNeg_eq {M : Type u_1} {M' : Type u_2} [AddCommGroup M] [Module ℝ M] [AddCommGroup M'] [Module ℝ M'] [FiniteDimensional ℝ M] [FiniteDimensional ℝ M'] {Q : QuadraticForm ℝ M} {Q' : QuadraticForm ℝ M'} (hQ : QuadraticMap.Nondegenerate) (hQ' : QuadraticMap.Nondegenerate) : QuadraticMap.Equivalent Q Q' ↔ sigPos Q = sigPos Q' ∧ sigNeg Q = sigNeg Q'

Sylvester's law of inertia for regular forms: two nondegenerate real quadratic forms are isometric exactly when their signatures agree.

def QuadraticForm.realSignatureForm (p q : ℕ) : QuadraticForm ℝ (Fin p ⊕ Fin q → ℝ)

The normal form of signature (p, q): the orthogonal sum of p copies of ⟨1⟩ and q copies of ⟨-1⟩.

theorem QuadraticForm.realSignatureForm_def (p q : ℕ) : realSignatureForm p q = QuadraticMap.weightedSumSquares ℝ (Sum.elim (fun (x : Fin p) => 1) fun (x : Fin q) => -1)

The normal form is the weighted sum of squares with p positive and q negative weights.

@[simp]

theorem QuadraticForm.realSignatureForm_apply (p q : ℕ) (x : Fin p ⊕ Fin q → ℝ) : (realSignatureForm p q) x = ∑ i : Fin p, x (Sum.inl i) ^ 2 - ∑ j : Fin q, x (Sum.inr j) ^ 2

@[simp]

theorem QuadraticForm.sigPos_realSignatureForm (p q : ℕ) : sigPos (realSignatureForm p q) = p

The positive index of inertia of the normal form realSignatureForm p q is p.

@[simp]

theorem QuadraticForm.sigNeg_realSignatureForm (p q : ℕ) : sigNeg (realSignatureForm p q) = q

The negative index of inertia of the normal form realSignatureForm p q is q.

@[simp]

theorem QuadraticForm.nondegenerate_realSignatureForm (p q : ℕ) : QuadraticMap.Nondegenerate

The normal form of signature (p, q) is regular, so every signature is realized by a regular real quadratic form.

@[simp]

theorem QuadraticForm.equivalent_realSignatureForm_iff_sigPos_eq_and_sigNeg_eq {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} (hQ : QuadraticMap.Nondegenerate) (p q : ℕ) : QuadraticMap.Equivalent Q (realSignatureForm p q) ↔ sigPos Q = p ∧ sigNeg Q = q

A regular real quadratic form is isometric to the normal form of signature (p, q) exactly when its positive and negative indices are p and q.

theorem QuadraticForm.equivalent_realSignatureForm_iff (p q p' q' : ℕ) : QuadraticMap.Equivalent (realSignatureForm p q) (realSignatureForm p' q') ↔ p = p' ∧ q = q'

Two normal forms are isometric exactly when their signatures coincide, so the signature is a complete and independent system of invariants for regular real quadratic forms.

theorem QuadraticForm.equivalent_realSignatureForm {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hQ : QuadraticMap.Nondegenerate) : QuadraticMap.Equivalent Q (realSignatureForm (sigPos Q) (sigNeg Q))

Every regular real quadratic form is isometric to the normal form of its signature.

theorem QuadraticForm.equivalent_weightedSumSquares_ite_lt_sigNeg {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hQ : QuadraticMap.Nondegenerate) : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ fun (i : Fin (Module.finrank ℝ M)) => if ↑i < sigNeg Q then -1 else 1)

Sylvester's normal form with the negative squares first. A regular real quadratic form Q on an n-dimensional space is isometric to the diagonal form -x₀² - ⋯ - x_{q-1}² + x_q² + ⋯ + x_{n-1}² on Fin n → ℝ, where q = sigNeg Q. This is the coordinate order of Morse charts, in which the negative directions of a Hessian come first.

theorem QuadraticForm.exists_nondegenerate_and_sigPos_eq_and_sigNeg_eq {n p : ℕ} (h : p ≤ n) : ∃ (Q : QuadraticForm ℝ (Fin n → ℝ)), QuadraticMap.Nondegenerate ∧ sigPos Q = p ∧ sigNeg Q = n - p

Every signature (p, n - p) with p ≤ n is the signature of a regular quadratic form on the coordinate space ℝⁿ: the normal form realSignatureForm p (n - p) transported along a bijection of its index type with Fin n.

theorem TauCeti.nonempty_isometryEquiv_toQuadraticForm'_one_of_posDef {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Q : QuadraticForm ℝ V} (hQ : QuadraticMap.PosDef Q) : Nonempty (QuadraticMap.IsometryEquiv Q (Matrix.toQuadraticForm' 1))

A positive definite real quadratic form is isometric to the standard sum-of-squares form in its dimension.