The local Hilbert symbol as a nondegenerate symmetric bilinear form

Let K be a nonarchimedean local field in which 2 is invertible, in any residue characteristic. The Hilbert symbol (a, b)_K ∈ {±1} only depends on the square classes of a and b, so it is a pairing on the finite 𝔽₂-vector space Kˣ/(Kˣ)². Read additively through the sign dictionary +1 ↦ 0, -1 ↦ 1 (TauCeti.hilbertSign), this pairing is a nondegenerate symmetric 𝔽₂-bilinear form TauCeti.hilbertSymbolForm on TauCeti.SquareClassGroup K.

The three properties are the square-class forms of the field-level results: symmetry is TauCeti.hilbertSymbol_comm, bilinearity is the bimultiplicativity TauCeti.hilbertSymbol_mul_right coming from the norm index theorem, and nondegeneracy is TauCeti.exists_hilbertSymbol_eq_neg_one.

Over a finite extension of ℚ_2 there is no closed formula for the symbol of Serre's shape, and this form, on a group of order 4 · q ^ e (TauCeti.natCard_squareClassGroup_dyadic), is what determines it: a finite Gram matrix in any 𝔽₂-basis of the square classes. Over ℚ_2 that matrix is TauCeti.toMatrix_hilbertSymbolForm_padicTwo.

Main definitions

• TauCeti.hilbertSymbolForm: the Hilbert symbol as a ZMod 2-bilinear form on the square-class group.

Main results

• TauCeti.hilbertSymbolOnSquareClasses_add_left and TauCeti.hilbertSymbolOnSquareClasses_add_right: the symbol on square classes is bimultiplicative.
• TauCeti.exists_hilbertSymbolOnSquareClasses_eq_neg_one: every nonzero square class pairs to -1 with some square class.
• TauCeti.hilbertSign_hilbertSymbolForm, TauCeti.hilbertSymbolForm_eq_zero_iff and TauCeti.hilbertSymbolForm_eq_one_iff: the sign of the form is the Hilbert symbol.
• TauCeti.isSymm_hilbertSymbolForm and TauCeti.nondegenerate_hilbertSymbolForm: the form is symmetric and nondegenerate.

References

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

The symbol on square classes

theorem TauCeti.hilbertSymbolOnSquareClasses_add_right {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x y z : SquareClassGroup K) : hilbertSymbolOnSquareClasses x (y + z) = hilbertSymbolOnSquareClasses x y * hilbertSymbolOnSquareClasses x z

Bimultiplicativity on square classes, in the second argument. Over a nonarchimedean local field in which 2 is invertible, (x, y + z)_K = (x, y)_K · (x, z)_K for square classes.

theorem TauCeti.hilbertSymbolOnSquareClasses_add_left {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x y z : SquareClassGroup K) : hilbertSymbolOnSquareClasses (x + y) z = hilbertSymbolOnSquareClasses x z * hilbertSymbolOnSquareClasses y z

Bimultiplicativity on square classes, in the first argument. Over a nonarchimedean local field in which 2 is invertible, (x + y, z)_K = (x, z)_K · (y, z)_K for square classes.

theorem TauCeti.exists_hilbertSymbolOnSquareClasses_eq_neg_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {x : SquareClassGroup K} (hx : x ≠ 0) : ∃ (y : SquareClassGroup K), hilbertSymbolOnSquareClasses x y = -1

Nondegeneracy on square classes. Over a nonarchimedean local field in which 2 is invertible, every nonzero square class x has (x, y)_K = -1 for some square class y.

The bilinear form

noncomputable def TauCeti.hilbertSymbolForm (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] : LinearMap.BilinForm (ZMod 2) (SquareClassGroup K)

The Hilbert symbol as a bilinear form over 𝔽₂. Over a nonarchimedean local field in which 2 is invertible, the Hilbert symbol on square classes, read in ZMod 2 through the dictionary +1 ↦ 0, -1 ↦ 1, is a ZMod 2-bilinear form on Kˣ/(Kˣ)². Its sign is the symbol (TauCeti.hilbertSign_hilbertSymbolForm).

theorem TauCeti.hilbertSymbolForm_apply {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x y : SquareClassGroup K) : ((hilbertSymbolForm K) x) y = additiveIntUnitsAddEquiv (Additive.ofMul (hilbertSymbolOnSquareClasses x y))

The Hilbert symbol form is the Hilbert symbol on square classes, read in ZMod 2 through TauCeti.additiveIntUnitsAddEquiv.

@[simp]

theorem TauCeti.hilbertSign_hilbertSymbolForm {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x y : SquareClassGroup K) : hilbertSign (((hilbertSymbolForm K) x) y) = hilbertSymbolOnSquareClasses x y

The sign of the Hilbert symbol form is the Hilbert symbol.

theorem TauCeti.hilbertSymbolForm_eq_zero_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x y : SquareClassGroup K) : ((hilbertSymbolForm K) x) y = 0 ↔ hilbertSymbolOnSquareClasses x y = 1

The Hilbert symbol form vanishes exactly where the Hilbert symbol is +1.

theorem TauCeti.hilbertSymbolForm_eq_one_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (x y : SquareClassGroup K) : ((hilbertSymbolForm K) x) y = 1 ↔ hilbertSymbolOnSquareClasses x y = -1

The Hilbert symbol form is 1 exactly where the Hilbert symbol is -1.

theorem TauCeti.isSymm_hilbertSymbolForm {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] : (hilbertSymbolForm K).IsSymm

The Hilbert symbol form is symmetric.

theorem TauCeti.nondegenerate_hilbertSymbolForm {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] : (hilbertSymbolForm K).Nondegenerate

The Hilbert symbol form is nondegenerate. A square class x with (x, y)_K = +1 for every square class y is trivial, in either argument.