The local invariants of a quadratic form, and the classification as an equivalence

A regular quadratic form over a nonarchimedean local field K in which 2 is invertible has three invariants: its rank n, its plain discriminant d ∈ Kˣ/(Kˣ)² and its local Hasse invariant s ∈ {±1}. This file bundles them as TauCeti.LocalFormInvariants K, the local counterpart of the global systems TauCeti.NumberField.QuadraticForm.GlobalFormInvariants, and cuts out the admissible triples: those with

• d = [1] and s = 1 in rank zero;
• s = 1 in rank one;
• s = 1 in rank two whenever d = [-1].

The classification of forms over K by (n, d, s) (O'Meara 63:20, Serre IV Thm 7) and the realization of invariants (O'Meara 63:23, Serre IV Prop 6) together say that taking invariants is a bijection from isometry classes onto admissible triples. This is TauCeti.RegularFormClass.localInvariantsEquiv; its inverse is the realization map, sending an admissible triple to the unique class with those invariants.

Over ℚ_2 the binary form ⟨-1, -1⟩ has discriminant [1] and Hasse invariant (-1, -1)_{ℚ_2} = -1, so it realizes (2, [1], -1), while (2, [-1], -1) is excluded. The two discriminants in the rank-two exception therefore cannot be confused with each other.

Main definitions

• TauCeti.LocalFormInvariants: rank, discriminant and Hasse sign.
• TauCeti.LocalFormInvariants.IsAdmissible: the admissibility conditions above.
• TauCeti.RegularFormClass.localInvariants: the invariants of a regular-form class.
• TauCeti.RegularFormClass.localInvariantsEquiv: regular-form classes are in bijection with admissible triples.

Main results

• TauCeti.RegularFormClass.localInvariants_injective: the classification.
• TauCeti.RegularFormClass.range_localInvariants: the realized triples are exactly the admissible ones.
• TauCeti.RegularFormClass.localInvariants_mk_binary: the invariants of ⟨a, b⟩.
• TauCeti.RegularFormClass.localInvariants_neg_one_neg_one_padicTwo: ⟨-1, -1⟩ over ℚ_2 realizes (2, [1], -1).

References

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

structure TauCeti.LocalFormInvariants (K : Type u_1) [Field K] : Type u_1

The local invariants of a regular quadratic form over a field K: a rank n, a discriminant in Kˣ/(Kˣ)², and a Hasse sign in {±1}. The triples that occur over a nonarchimedean local field are cut out by LocalFormInvariants.IsAdmissible.

• rank : ℕ

  The rank.

• discr : SquareClassGroup K

  The plain discriminant, a square class.

• hasse : ℤˣ

  The Hasse sign.

theorem TauCeti.LocalFormInvariants.ext {K : Type u_1} {inst✝ : Field K} {x y : LocalFormInvariants K} (rank : x.rank = y.rank) (discr : x.discr = y.discr) (hasse : x.hasse = y.hasse) : x = y

theorem TauCeti.LocalFormInvariants.ext_iff {K : Type u_1} {inst✝ : Field K} {x y : LocalFormInvariants K} : x = y ↔ x.rank = y.rank ∧ x.discr = y.discr ∧ x.hasse = y.hasse

structure TauCeti.LocalFormInvariants.IsAdmissible {K : Type u_1} [Field K] (I : LocalFormInvariants K) : Prop

Admissibility of a triple of local invariants. A triple (n, d, s) is admissible when d = [1] and s = 1 in rank zero, s = 1 in rank one, and s = 1 in rank two whenever d = [-1]. Over a nonarchimedean local field these are exactly the triples realized by regular forms (TauCeti.RegularFormClass.range_localInvariants).

• discr_eq_zero_of_rank_eq_zero : I.rank = 0 → I.discr = 0

  In rank zero the discriminant is trivial.

• hasse_eq_one_of_rank_le_one : I.rank ≤ 1 → I.hasse = 1

  In rank at most one the Hasse sign is trivial.

• hasse_eq_one_of_rank_eq_two : I.rank = 2 → I.discr = squareClass (-1) → I.hasse = 1

  In rank two the Hasse sign is trivial when the discriminant is the class of -1.

noncomputable def TauCeti.RegularFormClass.localInvariants {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x : RegularFormClass K) : LocalFormInvariants K

The local invariants (n, d, s) of a regular-form class: its rank, its plain discriminant and its local Hasse invariant.

@[simp]

theorem TauCeti.RegularFormClass.rank_localInvariants {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x : RegularFormClass K) : x.localInvariants.rank = x.rank

The rank of localInvariants x is the rank of x.

@[simp]

theorem TauCeti.RegularFormClass.discr_localInvariants {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x : RegularFormClass K) : x.localInvariants.discr = x.discr

The discriminant of localInvariants x is the discriminant of x.

@[simp]

theorem TauCeti.RegularFormClass.hasse_localInvariants {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x : RegularFormClass K) : x.localInvariants.hasse = x.localHasse

The Hasse sign of localInvariants x is the local Hasse invariant of x.

@[simp]

theorem TauCeti.RegularFormClass.localInvariants_zero {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] : localInvariants 0 = { rank := 0, discr := 0, hasse := 1 }

The zero class has invariants (0, [1], 1).

@[simp]

theorem TauCeti.RegularFormClass.localInvariants_mk_binary {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (a b : Kˣ) : localInvariants ⟦⟨2, ![a, b]⟩⟧ = { rank := 2, discr := squareClass (a * b), hasse := hilbertSymbol a b }

The invariants of the binary diagonal class ⟨a, b⟩ are (2, [ab], (a, b)_K).

theorem TauCeti.RegularFormClass.isAdmissible_localInvariants {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x : RegularFormClass K) : x.localInvariants.IsAdmissible

The invariants of every regular-form class are admissible.

theorem TauCeti.RegularFormClass.localInvariants_injective {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] : Function.Injective localInvariants

Local classification (O'Meara 63:20, Serre IV Thm 7). A regular-form class over a nonarchimedean local field is determined by its rank, discriminant and local Hasse invariant.

@[simp]

theorem TauCeti.RegularFormClass.localInvariants_inj {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x y : RegularFormClass K} : x.localInvariants = y.localInvariants ↔ x = y

Two regular-form classes are equal exactly when their local invariants are.

theorem TauCeti.RegularFormClass.range_localInvariants {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] : Set.range localInvariants = {I : LocalFormInvariants K | I.IsAdmissible}

Realization of local invariants (O'Meara 63:23, Serre IV Prop 6). The triples (n, d, s) of rank, discriminant and local Hasse invariant of regular-form classes over a nonarchimedean local field are exactly the admissible ones.

noncomputable def TauCeti.RegularFormClass.localInvariantsEquiv {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] : RegularFormClass K ≃ { I : LocalFormInvariants K // I.IsAdmissible }

The classification of regular forms over a local field, as an equivalence. Taking rank, discriminant and local Hasse invariant is a bijection from regular-form classes over a nonarchimedean local field onto admissible triples. Its inverse is the realization map.

@[simp]

theorem TauCeti.RegularFormClass.coe_localInvariantsEquiv_apply {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x : RegularFormClass K) : ↑(localInvariantsEquiv x) = x.localInvariants

localInvariantsEquiv sends a class to its local invariants.

@[simp]

theorem TauCeti.RegularFormClass.localInvariants_localInvariantsEquiv_symm_apply {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (I : { I : LocalFormInvariants K // I.IsAdmissible }) : (localInvariantsEquiv.symm I).localInvariants = ↑I

The realization map: the class localInvariantsEquiv.symm I has invariants I.

theorem TauCeti.RegularFormClass.localInvariants_neg_one_neg_one_padicTwo : localInvariants ⟦⟨2, ![-1, -1]⟩⟧ = { rank := 2, discr := 0, hasse := -1 }

Worked example over ℚ_2. The binary form ⟨-1, -1⟩ has discriminant [1] and Hasse invariant (-1, -1)_{ℚ_2} = -1, so it realizes the admissible triple (2, [1], -1).