The p-adic Hilbert symbol at an odd prime #
This file begins the computation of the Hilbert symbol (a,b)_p on ℚ_[p] for odd p,
following Serre's explicit formula
(a,b)_p = (-1)^{αβ(p-1)/2} · (u/p)^β · (v/p)^α, where a = p^α u, b = p^β v,
u,v ∈ ℤ_[p]ˣ, and (·/p) is the quadratic character modulo p.
The first ingredient is the "case 00" of the formula: two p-adic units have
Hilbert symbol 1. Although upstream states this through the Legendre symbol (with both
valuations zero the formula collapses), the underlying geometric content is just that the
ternary form z² - u x² - v y² has a nontrivial zero: modulo p this form is isotropic
(sum of two squares cover a finite field), and a nonsingular mod-p point Hensel-lifts.
We prove this here as hilbertSym_padicInt_units. The remaining cases 10 / 11
(one resp. two factors divisible by p) and the general multiplicativity mul_left_eq
are recorded in HANDOFF-hilbertpadic.md as the outstanding work; only p = 2 is out of
scope entirely.
General consequences of a nontrivial zero #
A quadratic form z² - a x² - b y² with a nontrivial zero has Hilbert symbol 1
(provided a and b are nonzero).
Isotropy of u x² + v y² = 1 over 𝔽_p #
The case of two units #
Case 10: a unit against an element of valuation 1 #
Serre's formula for (a,b)_p with a a unit and b of valuation 1 collapses to the
Legendre symbol (a/p) of the unit a. Geometrically the form z² - a x² - b y² has
its b-term divisible by p, so after rescaling to an integral solution with a unit
coordinate a mod-p argument identifies a with a square exactly when a solution exists.
The scaling lemma below is the same normalization as Padic.exists_padicInt_solution
(Padics/CommonRoot.lean), but with both coefficients arbitrary — the coefficients never
enter the rescaling.
Case 11: two elements of valuation 1 #
With both arguments of valuation 1 the form z² - p x² - p y² has a nontrivial zero
exactly when -1 is a square modulo p, i.e. (p,p)_p = (-1)^{(p-1)/2}. The square
direction is the explicit solution (0, s, 1) with s² = -1; the non-square direction
reduces an integral solution mod p twice, forcing X² + Y² ≡ 0.
The general formula for odd p #
Assembling the four square-class cases gives Serre's formula. For nonzero a, b : ℚ_[p] write
a = p ^ α · u, b = p ^ β · v with α = a.valuation, β = b.valuation and units
u = padicUnit a ha, v = padicUnit b hb (the "unit part" a · p ^ (-α)). Then
(a,b)_p = (-1)^{αβ(p-1)/2} · χ(u)^β · χ(v)^α, χ = quadraticChar (ZMod p).
Since χ(-1) = (-1)^{(p-1)/2} the sign is χ(-1)^{αβ}. Negative exponents are handled by
parityPow, which is b ^ n when b = ±1 and depends only on the parity of n.
The proof reduces α, β modulo 2 by absorbing (p^{α/2})² into the arguments through
hilbertSym_mul_square_eq, then checks the four parities against the case lemmas 00, 10
and 11. Bilinearity in the first argument follows formally.