Global properties of the Hilbert symbol over ℚ

The Hilbert symbol (a,b)_v is defined at every place v of ℚ — the finite places v = p (a prime, giving ℚ_[p]) and the archimedean place v = ∞ (giving ℝ).

This file records the two global properties:

• almost_all_one — for fixed nonzero a b : ℚ, the symbol (a,b)_p is 1 for all but finitely many primes p. This is a genuinely local fact: for p not dividing the numerator or denominator of a or b, both arguments are p-adic units, and the case 00 of Serre's formula gives 1.

• Hilbert reciprocity ∏_v (a,b)_v = 1 (hilbertReciprocity). The hard input is quadratic reciprocity (legendreSym.quadratic_reciprocity); the proof reduces to the square-class generators -1 and the primes, using the case in which one argument is a square (prod_eq_one_of_isSquare, where every local symbol is 1) as a step.

instance HasseMinkowski.instFactPrimeCoeNat (p : Nat.Primes) : Fact (Nat.Prime ↑p)

A prime bundled as a natural number carries its own Fact instance.

Almost all local symbols are trivial

For a rational q, padicValRat p q = 0 precisely when p divides neither the numerator nor the denominator of q; such a q is a p-adic unit. There are only finitely many primes dividing a fixed nonzero rational, so for fixed a, b the symbol (a,b)_p is 1 for all but finitely many p.

theorem HasseMinkowski.almost_all_one {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, hilbertSym ↑a ↑b = 1

theorem HasseMinkowski.finite_nontrivial_hilbertSym {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : {p : Nat.Primes | hilbertSym ↑a ↑b ≠ 1}.Finite

Corollaries: squares give the trivial symbol

If a is a nonzero rational square, then (a,b)_v = 1 at every place v (both the finite places and the archimedean one), because the conic z² - a x² - b y² = 0 then has the obvious point (c, 1, 0) with a = c². Consequently the product over all places is 1; this is the special case of Hilbert reciprocity that needs no quadratic reciprocity.

theorem HasseMinkowski.hilbertSym_rat_eq_one_of_isSquare_left {a b : ℚ} (ha0 : a ≠ 0) (ha : IsSquare a) (hb : b ≠ 0) (p : Nat.Primes) : hilbertSym ↑a ↑b = 1

theorem HasseMinkowski.prod_eq_one_of_isSquare_left {a b : ℚ} (ha0 : a ≠ 0) (ha : IsSquare a) (hb : b ≠ 0) : (∏ᶠ (p : Nat.Primes), hilbertSym ↑a ↑b) * hilbertSym ↑a ↑b = 1

theorem HasseMinkowski.prod_eq_one_of_isSquare_right {a b : ℚ} (ha : a ≠ 0) (hb0 : b ≠ 0) (hb : IsSquare b) : (∏ᶠ (p : Nat.Primes), hilbertSym ↑a ↑b) * hilbertSym ↑a ↑b = 1

theorem HasseMinkowski.prod_eq_one_of_isSquare {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) (h : IsSquare a ∨ IsSquare b) : (∏ᶠ (p : Nat.Primes), hilbertSym ↑a ↑b) * hilbertSym ↑a ↑b = 1

The general statement (not proved here)

Hilbert reciprocity — the product of (a,b)_v over all places v of ℚ equals 1 — is the deep quadratic-reciprocity input. Its proof requires the full explicit formulas at every place (including p = 2, where only the unit case is available locally) and the quadratic reciprocity law assembled over all primes; that is beyond what this file formalises. We record the statement as a Prop for downstream reference.

def HasseMinkowski.HilbertReciprocity : Prop

Hilbert reciprocity for ℚ: for nonzero rationals a, b, the product of the local Hilbert symbols over all places (the finite places ℚ_[p] and the archimedean place ℝ) is 1. Stated for reference; not proved in this file.

Equations

• HasseMinkowski.HilbertReciprocity = ∀ (a b : ℚ), a ≠ 0 → b ≠ 0 → (∏ᶠ (p : Nat.Primes), HasseMinkowski.hilbertSym ↑a ↑b) * HasseMinkowski.hilbertSym ↑a ↑b = 1

Phase 1: reduction of Hilbert reciprocity to square classes

Write hilbertProd a b for the product of the local symbols of a, b over every place of ℚ. Every local symbol is bimultiplicative in each argument, so hilbertProd is too; and multiplying an argument by a nonzero square (or inverting it) leaves hilbertProd unchanged. Hence hilbertProd factors through the square-class group ℚ*/ℚ*², which is generated by -1 and the primes. So Hilbert reciprocity follows from its restriction to pairs of generators g ∈ {-1} ∪ {primes}: this is hilbertReciprocity_of_generators. The generator cases themselves (the content of quadratic reciprocity) are Phase 2.

noncomputable def HasseMinkowski.hilbertProd (a b : ℚ) : ℤ

The product of the local Hilbert symbols of a and b over all places of ℚ: the finite places ℚ_[p] together with the archimedean place ℝ.

Equations

• HasseMinkowski.hilbertProd a b = (∏ᶠ (p : Nat.Primes), HasseMinkowski.hilbertSym ↑a ↑b) * HasseMinkowski.hilbertSym ↑a ↑b

def HasseMinkowski.IsGen (g : ℚ) : Prop

A generator of the square-class group ℚ*/ℚ*²: -1 or a prime.

Equations

• HasseMinkowski.IsGen g = (g = -1 ∨ ∃ (p : Nat.Primes), g = ↑↑p)

theorem HasseMinkowski.hilbertProd_mul_left (a a' b : ℚ) (ha : a ≠ 0) (ha' : a' ≠ 0) (hb : b ≠ 0) : hilbertProd (a * a') b = hilbertProd a b * hilbertProd a' b

theorem HasseMinkowski.hilbertProd_mul_right (a b b' : ℚ) (ha : a ≠ 0) (hb : b ≠ 0) (hb' : b' ≠ 0) : hilbertProd a (b * b') = hilbertProd a b * hilbertProd a b'

theorem HasseMinkowski.hilbertProd_comm (a b : ℚ) : hilbertProd a b = hilbertProd b a

theorem HasseMinkowski.hilbertProd_one_right (a : ℚ) (ha : a ≠ 0) : hilbertProd a 1 = 1

theorem HasseMinkowski.hilbertProd_one_left (b : ℚ) (hb : b ≠ 0) : hilbertProd 1 b = 1

theorem HasseMinkowski.hilbertProd_mul_square_right (a b c : ℚ) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) : hilbertProd a (b * c ^ 2) = hilbertProd a b

theorem HasseMinkowski.hilbertProd_mul_square_left (a c b : ℚ) (ha : a ≠ 0) (hc : c ≠ 0) (hb : b ≠ 0) : hilbertProd (a * c ^ 2) b = hilbertProd a b

theorem HasseMinkowski.hilbertProd_inv_left (a b : ℚ) (ha : a ≠ 0) (hb : b ≠ 0) : hilbertProd a⁻¹ b = hilbertProd a b

theorem HasseMinkowski.hilbertProd_inv_right (a b : ℚ) (ha : a ≠ 0) (hb : b ≠ 0) : hilbertProd a b⁻¹ = hilbertProd a b

theorem HasseMinkowski.hilbertProd_finset_prod_left {ι : Type u_1} (S : Finset ι) (f : ι → ℚ) (b : ℚ) (hf : ∀ i ∈ S, f i ≠ 0) (hb : b ≠ 0) : hilbertProd (∏ i ∈ S, f i) b = ∏ i ∈ S, hilbertProd (f i) b

theorem HasseMinkowski.hilbertProd_finset_prod_right {ι : Type u_1} (S : Finset ι) (f : ι → ℚ) (a : ℚ) (hf : ∀ i ∈ S, f i ≠ 0) (ha : a ≠ 0) : hilbertProd a (∏ i ∈ S, f i) = ∏ i ∈ S, hilbertProd a (f i)

The square-class decomposition

Every nonzero rational is a generator product times a nonzero square. Write q = ±u/v with u = |q.num|, v = q.den; apply Nat.sq_mul_squarefree_of_pos to u * v, so that u * v = b² · a with a squarefree. Then u/v = a · (b/v)², and the squarefree a is the product of its (prime) factors.

theorem HasseMinkowski.IsGen.ne_zero {g : ℚ} (hg : IsGen g) : g ≠ 0

theorem HasseMinkowski.exists_gen_prod_mul_sq (q : ℚ) (hq : q ≠ 0) : ∃ (S : Finset ℚ) (s : ℚ), (∀ g ∈ S, IsGen g) ∧ s ≠ 0 ∧ q = S.prod id * s ^ 2

Phase 1: reduction to the generator cases

theorem HasseMinkowski.hilbertProd_gen_left (hgen : ∀ (g h : ℚ), IsGen g → IsGen h → hilbertProd g h = 1) (g : ℚ) (hg : IsGen g) (b : ℚ) (hb : b ≠ 0) : hilbertProd g b = 1

theorem HasseMinkowski.hilbertProd_eq_one (hgen : ∀ (g h : ℚ), IsGen g → IsGen h → hilbertProd g h = 1) {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : hilbertProd a b = 1

theorem HasseMinkowski.hilbertReciprocity_of_generators (hgen : ∀ (g h : ℚ), IsGen g → IsGen h → hilbertProd g h = 1) : HilbertReciprocity

Phase 2: the generator cases

hilbertReciprocity_of_generators reduces HilbertReciprocity to the values on pairs of generators g, h ∈ {-1} ∪ {primes}. Those are exactly the quadratic-reciprocity computations:

• hilbertProd (-1) (-1) = 1: the archimedean and 2-adic symbols are both -1, and the finite product over the remaining places is -1, so the two cancel;
• hilbertProd (-1) p = 1: the two non-trivial places 2 and p both contribute (-1)^{(p-1)/2};
• hilbertProd p p = 1: the supplementary laws at 2 and at p;
• hilbertProd p q = 1 for distinct primes, the quadratic reciprocity law (p/q)(q/p) = (-1)^{(p-1)/2 · (q-1)/2} (Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity).

Each case is a finite finprod with support among {2, p, q}; applying hilbertReciprocity_of_generators to them yields HilbertReciprocity itself (hilbertReciprocity, at the end of the file).

Phase 2, infrastructure

finprod_hilbertSym_eq_finset_prod reduces the infinite product over all primes to a finite product over an explicit small set. hilbertSym_padic_odd_units handles every odd place that divides neither argument, and quadraticChar_padicUnit_nat identifies the quadratic character of the unit part of a rational prime with Mathlib's legendreSym.

Phase 2, the 2-adic supplementary laws

The 2-adic unit formulas of Two.lean are stated for units of ℤ_[2]; we package an odd natural n as the unit unitTwo n. The three evaluations needed below are (-1,-1)_2 = -1, (-1,n)_2 = χ₄ n and (n,n)_2 = χ₄ n, the last two being the supplementary laws at 2 rewritten as values of the Dirichlet character χ₄.

Phase 2, the odd-prime evaluations

Phase 2, the generator cases

theorem HasseMinkowski.hilbertProd_neg_one_neg_one : hilbertProd (-1) (-1) = 1

theorem HasseMinkowski.hilbertProd_neg_one_prime (p : Nat.Primes) : hilbertProd (-1) ↑↑p = 1

theorem HasseMinkowski.hilbertProd_prime_self (p : Nat.Primes) : hilbertProd ↑↑p ↑↑p = 1

Phase 2, the case (p,q) of distinct primes

The final generator case is genuinely quadratic reciprocity. At the two odd places p and q the local symbols are (q/p) and (p/q); at 2 the symbol is the quadratic-reciprocity sign (-1)^{(p-1)/2 · (q-1)/2}; and the archimedean symbol is 1 because both primes are positive. The product is 1 by legendreSym.quadratic_reciprocity.

theorem HasseMinkowski.hilbertProd_two_prime (q : Nat.Primes) (hq2 : ↑q ≠ 2) : hilbertProd 2 ↑↑q = 1

theorem HasseMinkowski.hilbertProd_prime_prime (p q : Nat.Primes) (hpq : p ≠ q) : hilbertProd ↑↑p ↑↑q = 1

Hilbert reciprocity

theorem HasseMinkowski.hilbertReciprocity : HilbertReciprocity