Regular quadratic forms of rank at most three

Over a field K in which two is invertible, two regular quadratic forms of the same rank n ≤ 3 are isometric exactly when they have the same discriminant d and the same Hasse invariant s (Lam V.3.21). The bound on the rank cannot be dropped: over ℝ the forms ⟨1, 1, 1, 1⟩ and ⟨-1, -1, -1, -1⟩ both have trivial discriminant and trivial Hasse invariant, since [(-1, -1)]⁶ = 1, and they are not isometric, one being positive and the other negative definite.

The class-level theorem is stated for RegularFormClass K; its form-level counterpart applies to regular forms on finite-dimensional spaces of the same dimension. Use either theorem after proving equality of the rank, discriminant, and Hasse invariant, together with the bound n ≤ 3.

The file also records isotropy in rank two: a regular binary form is isotropic exactly when its discriminant is the class of -1, that is, exactly when it is a hyperbolic plane. Through the isotropy of ⟨-c⟩ ⊥ q, this describes the units represented by a form q of rank one: they are the units in its discriminant square class.

Main results

• TauCeti.RegularFormClass.hasseInvariant_mk_neg_neg_mul: the Hasse invariant of ⟨-a, -b, ab⟩ is [(a, b)] · [(-1, -1)].
• TauCeti.RegularFormClass.exists_eq_mk_neg_neg_mul: a class of rank three and trivial discriminant is the class of some ⟨-a, -b, ab⟩.
• TauCeti.RegularFormClass.eq_iff_discr_eq_and_hasseInvariant_eq: classes of the same rank at most three are equal exactly when their discriminants and Hasse invariants agree.
• QuadraticForm.equivalent_iff_discr_eq_and_hasseInvariant_eq: the same statement for regular forms on finite-dimensional spaces of the same dimension at most three.
• TauCeti.RegularFormClass.not_anisotropic_iff_discr_eq_neg_one_of_rank_eq_two, QuadraticForm.not_anisotropic_iff_discr_eq_neg_one_of_finrank_eq_two: a regular binary form is isotropic exactly when its discriminant is the class of -1.
• QuadraticForm.mem_unitValueSet_iff_squareClass_eq_discr_of_finrank_eq_one: a regular form of dimension one represents exactly the units in its discriminant square class.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Graduate Studies in Mathematics 67, American Mathematical Society (2005), Chapter V, §3, (3.21).

theorem TauCeti.RegularFormClass.eq_of_discr_eq_of_hasseInvariant_eq {K : Type u} [Field K] [Invertible 2] {x y : RegularFormClass K} (hrank : x.rank = y.rank) (h3 : x.rank ≤ 3) (hd : x.discr = y.discr) (hs : x.hasseInvariant = y.hasseInvariant) : x = y

Classification in rank at most three (Lam V.3.21): two regular-form classes of the same rank n ≤ 3 with the same discriminant and the same Hasse invariant are equal.

theorem TauCeti.RegularFormClass.eq_iff_discr_eq_and_hasseInvariant_eq {K : Type u} [Field K] [Invertible 2] {x y : RegularFormClass K} (hrank : x.rank = y.rank) (h3 : x.rank ≤ 3) : x = y ↔ x.discr = y.discr ∧ x.hasseInvariant = y.hasseInvariant

Classification in rank at most three (Lam V.3.21): two regular-form classes of the same rank n ≤ 3 are equal exactly when they have the same discriminant and the same Hasse invariant.

Isotropy in rank two

theorem TauCeti.RegularFormClass.not_anisotropic_iff_discr_eq_neg_one_of_rank_eq_two {K : Type u} [Field K] [Invertible 2] {x : RegularFormClass K} (hx : x.rank = 2) : ¬x.Anisotropic ↔ x.discr = squareClass (-1)

Isotropy in rank two. A regular-form class of rank two is isotropic exactly when its discriminant is the class of -1, that is, exactly when it is the hyperbolic class.

theorem QuadraticForm.equivalent_iff_discr_eq_and_hasseInvariant_eq {K : Type u} [Field K] [Invertible 2] {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {R : QuadraticForm K W} (hR : QuadraticMap.Nondegenerate) (hdim : Module.finrank K V = Module.finrank K W) (h3 : Module.finrank K V ≤ 3) : QuadraticMap.Equivalent Q R ↔ (TauCeti.formClass Q hQ).discr = (TauCeti.formClass R hR).discr ∧ (TauCeti.formClass Q hQ).hasseInvariant = (TauCeti.formClass R hR).hasseInvariant

Classification of regular forms in dimension at most three (Lam V.3.21): two regular quadratic forms on finite-dimensional spaces of the same dimension n ≤ 3 are isometric exactly when they have the same discriminant and the same Hasse invariant.

theorem QuadraticForm.not_anisotropic_iff_discr_eq_neg_one_of_finrank_eq_two {K : Type u} [Field K] [Invertible 2] {V : Type u_1} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 2) : ¬QuadraticMap.Anisotropic Q ↔ (TauCeti.formClass Q hQ).discr = TauCeti.squareClass (-1)

Isotropy in dimension two. A regular quadratic form on a space of dimension two is isotropic exactly when its discriminant is the class of -1.

theorem QuadraticForm.mem_unitValueSet_iff_squareClass_eq_discr_of_finrank_eq_one {K : Type u} [Field K] [Invertible 2] {V : Type u_1} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 1) (c : Kˣ) : c ∈ QuadraticMap.unitValueSet Q ↔ TauCeti.squareClass c = (TauCeti.formClass Q hQ).discr

Representation in dimension one. A regular quadratic form on a space of dimension one represents a unit c exactly when c lies in the discriminant square class.