B7′: the dyadic Hilbert symbol #

The paper's Lemma 3.5 evaluates the cup product H¹(ℚ₂, μ₂) × H¹(ℚ₂, μ₂) → H²(ℚ₂, μ₂) ≅ 𝔽₂ on the square-class basis via the Hilbert symbol (·,·)₂. This file provides that symbol elementarily and records the explicit dyadic formula as the axiom B7′.

GQ2.HilbertSymbol.IsHilbertSolvable a b — the ternary form a X² + b Y² - Z² has a nontrivial ℚ₂-zero. hilbertSymbol a b : ℤˣ (= {±1}) is 1 on this locus, -1 off it. Defined with no cohomology, so the elementary identities below are theorems.
GQ2.HilbertSymbol.ε, GQ2.HilbertSymbol.ω : ℤ₂ˣ → 𝔽₂ — Serre's residue characters ε(u) ≡ (u-1)/2, ω(u) ≡ (u²-1)/8 (mod 2) (A Course in Arithmetic, Ch. II §3.3), computed through the reduction ℤ₂ → ℤ/8. Both are homomorphisms on units (ε_mul, ω_mul).
Axiom hilbertSymbol_dyadic = Serre CiA III §1.2 Theorem 1, p = 2 case: (2^α u, 2^β v)₂ = (-1)^{ε(u)ε(v) + α ω(v) + β ω(u)}.

Stress tests (theorems): symmetry (a,b)=(b,a); (a,-a)=1; square-class invariance in one slot; the ε/ω residue tables and their values on the unit -1; and (as a consequence of the axiom) the square-class-basis value (-1,-1)₂ = -1, the nontrivial diagonal entry of the paper's initial cup form α² + βγ + γβ.

Conventions: ℚ_[2] = Padic 2, ℤ_[2] = PadicInt 2, 𝔽₂ = ZMod 2; the symbol is ℤˣ = {±1}-valued via signOf : 𝔽₂ → ℤˣ, 0 ↦ 1, 1 ↦ -1.

The dyadic formula is proved in GQ2/HilbertSymbolDyadicClose.lean; its public theorem is exposed from GQ2/Foundations/Axioms.lean alongside the remaining literature interfaces.

The Hilbert symbol via solvability of `z² = a x² + b y²` #

source

def GQ2.HilbertSymbol.IsHilbertSolvable (a b : ℚ_[2]) :

Prop

IsHilbertSolvable a b: the ternary quadratic form a X² + b Y² - Z² has a nontrivial zero over ℚ₂, i.e. the Hilbert symbol (a, b)₂ is +1. (Serre, A Course in Arithmetic, III §1.1.)

Equations

GQ2.HilbertSymbol.IsHilbertSolvable a b = ∃ (x : ℚ_[2]) (y : ℚ_[2]) (z : ℚ_[2]), (x ≠ 0 ∨ y ≠ 0 ∨ z ≠ 0) ∧ a * x ^ 2 + b * y ^ 2 = z ^ 2

Instances For

source

def GQ2.HilbertSymbol.signOf (x : ZMod 2) :

ℤˣ

signOf x = (-1)^x ∈ ℤˣ = {±1}.

Equations

GQ2.HilbertSymbol.signOf x = if x = 0 then 1 else -1

Instances For

source

noncomputable def GQ2.HilbertSymbol.hilbertSymbol (a b : ℚ_[2]ˣ) :

ℤˣ

The (quadratic) Hilbert symbol (a, b)₂ ∈ ℤˣ = {±1} for a, b ∈ ℚ₂ˣ: +1 iff a X² + b Y² = Z² has a nontrivial solution, else -1.

Equations

GQ2.HilbertSymbol.hilbertSymbol a b = if GQ2.HilbertSymbol.IsHilbertSolvable ↑a ↑b then 1 else -1

Instances For

Elementary identities (theorems, from the definition) #

Serre's residue characters `ε` and `ω` (CiA Ch. II §3.3) #

ε and ω depend only on u (mod 8), so they factor through the reduction ℤ₂ → ℤ/8. We define them by the literal formulas (u-1)/2 and (u²-1)/8 on the residue's canonical representative ZMod.val ∈ {0,…,7} (both numerators are divisible by 2, resp. 8, on the odd residues).

source

def GQ2.HilbertSymbol.epsResidue (r : ZMod 8) :

ZMod 2

ε on residues: (r - 1)/2 mod 2, using the representative r.val ∈ {0,…,7}.

Equations

GQ2.HilbertSymbol.epsResidue r = ↑((r.val - 1) / 2)

Instances For

source

def GQ2.HilbertSymbol.omegaResidue (r : ZMod 8) :

ZMod 2

ω on residues: (r² - 1)/8 mod 2, using the representative r.val ∈ {0,…,7}.

Equations

GQ2.HilbertSymbol.omegaResidue r = ↑((r.val ^ 2 - 1) / 8)

Instances For

source

noncomputable def GQ2.HilbertSymbol.ε (u : ℤ_[2]ˣ) :

ZMod 2

ε(u) ≡ (u - 1)/2 (mod 2) — Serre, A Course in Arithmetic, Ch. II §3.3.

Equations

GQ2.HilbertSymbol.ε u = GQ2.HilbertSymbol.epsResidue ((PadicInt.toZModPow 3) ↑u)

Instances For

source

noncomputable def GQ2.HilbertSymbol.ω (u : ℤ_[2]ˣ) :

ZMod 2

ω(u) ≡ (u² - 1)/8 (mod 2) — Serre, A Course in Arithmetic, Ch. II §3.3.

Equations

GQ2.HilbertSymbol.ω u = GQ2.HilbertSymbol.omegaResidue ((PadicInt.toZModPow 3) ↑u)

Instances For

source

theorem GQ2.HilbertSymbol.toZModPow_neg_one :

(PadicInt.toZModPow 3) ↑(-1) = -1

The reduction of the unit -1 ∈ ℤ₂ˣ is -1 ∈ ℤ/8.

source

theorem GQ2.HilbertSymbol.ε_neg_one :

ε (-1) = 1

ε(-1) = 1 (as -1 ≡ 3 (mod 4)); checks the ℤ₂ˣ → 𝔽₂ reduction, not just the residue.

source

theorem GQ2.HilbertSymbol.ω_neg_one :

ω (-1) = 0

ω(-1) = 0 (as -1 ≡ -1 (mod 8)); checks the ℤ₂ˣ → 𝔽₂ reduction, not just the residue.

Inputs of the dyadic Hilbert-symbol formula (former axiom B7′) #

The statement itself — (2^α u, 2^β v)₂ = (-1)^{ε(u)ε(v) + αω(v) + βω(u)}, Serre CiA III §1.2 Thm 1 — lives in GQ2/Foundations/Axioms.lean (GQ2.HilbertSymbol.hilbertSymbol_dyadic) as a theorem proved in GQ2/HilbertSymbolDyadicClose.lean, together with its faithfulness check (-1,-1)₂ = -1. Here we provide the two decomposition inputs of its statement.

source

noncomputable def GQ2.HilbertSymbol.unit2 :

ℚ_[2]ˣ

The unit 2 ∈ ℚ₂ˣ.

Equations