The quaternion subgroup over a local field

Over a nonarchimedean local field in which two is invertible, the subgroup of the Brauer group generated by quaternion classes has exactly two elements: the split class and the unique quaternion division class. Its canonical isomorphism with ℤˣ sends the split class to 1 and the division class to -1. On quaternion symbols it is the norm-equation Hilbert symbol.

Main results

• TauCeti.BrauerGroup.natCard_quaternionSubgroup: the quaternion subgroup has two elements.
• TauCeti.BrauerGroup.quaternionSubgroupSignEquiv: the canonical sign isomorphism.
• TauCeti.BrauerGroup.quaternionSubgroupSignEquiv_apply_quaternionClass: its value on a symbol.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapters V, §3 and VI, §2.
• J.-P. Serre, A Course in Arithmetic, Chapter IV, §2.

theorem TauCeti.BrauerGroup.mem_quaternionSubgroup_iff_of_hilbertSymbol_eq_neg_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {a b : Kˣ} (hab : hilbertSymbol a b = -1) (x : BrauerGroup K) : x ∈ quaternionSubgroup K ↔ x = 1 ∨ x = quaternionClass a b

Fixing any quaternion division class identifies the quaternion subgroup with the two classes 1 and that division class.

@[simp]

theorem TauCeti.BrauerGroup.mem_quaternionSubgroup_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x : BrauerGroup K) : x ∈ quaternionSubgroup K ↔ ∃ (a : Kˣ) (b : Kˣ), quaternionClass a b = x

Over a local field every product of quaternion classes is itself a quaternion class.

theorem TauCeti.BrauerGroup.natCard_quaternionSubgroup {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] : Nat.card ↥(quaternionSubgroup K) = 2

The quaternion subgroup of a local field has exactly two elements.

noncomputable def TauCeti.BrauerGroup.quaternionSubgroupSignEquiv {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] : ↥(quaternionSubgroup K) ≃* ℤˣ

The canonical sign isomorphism on quaternion Brauer classes: it sends the split class to 1 and the quaternion division class to -1.

@[simp]

theorem TauCeti.BrauerGroup.quaternionSubgroupSignEquiv_apply_quaternionClass {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (a b : Kˣ) : quaternionSubgroupSignEquiv ⟨quaternionClass a b, ⋯⟩ = hilbertSymbol a b

On a quaternion class the sign isomorphism is the norm-equation Hilbert symbol.