Realization of local invariants of quadratic forms

Let K be a nonarchimedean local field in which 2 is invertible, in any residue characteristic. A regular quadratic form over K has three invariants: its rank n, its discriminant d ∈ Kˣ/(Kˣ)² and its local Hasse invariant s ∈ {±1}. This file determines exactly which triples (n, d, s) with n ≥ 1 occur: all of them, except n = 1 with s = -1, and n = 2 with d = [-1] and s = -1.

Both exceptions are forced. A form of rank one has the empty Hasse product, and a binary form of discriminant [-1] is the hyperbolic plane ⟨1, -1⟩, whose Hasse invariant is (1, -1)_K = 1 (TauCeti.RegularFormClass.localHasse_eq_one_of_rank_le_one and TauCeti.RegularFormClass.localHasse_eq_one_of_rank_eq_two_of_discr_eq_neg_one). Conversely, ⟨a, a δ⟩ has discriminant [δ] and Hasse invariant (a, -δ)_K, which is -1 for a suitable a as soon as -δ is a nonsquare, by nondegeneracy of the Hilbert symbol. In rank three one adds a rank-one form ⟨c⟩ to such a binary form, with c chosen so that the binary form falls outside the second exception, and in higher rank one adds copies of ⟨1⟩, which change none of the invariants.

This is the existence half of the classification of regular forms over K by (n, d, s), and the local input to the realization of admissible systems of invariants over a number field.

Main results

• TauCeti.RegularFormClass.exists_of_realization: every triple (n, d, s) with n ≥ 1 outside the two exceptions is the rank, discriminant and local Hasse invariant of a regular form.
• TauCeti.RegularFormClass.exists_rank_eq_discr_eq_localHasse_eq_iff: the realizable triples of positive rank are exactly those outside the two exceptions.

References

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

theorem TauCeti.RegularFormClass.exists_of_realization {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {n : ℕ} (hn : 1 ≤ n) (d : SquareClassGroup K) (s : ℤˣ) (h₁ : n = 1 → s = 1) (h₂ : n = 2 → d = squareClass (-1) → s = 1) : ∃ (x : RegularFormClass K), x.rank = n ∧ x.discr = d ∧ x.localHasse = s

Realization of local invariants (O'Meara 63:23, Serre IV Prop 6). Over a nonarchimedean local field, every triple (n, d, s) of a rank n ≥ 1, a square class d and a sign s is the rank, discriminant and local Hasse invariant of a regular form, except when n = 1 and s = -1, or when n = 2, d = [-1] and s = -1. The two hypotheses exclude exactly these cases, and both exclusions are necessary (exists_rank_eq_discr_eq_localHasse_eq_iff).

theorem TauCeti.RegularFormClass.exists_rank_eq_discr_eq_localHasse_eq_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {n : ℕ} (hn : 1 ≤ n) (d : SquareClassGroup K) (s : ℤˣ) : (∃ (x : RegularFormClass K), x.rank = n ∧ x.discr = d ∧ x.localHasse = s) ↔ (n = 1 → s = 1) ∧ (n = 2 → d = squareClass (-1) → s = 1)

The realizable local invariants (O'Meara 63:23, Serre IV Prop 6). For n ≥ 1, a regular form of rank n, discriminant d and local Hasse invariant s exists if and only if neither n = 1 and s = -1, nor n = 2, d = [-1] and s = -1.