The Hilbert symbol over ℚ_2

Write a, b ∈ ℚ_2ˣ as a = 2 ^ α u and b = 2 ^ β v with u, v units of ℤ_2. Serre's closed formula for the Hilbert symbol over ℚ_2 is

(a, b) = (-1) ^ (ε(u) ε(v) + α ω(v) + β ω(u)),

where ε(u) = (u − 1)/2 and ω(u) = (u² − 1)/8 modulo 2 are the sign functions TauCeti.serreEps and TauCeti.serreOmega. The exponent lives in ZMod 2, and the sign is (-1 : ℤˣ) ^ x for x : ZMod 2. This explicit formula over ℚ_2 pins down the sign convention of the local Hilbert symbol in residue characteristic 2.

The classes of -1, 2 and 5 form a ZMod 2-basis of ℚ_2ˣ/(ℚ_2ˣ)²: they generate it, since every unit of ℤ_2 is (-1) ^ ε(u) 5 ^ ω(u) times a square (TauCeti.exists_eq_neg_one_pow_mul_five_pow_mul_sq), and they are independent because the symbol is nondegenerate on them. On these generators the symbol takes the values

• (-1, 2) = (-1, 5) = (2, 2) = (5, 5) = +1, and
• (-1, -1) = (2, 5) = −1,

so in coordinates x₀, x₁, x₂ along -1, 2, 5 it is (-1) ^ (x₀ y₀ + x₁ y₂ + x₂ y₁). Read on the eight representatives 1, -1, 5, -5, 2, -2, 10, -10 of the square classes this gives the full 8 × 8 table of the symbol over ℚ_2, the check that pins the dyadic sign convention.

Main results

• TauCeti.hilbertSymbol_padicTwo: Serre's formula for the Hilbert symbol over ℚ_2.
• TauCeti.hilbertSymbol_natCast_natCast_padicTwo: for odd natural numbers m and n, (m, n) = (-1) ^ ((m - 1)/2 · (n - 1)/2) over ℚ_2.
• TauCeti.coe_hilbertSymbol_neg_one_natCast_padicTwo, TauCeti.coe_hilbertSymbol_two_natCast_padicTwo: for an odd natural number n, (-1, n) = χ₄(n) and (2, n) = χ₈(n) over ℚ_2.
• TauCeti.hilbertSymbol_neg_one_neg_one_padicTwo: (-1, -1) = −1 over ℚ_2, that is -1 is not of the form x² + y² in ℚ_2.
• TauCeti.hilbertSymbol_two_five_padicTwo: (2, 5) = −1 over ℚ_2.
• TauCeti.padicTwoSquareClassBasis: the classes of -1, 2, 5 as a ZMod 2-basis of the square-class group of ℚ_2.
• TauCeti.hilbertSymbolOnSquareClasses_padicTwo: the symbol on square classes in the coordinates of that basis.
• TauCeti.toMatrix_hilbertSymbolForm_padicTwo: the Gram matrix of the ZMod 2-bilinear Hilbert symbol form TauCeti.hilbertSymbolForm in that basis.
• TauCeti.squareClass_padicTwoSquareClassRep_bijective: 1, -1, 5, -5, 2, -2, 10, -10 represent each square class of ℚ_2 exactly once.
• TauCeti.hilbertSymbol_padicTwoSquareClassRep: the 8 × 8 table of the symbol on these representatives.

References

• J.-P. Serre, A Course in Arithmetic, Chapter III, §1.2, Theorem 1.

theorem TauCeti.hilbertSymbol_neg_one_neg_one_padicTwo : hilbertSymbol (-1) (-1) = -1

(-1, -1) = −1 over ℚ_2: -1 is not of the form x² + y² with x, y ∈ ℚ_2.

instance TauCeti.instFactNotIsSquarePadicOfNatNatNeg_tauCeti : Fact ¬IsSquare (-1)

-1 is not a square in ℚ_2, so the quadratic algebra ℚ_2(i) is a field.

theorem TauCeti.hilbertSymbol_two_five_padicTwo : hilbertSymbol (Units.mk0 2 ⋯) (Units.mk0 5 hilbertSymbol_two_five_padicTwo._proof_1) = -1

(2, 5) = −1 over ℚ_2: 5 is not of the form x² − 2 y² with x, y ∈ ℚ_2.

theorem TauCeti.hilbertSymbol_padicTwo {a b : ℚ_[2]ˣ} {α β : ℤ} {u v : ℤ_[2]ˣ} (ha : ↑a = 2 ^ α * ↑↑u) (hb : ↑b = 2 ^ β * ↑↑v) : hilbertSymbol a b = (-1) ^ (serreEps u * serreEps v + ↑α * serreOmega v + ↑β * serreOmega u)

Serre's formula for the Hilbert symbol over ℚ_2. For a = 2 ^ α u and b = 2 ^ β v with u, v units of ℤ_2,

(a, b) = (-1) ^ (ε(u) ε(v) + α ω(v) + β ω(u)),

with the exponent computed in ZMod 2.

theorem TauCeti.hilbertSymbol_natCast_natCast_padicTwo {m n : ℕ} (hm : Odd m) (hn : Odd n) : hilbertSymbol (Units.mk0 ↑m ⋯) (Units.mk0 ↑n ⋯) = (-1) ^ (m / 2 * (n / 2))

The Hilbert symbol of two odd natural numbers over ℚ_2: (m, n) = (-1) ^ ((m - 1)/2 · (n - 1)/2), which is -1 exactly when m ≡ n ≡ 3 (mod 4). This is the dyadic factor of the product formula behind quadratic reciprocity.

theorem TauCeti.coe_hilbertSymbol_neg_one_natCast_padicTwo {n : ℕ} (hn : Odd n) : ↑(hilbertSymbol (-1) (Units.mk0 ↑n ⋯)) = ZMod.χ₄ ↑n

The Hilbert symbol of -1 and an odd natural number over ℚ_2: (-1, n) = χ₄(n), which is -1 exactly when n ≡ 3 (mod 4). This is the dyadic factor of the product formula behind the first supplementary law of quadratic reciprocity.

theorem TauCeti.coe_hilbertSymbol_two_natCast_padicTwo {n : ℕ} (hn : Odd n) : ↑(hilbertSymbol (Units.mk0 2 ⋯) (Units.mk0 ↑n ⋯)) = ZMod.χ₈ ↑n

The Hilbert symbol of 2 and an odd natural number over ℚ_2: (2, n) = χ₈(n), which is -1 exactly when n ≡ ±3 (mod 8). This is the dyadic factor of the product formula behind the second supplementary law of quadratic reciprocity.

The symbol on a basis of the square classes, and the 8 × 8 table

noncomputable def TauCeti.padicTwoSquareClassBasis : Module.Basis (Fin 3) (ZMod 2) (SquareClassGroup ℚ_[2])

The basis -1, 2, 5 of the square classes of ℚ_2. The classes of -1, 2 and 5 form a ZMod 2-basis of ℚ_2ˣ/(ℚ_2ˣ)², which therefore has eight elements.

@[simp]

theorem TauCeti.coe_padicTwoSquareClassBasis : ⇑padicTwoSquareClassBasis = ![squareClass (-1), squareClass (Units.mk0 2 ⋯), squareClass (Units.mk0 5 hilbertSymbol_two_five_padicTwo._proof_1)]

The basis vectors of TauCeti.padicTwoSquareClassBasis are the classes of -1, 2, 5.

theorem TauCeti.hilbertSymbolOnSquareClasses_padicTwo (x y : SquareClassGroup ℚ_[2]) : hilbertSymbolOnSquareClasses x y = (-1) ^ ((padicTwoSquareClassBasis.repr x) 0 * (padicTwoSquareClassBasis.repr y) 0 + (padicTwoSquareClassBasis.repr x) 1 * (padicTwoSquareClassBasis.repr y) 2 + (padicTwoSquareClassBasis.repr x) 2 * (padicTwoSquareClassBasis.repr y) 1)

The Gram matrix of the Hilbert symbol over ℚ_2. In the coordinates x₀, x₁, x₂ of a square class with respect to the basis -1, 2, 5 (TauCeti.padicTwoSquareClassBasis), the Hilbert symbol is (x, y) = (-1) ^ (x₀ y₀ + x₁ y₂ + x₂ y₁). Its Gram matrix

        −1   2   5
  −1     1   0   0
   2     0   0   1
   5     0   1   0

is invertible over ZMod 2, which is the nondegeneracy of the symbol read on this basis.

theorem TauCeti.toMatrix_hilbertSymbolForm_padicTwo : (LinearMap.BilinForm.toMatrix padicTwoSquareClassBasis) (hilbertSymbolForm ℚ_[2]) = !![1, 0, 0; 0, 0, 1; 0, 1, 0]

The Gram matrix of the Hilbert symbol form over ℚ_2. In the basis -1, 2, 5 of the square classes (TauCeti.padicTwoSquareClassBasis), the ZMod 2-bilinear Hilbert symbol form TauCeti.hilbertSymbolForm has the invertible Gram matrix

        −1   2   5
  −1     1   0   0
   2     0   0   1
   5     0   1   0

that is (-1, -1) = (2, 5) = (5, 2) = −1, and every other pairing of basis vectors is +1.

noncomputable def TauCeti.padicTwoSquareClassRep (i : Fin 8) : ℚ_[2]ˣ

The eight representatives 1, -1, 5, -5, 2, -2, 10, -10 of the square classes of ℚ_2, in this order.

@[simp]

theorem TauCeti.coe_padicTwoSquareClassRep (i : Fin 8) : ↑(padicTwoSquareClassRep i) = ![1, -1, 5, -5, 2, -2, 10, -10] i

The values of TauCeti.padicTwoSquareClassRep in ℚ_2.

theorem TauCeti.squareClass_padicTwoSquareClassRep_bijective : Function.Bijective fun (i : Fin 8) => squareClass (padicTwoSquareClassRep i)

1, -1, 5, -5, 2, -2, 10, -10 represent each square class of ℚ_2 exactly once.

theorem TauCeti.hilbertSymbol_padicTwoSquareClassRep (i j : Fin 8) : hilbertSymbol (padicTwoSquareClassRep i) (padicTwoSquareClassRep j) = !![1, 1, 1, 1, 1, 1, 1, 1; 1, -1, 1, -1, 1, -1, 1, -1; 1, 1, 1, 1, -1, -1, -1, -1; 1, -1, 1, -1, -1, 1, -1, 1; 1, 1, -1, -1, 1, 1, -1, -1; 1, -1, -1, 1, 1, -1, -1, 1; 1, 1, -1, -1, -1, -1, 1, 1; 1, -1, -1, 1, -1, 1, 1, -1] i j

The 8 × 8 table of the Hilbert symbol over ℚ_2 on the representatives 1, -1, 5, -5, 2, -2, 10, -10 of the square classes (Serre, A Course in Arithmetic, III §1.2). Rows and columns are listed in this order.