Quadratic reciprocity from Hilbert reciprocity

Hilbert's reciprocity law over ℚ says that for a, b ∈ ℚˣ the cohomological Hilbert invariants inv_v((a) ∪ (b)) ∈ ZMod 2 sum to zero over all places v of ℚ. This file evaluates that sum when a = p and b = q are distinct odd primes, and so identifies Hilbert reciprocity for p and q with the quadratic reciprocity law; and when a is -1 or 2 and b = p is an odd prime, identifying Hilbert reciprocity with the two supplementary laws.

Through TauCeti.finprod_hilbertSymbol_mul_prod_hilbertSymbol_eq_hilbertSign the sign of the sum is the product of the norm-equation Hilbert symbols (p, q)_v, and each factor is explicit:

• at the real place, (p, q)_∞ = 1, as p and q are positive;
• at a prime ℓ ∉ {2, p, q}, both p and q are ℓ-adic units and (p, q)_ℓ = 1;
• at p, (p, q)_p = (q / p), and at q, (p, q)_q = (p / q), the Legendre symbols;
• at 2, (p, q)_2 = (-1) ^ ((p - 1)/2 · (q - 1)/2), by Serre's dyadic formula.

The finite places of ℚ are read in ℚ_ℓ through TauCeti.hilbertSymbol_unitAtFinitePlace_rat. Hence the sum vanishes exactly when (p / q) (q / p) = (-1) ^ ((p - 1)/2 · (q - 1)/2). Read from left to right this derives quadratic reciprocity from Hilbert reciprocity; read from right to left with Mathlib's legendreSym.quadratic_reciprocity, it checks the normalization of the cohomological invariants at 2, p and q against the classical symbols.

The two supplementary laws come from the same sum for a = -1 and for a = 2, with b = p an odd prime. Only the places 2 and p contribute: (a, p)_p = (a / p), the real place contributes nothing as p is positive, and at 2 Serre's formula gives (-1, p)_2 = χ₄(p) and (2, p)_2 = χ₈(p). So Hilbert reciprocity for -1 and p is the first supplementary law (-1 / p) = χ₄(p) = (-1) ^ ((p - 1)/2), and for 2 and p it is the second supplementary law (2 / p) = χ₈(p) = (-1) ^ ((p² - 1)/8), in the forms of Mathlib's legendreSym.at_neg_one and legendreSym.at_two.

Main results

• coe_finprod_hilbertSymbol_unitAtFinitePlace_eq_legendreSym: the product of the Hilbert symbols (p, q)_v over the finite places.
• coe_hilbertSign_sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt: the sign of the sum of the cohomological Hilbert invariants of p and q.
• sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_eq_zero_iff: Hilbert reciprocity for p and q is equivalent to quadratic reciprocity for p and q.
• coe_finprod_hilbertSymbol_unitAtFinitePlace_eq_mul_legendreSym: the product of the Hilbert symbols (m, p)_v over the finite places, for an integer m divisible by no odd prime.
• coe_hilbertSign_sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_eq_mul: the sign (m, p)_2 · (m / p) of the sum of the cohomological Hilbert invariants of such m and p.
• sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_eq_zero_iff_neg_one and sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_eq_zero_iff_two: Hilbert reciprocity for -1 and p, respectively for 2 and p, is equivalent to the first, respectively the second, supplementary law for p.

All declarations are in the namespace TauCeti.ClassFieldTheory.

References

• J.-P. Serre, A Course in Arithmetic, Chapter III, §1.2, Theorem 1 (the local symbols) and §2.2, proof of Theorem 3 (their product for two odd primes, and for -1 or 2 and an odd prime).

theorem TauCeti.ClassFieldTheory.coe_finprod_hilbertSymbol_unitAtFinitePlace_eq_legendreSym {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] {a b : ℚˣ} (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) (ha : ↑a = ↑p) (hb : ↑b = ↑q) : ↑(∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)), hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b)) = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q * legendreSym q ↑p

The finite part of the Hilbert product formula for two odd primes. For distinct odd primes p and q, the product over the finite places v of ℚ of the Hilbert symbols (p, q)_v is (-1) ^ ((p - 1)/2 · (q - 1)/2) · (q / p) · (p / q): the place 2 contributes the sign, the places p and q the two Legendre symbols, and every other place 1.

theorem TauCeti.ClassFieldTheory.coe_hilbertSign_sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] {a b : ℚˣ} (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) (ha : ↑a = ↑p) (hb : ↑b = ↑q) : ↑(hilbertSign (∑ v ∈ finiteHilbertSupport ℚ a b, finiteHilbertInvariantAt ℚ v a b + ∑ w : NumberField.InfinitePlace ℚ, infiniteHilbertInvariantAt ℚ w a b)) = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q * legendreSym q ↑p

The Hilbert reciprocity sum of two odd primes. For distinct odd primes p and q, the sign of the sum over all places of ℚ of the cohomological Hilbert invariants of p and q is (-1) ^ ((p - 1)/2 · (q - 1)/2) · (q / p) · (p / q). The real place contributes nothing, as p and q are positive.

theorem TauCeti.ClassFieldTheory.sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_eq_zero_iff {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] {a b : ℚˣ} (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) (ha : ↑a = ↑p) (hb : ↑b = ↑q) : ∑ v ∈ finiteHilbertSupport ℚ a b, finiteHilbertInvariantAt ℚ v a b + ∑ w : NumberField.InfinitePlace ℚ, infiniteHilbertInvariantAt ℚ w a b = 0 ↔ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

Quadratic reciprocity is Hilbert reciprocity for two odd primes. For distinct odd primes p and q, the cohomological Hilbert invariants of p and q sum to zero over the places of ℚ exactly when (p / q) (q / p) = (-1) ^ ((p - 1)/2 · (q - 1)/2). So Hilbert's reciprocity law ∑_v inv_v((p) ∪ (q)) = 0 gives the quadratic reciprocity law, its dyadic factor being the sign.

The supplementary laws

theorem TauCeti.ClassFieldTheory.coe_finprod_hilbertSymbol_unitAtFinitePlace_eq_mul_legendreSym {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚˣ} (hp : p ≠ 2) {m : ℤ} (hm : ∀ (ℓ : ℕ), Nat.Prime ℓ → ℓ ≠ 2 → ¬↑ℓ ∣ m) (ha : ↑a = ↑m) (hb : ↑b = ↑p) : ↑(∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)), hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b)) = ↑(hilbertSymbol ((Units.map ↑(algebraMap ℚ ℚ_[2])) a) ((Units.map ↑(algebraMap ℚ ℚ_[2])) b)) * legendreSym p m

The finite part of the Hilbert product formula for an odd prime and a power of 2 up to sign. Let p be an odd prime and m an integer divisible by no odd prime. Then the product over the finite places v of ℚ of the Hilbert symbols (m, p)_v is (m, p)_2 · (m / p): the place p contributes the Legendre symbol, and every place other than 2 and p contributes 1.

theorem TauCeti.ClassFieldTheory.coe_hilbertSign_sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_eq_mul {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚˣ} (hp : p ≠ 2) {m : ℤ} (hm : ∀ (ℓ : ℕ), Nat.Prime ℓ → ℓ ≠ 2 → ¬↑ℓ ∣ m) (ha : ↑a = ↑m) (hb : ↑b = ↑p) : ↑(hilbertSign (∑ v ∈ finiteHilbertSupport ℚ a b, finiteHilbertInvariantAt ℚ v a b + ∑ w : NumberField.InfinitePlace ℚ, infiniteHilbertInvariantAt ℚ w a b)) = ↑(hilbertSymbol ((Units.map ↑(algebraMap ℚ ℚ_[2])) a) ((Units.map ↑(algebraMap ℚ ℚ_[2])) b)) * legendreSym p m

The Hilbert reciprocity sum of an odd prime and a power of 2 up to sign. Let p be an odd prime and m an integer divisible by no odd prime. Then the sign of the sum over all places of ℚ of the cohomological Hilbert invariants of m and p is (m, p)_2 · (m / p). The real place contributes nothing, as p is positive.

theorem TauCeti.ClassFieldTheory.coe_hilbertSign_sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_neg_one {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚˣ} (hp : p ≠ 2) (ha : ↑a = -1) (hb : ↑b = ↑p) : ↑(hilbertSign (∑ v ∈ finiteHilbertSupport ℚ a b, finiteHilbertInvariantAt ℚ v a b + ∑ w : NumberField.InfinitePlace ℚ, infiniteHilbertInvariantAt ℚ w a b)) = ZMod.χ₄ ↑p * legendreSym p (-1)

The Hilbert reciprocity sum of -1 and an odd prime. For an odd prime p, the sign of the sum over all places of ℚ of the cohomological Hilbert invariants of -1 and p is χ₄(p) · (-1 / p). The real place contributes nothing, as p is positive, and the place 2 contributes (-1, p)_2 = χ₄(p).

theorem TauCeti.ClassFieldTheory.sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_eq_zero_iff_neg_one {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚˣ} (hp : p ≠ 2) (ha : ↑a = -1) (hb : ↑b = ↑p) : ∑ v ∈ finiteHilbertSupport ℚ a b, finiteHilbertInvariantAt ℚ v a b + ∑ w : NumberField.InfinitePlace ℚ, infiniteHilbertInvariantAt ℚ w a b = 0 ↔ legendreSym p (-1) = ZMod.χ₄ ↑p

The first supplementary law is Hilbert reciprocity for -1 and an odd prime. For an odd prime p, the cohomological Hilbert invariants of -1 and p sum to zero over the places of ℚ exactly when (-1 / p) = χ₄(p), that is (-1 / p) = (-1) ^ ((p - 1)/2).

theorem TauCeti.ClassFieldTheory.coe_hilbertSign_sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_two {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚˣ} (hp : p ≠ 2) (ha : ↑a = 2) (hb : ↑b = ↑p) : ↑(hilbertSign (∑ v ∈ finiteHilbertSupport ℚ a b, finiteHilbertInvariantAt ℚ v a b + ∑ w : NumberField.InfinitePlace ℚ, infiniteHilbertInvariantAt ℚ w a b)) = ZMod.χ₈ ↑p * legendreSym p 2

The Hilbert reciprocity sum of 2 and an odd prime. For an odd prime p, the sign of the sum over all places of ℚ of the cohomological Hilbert invariants of 2 and p is χ₈(p) · (2 / p). The real place contributes nothing, as p is positive, and the place 2 contributes (2, p)_2 = χ₈(p).

theorem TauCeti.ClassFieldTheory.sum_finiteHilbertInvariantAt_add_sum_infiniteHilbertInvariantAt_eq_zero_iff_two {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚˣ} (hp : p ≠ 2) (ha : ↑a = 2) (hb : ↑b = ↑p) : ∑ v ∈ finiteHilbertSupport ℚ a b, finiteHilbertInvariantAt ℚ v a b + ∑ w : NumberField.InfinitePlace ℚ, infiniteHilbertInvariantAt ℚ w a b = 0 ↔ legendreSym p 2 = ZMod.χ₈ ↑p

The second supplementary law is Hilbert reciprocity for 2 and an odd prime. For an odd prime p, the cohomological Hilbert invariants of 2 and p sum to zero over the places of ℚ exactly when (2 / p) = χ₈(p), that is (2 / p) = (-1) ^ ((p² - 1)/8).