The anisotropic quaternary form and the quaternion division algebra over a local field

Let K be a nonarchimedean local field in which 2 is invertible. By the quaternary isotropy criterion, a regular form of rank four over K is anisotropic exactly when its discriminant is trivial and its local Hasse invariant is -(-1, -1)_K. These invariants do not depend on the form, so by the local classification there is exactly one anisotropic regular quaternary form over K up to isometry. It is the norm form <<a, b>> = <1, -a, -b, ab> of every quaternion division algebra ℍ[K,a,b], that is of every ℍ[K,a,b] with (a, b)_K = -1.

Two quaternion division algebras over K therefore have isometric norm forms. Witt cancellation of the common summand <1> leaves isometric pure norm forms <-a, -b, ab> and <-c, -d, cd>, whose Hasse invariants [(a, b)] · [(-1, -1)] and [(c, d)] · [(-1, -1)] agree. So ℍ[K,a,b] and ℍ[K,c,d] have the same Brauer class and are isomorphic. Since the split quaternion algebras are all isomorphic to M₂(K), the Hilbert symbol (a, b)_K is a complete invariant of ℍ[K,a,b], and there are exactly two quaternion algebras over K up to isomorphism; both occur, because the Hilbert symbol takes both values (TauCeti.uncurry_hilbertSymbol_surjective).

Over ℚ_2, where (-1, -1) = -1, the anisotropic quaternary form is the sum of four squares <1, 1, 1, 1>, the norm form of Hamilton's quaternions.

Main results

• TauCeti.RegularFormClass.eq_of_rank_eq_four_of_anisotropic: two anisotropic regular-form classes of rank four over K are equal.
• TauCeti.RegularFormClass.anisotropic_iff_eq_pfisterFormClass_two: if (a, b)_K = -1, a class of rank four is anisotropic exactly when it is the class of <<a, b>>.
• QuadraticForm.equivalent_of_finrank_eq_four_of_anisotropic: two anisotropic quadratic forms on spaces of dimension four over K are isometric.
• TauCeti.QuaternionAlgebra.nonempty_algEquiv_iff_hilbertSymbol_eq: two quaternion algebras over K are isomorphic exactly when their Hilbert symbols agree.
• TauCeti.QuaternionAlgebra.nonempty_algEquiv_of_hilbertSymbol_eq_neg_one: any two quaternion division algebras over K are isomorphic.
• TauCeti.BrauerGroup.quaternionClass_eq_iff_hilbertSymbol_eq: two quaternion symbols over K have the same Brauer class exactly when their Hilbert symbols agree.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §63:17–63:18.
• J.-P. Serre, A Course in Arithmetic, Chapter IV, §2.3, Theorem 7 and its corollary.
• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapter VI, §2.

theorem TauCeti.RegularFormClass.eq_of_rank_eq_four_of_anisotropic {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x y : RegularFormClass K} (hx : x.rank = 4) (hy : y.rank = 4) (hxa : x.Anisotropic) (hya : y.Anisotropic) : x = y

The anisotropic quaternary form is unique (O'Meara 63:17, Serre IV Thm 7 cor.). Two anisotropic regular-form classes of rank four over K are equal: both have trivial discriminant and local Hasse invariant -(-1, -1)_K.

theorem TauCeti.RegularFormClass.anisotropic_iff_eq_pfisterFormClass_two {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x : RegularFormClass K} (hx : x.rank = 4) {a b : Kˣ} (hab : hilbertSymbol a b = -1) : x.Anisotropic ↔ x = pfisterFormClass ![a, b]

The anisotropic quaternary form is a norm form. If (a, b)_K = -1, that is if ℍ[K,a,b] is a division algebra, then a regular-form class of rank four over K is anisotropic exactly when it is the class of the norm form <<a, b>> = <1, -a, -b, ab> of ℍ[K,a,b].

theorem TauCeti.RegularFormClass.pfisterFormClass_two_eq_of_hilbertSymbol_eq_neg_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {a b c d : Kˣ} (hab : hilbertSymbol a b = -1) (hcd : hilbertSymbol c d = -1) : pfisterFormClass ![a, b] = pfisterFormClass ![c, d]

The norm forms of two quaternion division algebras are isometric. If (a, b)_K = -1 and (c, d)_K = -1, then <<a, b>> = <<c, d>>.

theorem TauCeti.BrauerGroup.quaternionClass_eq_iff_hilbertSymbol_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (a b c d : Kˣ) : quaternionClass a b = quaternionClass c d ↔ hilbertSymbol a b = hilbertSymbol c d

The Brauer class of a quaternion algebra over a local field is its Hilbert symbol: two quaternion symbols over K have the same Brauer class exactly when their Hilbert symbols agree.

theorem TauCeti.QuaternionAlgebra.nonempty_algEquiv_iff_hilbertSymbol_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (a b c d : Kˣ) : Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] QuaternionAlgebra K (↑c) 0 ↑d) ↔ hilbertSymbol a b = hilbertSymbol c d

Quaternion algebras over a local field are classified by the Hilbert symbol: ℍ[K,a,b] and ℍ[K,c,d] are isomorphic exactly when (a, b)_K = (c, d)_K. Since the symbol takes both values (TauCeti.uncurry_hilbertSymbol_surjective), there are exactly two quaternion algebras over K up to isomorphism: M₂(K) and the quaternion division algebra.

theorem TauCeti.QuaternionAlgebra.nonempty_algEquiv_of_hilbertSymbol_eq_neg_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {a b c d : Kˣ} (hab : hilbertSymbol a b = -1) (hcd : hilbertSymbol c d = -1) : Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] QuaternionAlgebra K (↑c) 0 ↑d)

The quaternion division algebra over a local field is unique: if (a, b)_K = -1 and (c, d)_K = -1, then ℍ[K,a,b] and ℍ[K,c,d] are isomorphic.

theorem QuadraticForm.equivalent_of_finrank_eq_four_of_anisotropic {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} {R : QuadraticForm K W} (hV : Module.finrank K V = 4) (hW : Module.finrank K W = 4) (hQ : QuadraticMap.Anisotropic Q) (hR : QuadraticMap.Anisotropic R) : QuadraticMap.Equivalent Q R

The anisotropic quaternary form is unique (O'Meara 63:17, Serre IV Thm 7 cor.). Two anisotropic quadratic forms on spaces of dimension four over K are isometric.