The index theorem for quadratic norms, and bimultiplicativity of the local Hilbert symbol

Let K be a nonarchimedean local field with 2 ≠ 0, in any residue characteristic. The norms from K(√a), that is the subgroup N of Kˣ consisting of the b of the form x² - a y² with x, y ∈ K, form a subgroup of index two in Kˣ for every nonsquare radicand a.

For odd-valuation radicands the index is computed directly from the base field's unit norm families by TauCeti.quadraticNormSubgroup_index_eq_two_of_odd. For the remaining radicands, the index is computed by counting square classes in a quadratic extension, uniformly in the residue characteristic and quadratic defect. For L = K(√a), TauCeti.two_mul_index_quadraticNormSubgroup_mul_card_squareClass gives 2 · (Kˣ : N) · #(Lˣ/(Lˣ)²) = #(Kˣ/(Kˣ)²)² over any field with 2 ≠ 0. Over a local field #(Kˣ/(Kˣ)²) = 4 q^{v_K(2)}, with q = #𝓀[K], and since [L : K] = 2, TauCeti.card_squareClass_eq_four_mul_pow_finrank gives #(Lˣ/(Lˣ)²) = 4 q^{2 v_K(2)}. Hence (Kˣ : N) = 2.

The sign indicator of an index-two subgroup is a character, so the local Hilbert symbol is bimultiplicative in both arguments. The same index theorem gives nondegeneracy, and there that step is purely group-theoretic: the sign indicator of a proper subgroup of index two is onto, so it takes the value -1 off the subgroup. The field-level statement is TauCeti.exists_hilbertSymbol_eq_neg_one_of_index_eq_two, which asks only that the norm subgroup of a have index two.

Nondegeneracy has two consequences for prescribing values of the symbol. Two distinct nontrivial characters (·, a)_K and (·, b)_K of the group Kˣ/(Kˣ)² of exponent two take every pair of values. And the norm group of K(√a) contains a nonsquare for every a: among a uniformizer, the unramified unit and their product, three nonsquares, the symbols with a multiply to 1.

The diagonal entry (a, a)_K = (a, -1)_K needs no arithmetic input and is stated for an arbitrary field in TauCeti.NumberTheory.HilbertSymbol.NormSubgroup, as TauCeti.hilbertSymbol_self.

Main results

• TauCeti.quadraticNormSubgroup_index_eq_two_of_not_isSquare: the norm index of every nonsquare radicand.
• TauCeti.hilbertSymbol_mul_right and TauCeti.hilbertSymbol_mul_left: the Hilbert symbol is bilinear in both arguments.
• TauCeti.exists_hilbertSymbol_eq_neg_one: for every nonsquare a there is a b with (a, b)_K = -1.
• TauCeti.exists_hilbertSymbol_eq_and_hilbertSymbol_eq: for nonsquares a, b with ab a nonsquare, the characters (·, a)_K and (·, b)_K take every pair of values.
• TauCeti.exists_not_isSquare_hilbertSymbol_eq_one: the norm group of K(√a) contains a nonsquare, for every a.
• TauCeti.uncurry_hilbertSymbol_surjective: the Hilbert symbol takes both values ±1.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §63A.
• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapter VI, §2.
• J.-P. Serre, A Course in Arithmetic, Chapter III, §1, Theorem 2.

theorem TauCeti.quadraticNormSubgroup_index_eq_two_of_not_isSquare {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {a : Kˣ} (ha : ¬IsSquare a) : (quadraticNormSubgroup ↑a).index = 2

The norm index of a nonsquare radicand. If 2 ≠ 0 in K, the norms from K(√a) form a subgroup of index two in Kˣ for every a that is not a square.

@[simp]

theorem TauCeti.hilbertSymbol_mul_right {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) (a b c : Kˣ) : hilbertSymbol a (b * c) = hilbertSymbol a b * hilbertSymbol a c

Bimultiplicativity of the local Hilbert symbol in the second argument. If 2 ≠ 0 in K, then (a, bc)_K = (a, b)_K (a, c)_K for every a, b and c.

@[simp]

theorem TauCeti.hilbertSymbol_mul_left {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) (a b c : Kˣ) : hilbertSymbol (b * c) a = hilbertSymbol b a * hilbertSymbol c a

Bimultiplicativity of the local Hilbert symbol in the first argument. If 2 ≠ 0 in K, then (bc, a)_K = (b, a)_K (c, a)_K for every a, b and c.

@[simp]

theorem TauCeti.hilbertSymbol_zpow_right {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) (a b : Kˣ) (n : ℤ) : hilbertSymbol a (b ^ n) = hilbertSymbol a b ^ n

The Hilbert symbol is multiplicative on integer powers of its second argument.

@[simp]

theorem TauCeti.hilbertSymbol_zpow_left {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) (a b : Kˣ) (n : ℤ) : hilbertSymbol (a ^ n) b = hilbertSymbol a b ^ n

The Hilbert symbol is multiplicative on integer powers of its first argument.

@[simp]

theorem TauCeti.hilbertSymbol_pow_left {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) (a b : Kˣ) (n : ℕ) : hilbertSymbol (a ^ n) b = hilbertSymbol a b ^ n

The Hilbert symbol is multiplicative on natural-number powers of its first argument.

theorem TauCeti.exists_hilbertSymbol_eq_neg_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {a : Kˣ} (ha : ¬IsSquare a) : ∃ (b : Kˣ), hilbertSymbol a b = -1

Nondegeneracy of the local Hilbert symbol. If 2 ≠ 0 in K, then for every nonsquare a there is a b ∈ Kˣ with (a, b)_K = -1. It is the field-level consequence TauCeti.exists_hilbertSymbol_eq_neg_one_of_index_eq_two of the norm index theorem.

Prescribing values of the Hilbert symbol

theorem TauCeti.exists_hilbertSymbol_eq_and_hilbertSymbol_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {a b : Kˣ} (ha : ¬IsSquare a) (hb : ¬IsSquare b) (hab : ¬IsSquare (a * b)) (s t : ℤˣ) : ∃ (x : Kˣ), hilbertSymbol x a = s ∧ hilbertSymbol x b = t

Two distinct nontrivial characters take every pair of values. If 2 ≠ 0 in K, then for nonsquares a, b with ab a nonsquare, every pair of signs (s, t) is ((x, a)_K, (x, b)_K) for some x ∈ Kˣ.

theorem TauCeti.exists_not_isSquare_hilbertSymbol_eq_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) (a : Kˣ) : ∃ (b : Kˣ), ¬IsSquare b ∧ hilbertSymbol b a = 1

The norm group of K(√a) contains a nonsquare. If 2 ≠ 0 in K, then for every a ∈ Kˣ there is a nonsquare b with (b, a)_K = 1: among a uniformizer π, the unramified unit Δ and their product, three nonsquares, the symbols with a multiply to 1, so one of them is 1.

theorem TauCeti.uncurry_hilbertSymbol_surjective {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Function.Surjective (Function.uncurry hilbertSymbol)

The local Hilbert symbol takes both values. Every sign ±1 is (a, b)_K for some a, b ∈ Kˣ; when 2 ≠ 0 in K, in particular some quaternion algebra ℍ[K,a,b] is a division algebra.