Hilbert symbols of global units at the finite places

For a, b ∈ Kˣ in a number field K, the Hilbert symbol (a_v, b_v)_v of their images in the completion K_v at a finite place v is 1 at every place v not above 2 at which a and b are units: there the norm equation x² - a y² = b is solved in the ring of integers of K_v by Hensel's lemma. The excluded places are finitely many, so the family of localized symbols has finite multiplicative support. The lemma carries @[fun_prop], so fun_prop extends this to finite products of such symbols, such as ∏_{i<j} (a_i, a_j)_v for the coefficients a_i of a diagonal form ⟨a₁, …, aₙ⟩.

Finite support is what makes the products of these signs over all finite places finite products, as they occur in the product formula for the Hilbert symbol and for the Hasse invariant of a global form.

Main results

• TauCeti.hilbertSymbol_mul_left_adicCompletion: over the completion at a finite place, the symbol is multiplicative in its first argument.
• TauCeti.hilbertSymbol_eq_one_of_valued_eq_one: over the completion at a finite place not above 2, the symbol of two elements of valuation 1 is 1.
• TauCeti.hilbertSymbol_unitAtFinitePlace_eq_one: the localized symbol is 1 at a finite place at which 2, a and b are units.
• TauCeti.hasFiniteMulSupport_hilbertSymbol_of_eventually_valued_eq_one: the symbol of a family of elements of the completions that are almost all local units, with a localized global element, is 1 at all but finitely many finite places.
• TauCeti.hasFiniteMulSupport_hilbertSymbol_unitAtFinitePlace: the localized symbol is 1 at all but finitely many finite places.
• TauCeti.hilbertSymbol_unitAtFinitePlace_rat: for K = ℚ, the localized symbol at the place above a prime ℓ is the Hilbert symbol over ℚ_ℓ.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 63:11, 66:6 and 71:18.
• J.-P. Serre, A Course in Arithmetic, Chapter III, §1.2, Theorem 1.

theorem TauCeti.hilbertSymbol_mul_left_adicCompletion {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a a' c : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : hilbertSymbol (a * a') c = hilbertSymbol a c * hilbertSymbol a' c

Multiplicativity of the Hilbert symbol at a finite place. Over the completion K_v at a finite place v, the Hilbert symbol is multiplicative in its first argument: (a a', c)_v = (a, c)_v (a', c)_v.

theorem TauCeti.hilbertSymbol_eq_one_of_valued_eq_one {K : Type u_1} [Field K] [NumberField K] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (h2 : (IsDedekindDomain.HeightOneSpectrum.valuation K v) 2 = 1) {u u' : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ} (hu : Valued.v ↑u = 1) (hu' : Valued.v ↑u' = 1) : hilbertSymbol u u' = 1

The Hilbert symbol of two local units at a nondyadic place. If 2 is a unit at the finite place v, then the Hilbert symbol over the completion K_v of two elements of valuation 1 is 1.

@[simp]

theorem TauCeti.hilbertSymbol_unitAtFinitePlace_eq_one {K : Type u_1} [Field K] [NumberField K] {a b : Kˣ} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (h2 : (IsDedekindDomain.HeightOneSpectrum.valuation K v) 2 = 1) (ha : (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑a = 1) (hb : (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑b = 1) : hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b) = 1

The Hilbert symbol at a good finite place. If 2, a and b are units at the finite place v, then the Hilbert symbol of the images of a and b in the completion K_v is 1.

theorem TauCeti.hasFiniteMulSupport_hilbertSymbol_of_eventually_valued_eq_one {K : Type u_1} [Field K] [NumberField K] {c : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ} (hc : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) in Filter.cofinite, Valued.v ↑(c v) = 1) (b : Kˣ) : Function.HasFiniteMulSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => hilbertSymbol (c v) (v.unitAtFinitePlace b)

Finite support of the local symbols of almost-everywhere local units. If c_v ∈ K_vˣ has valuation 1 at all but finitely many finite places v, then for b ∈ Kˣ the Hilbert symbol of c_v and the image of b in K_v is 1 at all but finitely many finite places v.

theorem TauCeti.hasFiniteMulSupport_hilbertSymbol_unitAtFinitePlace {K : Type u_1} [Field K] [NumberField K] (a b : Kˣ) : Function.HasFiniteMulSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b)

Finite support of the localized Hilbert symbol. For a, b ∈ Kˣ, the Hilbert symbol of the images of a and b in the completion K_v is 1 at all but finitely many finite places v.

theorem TauCeti.hilbertSymbol_unitAtFinitePlace_rat (ℓ : Nat.Primes) (a b : ℚˣ) : hilbertSymbol ((Rat.HeightOneSpectrum.primesEquiv.symm ℓ).unitAtFinitePlace a) ((Rat.HeightOneSpectrum.primesEquiv.symm ℓ).unitAtFinitePlace b) = hilbertSymbol ((Units.map ↑(algebraMap ℚ ℚ_[↑ℓ])) a) ((Units.map ↑(algebraMap ℚ ℚ_[↑ℓ])) b)

The Hilbert symbol at a finite place of ℚ is the Hilbert symbol over ℚ_ℓ. For a prime ℓ and a, b ∈ ℚˣ, the Hilbert symbol of the images of a and b in the completion of ℚ at the place above ℓ is their Hilbert symbol over ℚ_ℓ.