Classification of regular quadratic forms over a local field

Over a nonarchimedean local field in which two is invertible, the rank, plain discriminant, and local Hasse invariant form a complete set of invariants for regular quadratic forms. The classification applies to isometry classes and to forms on arbitrary finite-dimensional spaces, including the zero space. No restriction on the residue characteristic is imposed. Because the rank is part of the invariant tuple, the signed discriminant may replace the plain one.

Two spaces of positive dimension whose dimensions sum to at least five represent a common nonzero value: their difference is isotropic by the local isotropy bound. In dimensions at least three, this allows a common line to be split off and the classification to be reduced inductively to the binary criterion. The diagonal-chain API aligns the represented value with the leading coefficient; the orthogonal-sum formulas recover the invariants of the tails.

In particular, a class is the sum of m hyperbolic planes exactly when it has rank 2m, discriminant m · [-1] and local Hasse invariant (-1, -1)_K^{m(m-1)/2}.

Since the local Hasse invariant takes only the values ±1, a rank and a discriminant leave at most two classes, with opposite Hasse invariants. Consequently, if p ≠ p' share their rank and discriminant, then p ⊥ x ≅ p' ⊥ y for any classes x ≠ y that share their rank and discriminant.

References

• J.-P. Serre, A Course in Arithmetic, Chapter IV, §2.3, Theorem 7.
• O. T. O'Meara, Introduction to Quadratic Forms, §63:20.

theorem TauCeti.RegularFormClass.eq_of_discr_eq_of_localHasse_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x y : RegularFormClass K} (hrank : x.rank = y.rank) (hd : x.discr = y.discr) (hs : x.localHasse = y.localHasse) : x = y

Local classification. Equal rank, plain discriminant, and local Hasse invariant determine the isometry class of a regular quadratic form.

theorem TauCeti.RegularFormClass.eq_iff_rank_eq_and_discr_eq_and_localHasse_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x y : RegularFormClass K} : x = y ↔ x.rank = y.rank ∧ x.discr = y.discr ∧ x.localHasse = y.localHasse

The complete local invariant criterion, including equality of ranks.

theorem TauCeti.RegularFormClass.eq_iff_rank_eq_and_signedDiscr_eq_and_localHasse_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x y : RegularFormClass K} : x = y ↔ x.rank = y.rank ∧ x.signedDiscr = y.signedDiscr ∧ x.localHasse = y.localHasse

The complete local invariant criterion with the signed discriminant. Since the rank is part of the tuple, the signed discriminant may replace the plain one.

theorem TauCeti.RegularFormClass.eq_nsmul_hyperbolicClass_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x : RegularFormClass K} {m : ℕ} : x = m • hyperbolicClass K ↔ x.rank = 2 * m ∧ x.discr = m • squareClass (-1) ∧ x.localHasse = hilbertSymbol (-1) (-1) ^ m.choose 2

The local invariants of a hyperbolic space. A class is the sum of m hyperbolic planes exactly when it has rank 2m, discriminant m · [-1] and local Hasse invariant (-1, -1)_K^{m(m-1)/2}.

theorem TauCeti.RegularFormClass.localHasse_eq_neg_of_ne {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x y : RegularFormClass K} (hrank : x.rank = y.rank) (hd : x.discr = y.discr) (hne : x ≠ y) : x.localHasse = -y.localHasse

At most two classes of each rank and discriminant. Distinct classes with the same rank and plain discriminant have opposite local Hasse invariants.

theorem TauCeti.RegularFormClass.add_eq_add_iff_ne {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {p p' x y : RegularFormClass K} (hpr : p.rank = p'.rank) (hpd : p.discr = p'.discr) (hp : p ≠ p') (hxr : x.rank = y.rank) (hxd : x.discr = y.discr) : p + x = p' + y ↔ x ≠ y

Exchanging two pairs of distinct classes. Let p ≠ p' be classes with the same rank and plain discriminant, and let x, y be classes with the same rank and plain discriminant. Then p + x = p' + y, that is p ⊥ x ≅ p' ⊥ y, exactly when x ≠ y.

theorem QuadraticForm.equivalent_iff_finrank_eq_and_discr_eq_and_localHasse_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {V : Type u_2} {W : Type u_3} [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) : QuadraticMap.Equivalent Q R ↔ Module.finrank K V = Module.finrank K W ∧ (TauCeti.formClass Q hQ).discr = (TauCeti.formClass R hR).discr ∧ (TauCeti.formClass Q hQ).localHasse = (TauCeti.formClass R hR).localHasse

Local classification. Two regular local quadratic forms are isometric exactly when their dimensions, plain discriminants, and local Hasse invariants agree.