The 2-adic Hilbert symbol: units #
Serre's explicit formula for the Hilbert symbol at p = 2 writes a = 2 ^ α u,
b = 2 ^ β v with u, v ∈ ℤ_[2]ˣ and reads
(a,b)_2 = (-1)^{ε(u) ε(v) + α ω(v) + β ω(u)},
where ε(u) = 0 iff u ≡ 1 (mod 4) and ω(u) = 0 iff u ≡ ±1 (mod 8).
This file proves the unit case α = β = 0, in the intrinsic form
(u,v)_2 = 1 if u ≡ 1 (mod 4) or v ≡ 1 (mod 4), and (u,v)_2 = -1 otherwise.
The proof does not need any norm-group theory. It uses the square-class structure of
ℤ_[2]ˣ: every unit is a square times one of 1, 5, -1, -5, and on those four
representatives the symbol is decided either by an explicit rational point
(the 1 entries) or by reducing a putative solution modulo 4 (the -1 entries).
Note that the "two units have symbol 1" statement that holds for odd p is false
at p = 2: (3,3)_2 = -1.
Finite residue facts #
Square units #
Reducing rational solutions modulo 4 #
The homogeneity of z² - a x² - b y² lets us rescale any nontrivial rational solution by
the inverse of a coordinate of maximal norm, producing an integral solution with a unit
coordinate. This is the p = 2 specialization of the generic rescaling
exists_padicInt_solution_gen. Reducing that solution modulo 4 then contradicts
no_zmod4_sol whenever both coefficients are 3 mod 4.
Reducing a unit to its residue class modulo 8 #
Every unit u of ℤ_[2] is r · s² where r ∈ {1, 3, 5, 7} has the same residue as
u modulo 8 and s is another unit: indeed u * r is congruent to r² ≡ 1 modulo
8, hence a square. Because hilbertSym is unchanged when either argument is multiplied
by a nonzero square, this lets us compute the symbol on the four representatives.
The 4 × 4 table on the representatives #
The positive entries are witnessed by explicit points: (1,1,0), (1,0,1) and
(5,2,1) are rational, while (√17,1,2) and (√33,1,2) use that 17 ≡ 33 ≡ 1
modulo 8 are squares in ℤ_[2].
The unit classification #
The 2-adic unit decomposition #
The unit part of a nonzero 2-adic number: a = 2 ^ a.valuation * twoAdicUnit a ha.
Equations
Instances For
The symbol of 2 against a unit #
(2, v)_2 = 1 iff v ≡ ±1 (mod 8). The two -1 values are settled by reducing an
integral solution modulo 8 (there z² - 2x² - 3y² and z² - 2x² - 5y² have no zero with
a unit coordinate), and the two 1 values by explicit points: for v ≡ 1 the unit v is
a square, while for v ≡ 7 one has -v = s² and (s, s, 1) is a zero.
The ε and ω characters #
Serre's exponent ε(u)ε(v) + α ω(v) + β ω(u) uses ε(u) = 0 iff u ≡ 1 (mod 4) and
ω(u) = 0 iff u ≡ ±1 (mod 8). Both are read off the residues toZModPow 2 and
toZModPow 3 of the unit.
Serre's ε character: ε(u) = 0 iff u ≡ 1 (mod 4).
Equations
- HasseMinkowski.eps u = if (PadicInt.toZModPow 2) ↑u = 1 then 0 else 1
Instances For
Serre's ω character: ω(u) = 0 iff u ≡ ±1 (mod 8).
Equations
- HasseMinkowski.omg u = if (PadicInt.toZModPow 3) ↑u = 1 ∨ (PadicInt.toZModPow 3) ↑u = 7 then 0 else 1
Instances For
The mixed cases (2r, w) #
Serre's formula at p = 2 for a = 2r with r a unit and b = w a unit reads
(2r, w)_2 = (-1)^{ε(r) ε(w) + ω(w)}. Reducing r and w to the residues 1, 3, 5, 7
modulo 8 leaves a 4 × 4 table, whose 1 entries are witnessed by explicit rational
points and whose -1 entries are settled by reducing an integral solution modulo 8.
The r = 1 row is hilbertSym_two_unit_char.
The characters ε and ω only see the residue of the unit modulo 4 respectively
modulo 8; the next lemmas evaluate them on the four representatives.
Each row of the table is recorded against an arbitrary unit by reducing the second
argument. The row r = 1 is hilbertSym_two_unit_char, so only the rows 2r = 6, 10, 14
are new.
The identity (a,b) = (a,-ab) and the case α = β = 1 #
Completing the square turns a zero of z² - a x² - b y² into a zero of z² - a x² + a b y²
and conversely, so the two quadratic forms have nontrivial zeros simultaneously and the two
symbols agree. This reduces (2u, 2v) to (2u, -uv), which is the α = 1, β = 0 case
proved above.
The α = β = 1 exponent identity #
The characters ε and ω factor through the residue modulo 8, so the exponent identity
behind (2u, 2v) = (2u, -uv) is a finite computation on ZMod 8.
Assembling the closed formula #
Reducing the two valuations modulo 2 turns (a,b)_2 into one of the four base cases
already proved above. The only remaining bookkeeping is that the exponent in Serre's
formula uses the full valuations; since one summand valuation * ω(unit) is odd exactly
when both factors are odd, it differs from the reduced exponent by an even integer, and
parityPow (-1) only sees parity.
Multiplicativity in the first argument #
The closed formula of hilbertSym_padic_two_eq is a product of signs whose exponent is
built from the two valuations and the two unit characters ε, ω. Multiplicativity in
a therefore reduces to the two character identities ε(uv) ≡ ε(u) + ε(v) and
ω(uv) ≡ ω(u) + ω(v) modulo 2 (checked on the four units of ZMod 8), together with
valuation (a * a') = valuation a + valuation a' and multiplicativity of the unit part.