The norm-equation Hilbert symbol

TauCeti.hilbertSymbol a b is the sign +1 when b = x² - a y² is solvable, and -1 otherwise. The definition makes sense over any field. This file supplies the field-generic part of its theory: the quadratic-algebra norm and quaternion splitting criteria, symmetry, square rescaling, invariance under isomorphisms of fields, and the elementary split values.

The comparison theorems reuse the four-fold splitting criterion in TauCeti.Algebra.Quaternion.SplittingCriterion. No local classification enters the definition. In particular, no bimultiplicativity is asserted over an arbitrary field: that property needs a local norm-index theorem.

The symbol factors through square classes, so its value can be computed from any unit representatives.

References

• J.-P. Serre, A Course in Arithmetic, Chapter III, §1, Proposition 1.
• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapter III, §2.7.

noncomputable def TauCeti.hilbertSymbol {K : Type u_1} [Field K] (a b : Kˣ) : ℤˣ

The norm-equation Hilbert symbol, with values in the two integer units.

Equations

• TauCeti.hilbertSymbol a b = if ∃ (x : K) (y : K), ↑b = x ^ 2 - ↑a * y ^ 2 then 1 else -1

theorem TauCeti.hilbertSymbol_def {K : Type u_1} [Field K] (a b : Kˣ) : hilbertSymbol a b = if ∃ (x : K) (y : K), ↑b = x ^ 2 - ↑a * y ^ 2 then 1 else -1

The defining norm equation for the Hilbert symbol.

theorem TauCeti.hilbertSymbol_eq_one_iff {K : Type u_1} [Field K] (a b : Kˣ) : hilbertSymbol a b = 1 ↔ ∃ (x : K) (y : K), ↑b = x ^ 2 - ↑a * y ^ 2

The symbol is positive exactly when the norm equation has a solution.

theorem TauCeti.hilbertSymbol_eq_neg_one_iff {K : Type u_1} [Field K] (a b : Kˣ) : hilbertSymbol a b = -1 ↔ ¬∃ (x : K) (y : K), ↑b = x ^ 2 - ↑a * y ^ 2

The symbol is negative exactly when the norm equation has no solution.

theorem TauCeti.hilbertSymbol_eq_one_iff_exists_norm_eq {K : Type u_1} [Field K] (a b : Kˣ) : hilbertSymbol a b = 1 ↔ ∃ (z : QuadraticAlgebra K (↑a) 0), QuadraticAlgebra.norm z = ↑b

The symbol is positive exactly when the second parameter is a norm from the quadratic algebra, including the split case.

theorem TauCeti.hilbertSymbol_eq_one_iff_exists_unit_norm_eq {K : Type u_1} [Field K] (a b : Kˣ) : hilbertSymbol a b = 1 ↔ ∃ (z : (QuadraticAlgebra K (↑a) 0)ˣ), QuadraticAlgebra.norm ↑z = ↑b

The second parameter is a nonzero norm exactly when it is the norm of a unit.

theorem TauCeti.hilbertSymbol_eq_one_of_isSquare_right {K : Type u_1} [Field K] (a : Kˣ) {b : Kˣ} (hb : IsSquare b) : hilbertSymbol a b = 1

A square second parameter has positive symbol.

@[simp]

theorem TauCeti.hilbertSymbol_one_right {K : Type u_1} [Field K] (a : Kˣ) : hilbertSymbol a 1 = 1

The second parameter 1 has positive symbol.

@[simp]

theorem TauCeti.hilbertSymbol_neg_self {K : Type u_1} [Field K] (a : Kˣ) : hilbertSymbol a (-a) = 1

The norm of the square-root generator is -a.

@[simp]

theorem TauCeti.hilbertSymbol_one_sub {K : Type u_1} [Field K] (a : Kˣ) (h : 1 - ↑a ≠ 0) : hilbertSymbol a (Units.mk0 (1 - ↑a) h) = 1

The Steinberg relation follows from the norm of 1 + √a.

@[simp]

theorem TauCeti.hilbertSymbol_mul_sq_right {K : Type u_1} [Field K] (a b c : Kˣ) : hilbertSymbol a (b * c ^ 2) = hilbertSymbol a b

Multiplying the second parameter by a square does not change the symbol.

@[simp]

theorem TauCeti.hilbertSymbol_mul_sq_left {K : Type u_1} [Field K] (a b c : Kˣ) : hilbertSymbol (a * c ^ 2) b = hilbertSymbol a b

Multiplying the first parameter by a square does not change the symbol.

theorem TauCeti.hilbertSymbol_congr_sq {K : Type u_1} [Field K] (a a' b b' : Kˣ) (ha : IsSquare (a * a')) (hb : IsSquare (b * b')) : hilbertSymbol a b = hilbertSymbol a' b'

The Hilbert symbol depends only on the square classes of its parameters.

@[simp]

theorem TauCeti.hilbertSymbol_units_map_ringEquiv {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) (a b : Kˣ) : hilbertSymbol ((Units.map ↑e) a) ((Units.map ↑e) b) = hilbertSymbol a b

The Hilbert symbol is invariant under a ring isomorphism of fields: the norm equation b = x² - a y² is solvable over K exactly when its image is solvable over L.

noncomputable def TauCeti.hilbertSymbolOnSquareClasses {K : Type u_1} [Field K] (x y : SquareClassGroup K) : ℤˣ

The Hilbert symbol on square classes of a field.

Equations

• TauCeti.hilbertSymbolOnSquareClasses x y = TauCeti.hilbertSymbol (Additive.toMul (Quotient.out x)) (Additive.toMul (Quotient.out y))

@[simp]

theorem TauCeti.hilbertSymbolOnSquareClasses_squareClass {K : Type u_1} [Field K] (a b : Kˣ) : hilbertSymbolOnSquareClasses (squareClass a) (squareClass b) = hilbertSymbol a b

The square-class symbol agrees with the Hilbert symbol on representatives.

@[simp]

theorem TauCeti.hilbertSymbolOnSquareClasses_zero_right {K : Type u_1} [Field K] (x : SquareClassGroup K) : hilbertSymbolOnSquareClasses x 0 = 1

The square-class Hilbert symbol is trivial on a zero second argument.

theorem TauCeti.hilbertSymbol_eq_one_iff_nonempty_algEquiv_matrix {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : hilbertSymbol a b = 1 ↔ Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K)

The positive sign is equivalent to splitting the associated quaternion algebra.

theorem TauCeti.hilbertSymbol_eq_one_iff_not_anisotropic_weightedSumSquares {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : hilbertSymbol a b = 1 ↔ ¬(QuadraticMap.weightedSumSquares K ![1, -↑a, -↑b]).Anisotropic

The positive sign is equivalent to isotropy of the ternary form ⟨1,-a,-b⟩.

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

Isomorphic quaternion algebras have the same norm-equation sign.

theorem TauCeti.hilbertSymbol_comm {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : hilbertSymbol a b = hilbertSymbol b a

Symmetry of the norm-equation Hilbert symbol.

theorem TauCeti.hilbertSymbolOnSquareClasses_comm {K : Type u_1} [Field K] [Invertible 2] (x y : SquareClassGroup K) : hilbertSymbolOnSquareClasses x y = hilbertSymbolOnSquareClasses y x

The square-class Hilbert symbol is symmetric.

@[simp]

theorem TauCeti.hilbertSymbolOnSquareClasses_zero_left {K : Type u_1} [Field K] [Invertible 2] (y : SquareClassGroup K) : hilbertSymbolOnSquareClasses 0 y = 1

The square-class Hilbert symbol is trivial on a zero first argument.

theorem TauCeti.hilbertSymbol_eq_one_of_isSquare_left {K : Type u_1} [Field K] [Invertible 2] {a : Kˣ} (ha : IsSquare a) (b : Kˣ) : hilbertSymbol a b = 1

A square first parameter has positive symbol.

@[simp]

theorem TauCeti.hilbertSymbol_one_left {K : Type u_1} [Field K] [Invertible 2] (b : Kˣ) : hilbertSymbol 1 b = 1

The first parameter 1 has positive symbol.