The discriminant of a regular real quadratic form

Over ℝ the square class of a nonzero number is its sign, so the discriminant of a regular form only records the sign of the product of the weights of a diagonalization. By Sylvester's law of inertia that sign is (-1)^q, where q = sigNeg Q is the negative index of inertia. This is the determinant-sign formula sign (det Q) = (-1)^q, stated in the square-class group.

In particular the discriminant of a regular real form is determined by its signature, and it is trivial exactly when the negative index is even.

Main results

• QuadraticForm.discr_formClass_eq_sigNeg_nsmul: the discriminant of a regular real form is sigNeg Q • [-1].
• QuadraticForm.discr_formClass_eq_zero_iff_even_sigNeg: it is trivial exactly when sigNeg Q is even.
• TauCeti.discr_formClass_realSignatureForm: the normal form of signature (p, q) has discriminant q • [-1].

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter II, §3.

theorem QuadraticForm.discr_formClass_eq_sigNeg_nsmul {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hQ : QuadraticMap.Nondegenerate) : (TauCeti.formClass Q hQ).discr = sigNeg Q • TauCeti.squareClass (-1)

The determinant-sign formula. The discriminant of a regular real quadratic form is the class of (-1)^q, where q is its negative index of inertia.

@[simp]

theorem QuadraticForm.discr_formClass_eq_zero_iff_even_sigNeg {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hQ : QuadraticMap.Nondegenerate) : (TauCeti.formClass Q hQ).discr = 0 ↔ Even (sigNeg Q)

The discriminant of a regular real quadratic form is trivial exactly when its negative index of inertia is even.

@[simp]

theorem TauCeti.discr_formClass_realSignatureForm (p q : ℕ) : (formClass (QuadraticForm.realSignatureForm p q) ⋯).discr = q • squareClass (-1)

The normal form p⟨1⟩ ⊥ q⟨-1⟩ of signature (p, q) has discriminant q • [-1].