Hilbert symbols over ℚ_p for odd p

Let p be an odd prime. The prime p is a uniformizer of ℚ_p and the residue field of ℚ_p is 𝔽_p, so the odd-residue formulas for the Hilbert symbol become formulas in terms of residues modulo p.

• The residue sign of a unit u of ℤ_p is the quadratic character (u / p) of its reduction modulo p. Hence the odd-residue formula TauCeti.hilbertSymbol_oddResidue_formula, read at the uniformizer p, is Serre's closed formula: for a = p ^ α u and b = p ^ β v with u, v units of ℤ_p, (a, b)_p = (-1) ^ (α β (p - 1)/2) · (u / p) ^ β · (v / p) ^ α. Every element of ℚ_pˣ has this form, so the formula computes the symbol on all of ℚ_pˣ; for integers it reads in Legendre symbols.
• Two integers prime to p are units of ℤ_p, and their symbol is 1.
• For an integer n prime to p, the symbol (n, p)_p is the Legendre symbol (n / p): it is 1 exactly when n is a square modulo p. Together with the dyadic value TauCeti.hilbertSymbol_natCast_natCast_padicTwo, these are the local factors of the product formula behind quadratic reciprocity. As the symbol of a unit with the uniformizer detects squares, such an n is a square in ℚ_p exactly when it is a square modulo p.
• For p ≡ 3 (mod 4) the unit -1 has nonsquare residue in 𝔽_p, so (-1, p)_p = -1: the prime p is not of the form x² + y² in ℚ_p. Equivalently, by TauCeti.hilbertSymbol_eq_one_iff_not_anisotropic_weightedSumSquares, the ternary form ⟨1, 1, -p⟩ is anisotropic over ℚ_p. For p = 3 this is the local obstruction carried by the form ⟨1, 1, -3⟩ over ℚ, which is isotropic over ℝ but anisotropic over ℚ_3.

Main results

• Units.oddResidueSign_map_integerRingEquiv_symm_eq_quadraticChar: the residue sign of a unit of ℤ_p is the quadratic character of its reduction modulo p.
• TauCeti.Padic.hilbertSymbol_formula_of_ne_two: Serre's formula for the Hilbert symbol over ℚ_p.
• TauCeti.Padic.coe_hilbertSymbol_pow_mul_intCast_pow_mul_intCast: the same formula for p ^ α m and p ^ β n with integers m, n prime to p, in Legendre symbols.
• TauCeti.Padic.hilbertSymbol_intCast_intCast_eq_one: (m, n)_p = 1 for integers m, n prime to p.
• TauCeti.Padic.hilbertSymbol_intCast_self_eq_legendreSym: (n, p)_p = (n / p) for an integer n prime to p.
• TauCeti.Padic.isSquare_intCast_iff_legendreSym_eq_one: an integer prime to p is a square in ℚ_p exactly when it is a square modulo p.
• Padic.hilbertSymbol_neg_one_eq_neg_one_of_mod_four_eq_three: (-1, p)_p = -1 when p ≡ 3 (mod 4).

References

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

theorem Units.oddResidueSign_map_integerRingEquiv_symm_eq_quadraticChar {p : ℕ} [Fact (Nat.Prime p)] (u : ℤ_[p]ˣ) : TauCeti.Units.oddResidueSign ((map ↑(Padic.integerRingEquiv p).symm) u) = (quadraticChar (ZMod p)).toUnitHom ((map ↑PadicInt.toZMod) u)

The residue sign over ℚ_p is the Legendre character. For a unit u of ℤ_p, the residue sign of u, read in the integer ring of ℚ_p, is the quadratic character of the reduction of u modulo p; for u the image of an integer n, this is legendreSym p n.

theorem TauCeti.Padic.hilbertSymbol_formula_of_ne_two {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) {a b : ℚ_[p]ˣ} {α β : ℤ} {u v : ℤ_[p]ˣ} (ha : ↑a = ↑p ^ α * ↑↑u) (hb : ↑b = ↑p ^ β * ↑↑v) : hilbertSymbol a b = ((-1) ^ ((p - 1) / 2)) ^ (α * β) * (quadraticChar (ZMod p)).toUnitHom ((Units.map ↑PadicInt.toZMod) u) ^ β * (quadraticChar (ZMod p)).toUnitHom ((Units.map ↑PadicInt.toZMod) v) ^ α

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

(a, b) = ((-1) ^ ((p - 1)/2)) ^ (α β) · (u / p) ^ β · (v / p) ^ α,

where (u / p) is the quadratic character of the reduction of u modulo p, as a sign.

theorem TauCeti.Padic.coe_hilbertSymbol_pow_mul_intCast_pow_mul_intCast {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) (α β : ℕ) {m n : ℤ} (hm : ¬↑p ∣ m) (hn : ¬↑p ∣ n) : ↑(hilbertSymbol (Units.mk0 (↑p ^ α * ↑m) ⋯) (Units.mk0 (↑p ^ β * ↑n) ⋯)) = (-1) ^ (α * β * ((p - 1) / 2)) * legendreSym p m ^ β * legendreSym p n ^ α

Serre's formula over ℚ_p for integers, with Legendre symbols. For an odd prime p, integers m, n prime to p and natural numbers α, β,

(p ^ α m, p ^ β n) = (-1) ^ (α β (p - 1)/2) · (m / p) ^ β · (n / p) ^ α.

theorem TauCeti.Padic.hilbertSymbol_intCast_intCast_eq_one {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) {m n : ℤ} (hm : ¬↑p ∣ m) (hn : ¬↑p ∣ n) : hilbertSymbol (Units.mk0 ↑m ⋯) (Units.mk0 ↑n ⋯) = 1

The Hilbert symbol of two p-adic units. For an odd prime p and integers m and n prime to p, the Hilbert symbol (m, n) over ℚ_p is 1.

theorem TauCeti.Padic.hilbertSymbol_intCast_self_eq_legendreSym {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) {n : ℤ} (hn : ¬↑p ∣ n) : ↑(hilbertSymbol (Units.mk0 ↑n ⋯) (Units.mk0 ↑p ⋯)) = legendreSym p n

The Hilbert symbol (n, p) over ℚ_p is the Legendre symbol (n / p), for an odd prime p and an integer n prime to p: the integral unit n pairs with the uniformizer p to 1 exactly when its residue is a square in 𝔽_p.

theorem TauCeti.Padic.isSquare_intCast_iff_legendreSym_eq_one {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) {n : ℤ} (hn : ¬↑p ∣ n) : IsSquare ↑n ↔ legendreSym p n = 1

Squares in ℚ_p of integers prime to p. For an odd prime p and an integer n prime to p, the image of n in ℚ_p is a square exactly when n is a square modulo p, that is (n / p) = 1.

theorem Padic.hilbertSymbol_neg_one_eq_neg_one_of_mod_four_eq_three (p : ℕ) [Fact (Nat.Prime p)] (hp : p % 4 = 3) : TauCeti.hilbertSymbol (-1) (Units.mk0 ↑p ⋯) = -1

If p ≡ 3 (mod 4), then the Hilbert symbol (-1, p) over ℚ_p is -1: the prime p is not a sum of two squares in ℚ_p.