The product formula for the norm-equation Hilbert symbol and for the Hasse invariant

For a, b ∈ Kˣ in a number field K, Hilbert's product formula says that the norm-equation Hilbert symbols (a_v, b_v)_v ∈ {±1} multiply to 1 over all the places v of K: the finite places, read in the completions K_v, and the real places, read in ℝ. The complex places contribute nothing, because every element of ℂ is a square.

Hilbert's reciprocity law in its cohomological form is the vanishing of the sum of the local invariants of (a) ∪ (b) in ZMod 2 (TauCeti.ClassFieldTheory.hilbertProductFormula), and the product of the norm-equation symbols over the finite and real places is the sign of that sum (TauCeti.finprod_hilbertSymbol_mul_prod_hilbertSymbol_eq_hilbertSign). For K : Type this gives the norm-equation formula directly, and Shrink.ringEquiv K transports it to number fields in any universe. Over ℚ it reads ∏_ℓ (a, b)_ℓ · (a, b)_∞ = 1 over the primes ℓ and the real place, with the symbols computed in ℚ_ℓ and in ℝ.

Multiplying the product formula over the pairs of coefficients of a diagonalization Q ≅ ⟨a₁, …, aₙ⟩ gives the product formula for the Hasse invariant of a regular form Q: the product of its finite Hasse signs and of its real Hasse signs is 1. With the other conditions already checked in QuadraticForm.isAdmissible_globalInvariants_iff, the system of local invariants of every regular form of positive rank over K is then admissible.

Main results

• TauCeti.hilbertSymbol_productFormula: Hilbert's product formula for the norm-equation symbols over every number field.
• TauCeti.finprod_hilbertSymbol_padic_mul_hilbertSymbol_real_eq_one: the product formula over ℚ, with the local symbols in ℚ_ℓ and ℝ.
• QuadraticForm.globalInvariants_hasseProduct_eq_one: the Hasse product formula for every regular form over a number field.
• QuadraticForm.isAdmissible_globalInvariants: the system of local invariants of every regular form of positive rank over a number field is admissible.

References

• J.-P. Serre, A Course in Arithmetic, Springer (1973), Chapter III, §2, Theorem 3, and Chapter IV, §3.1, condition (1) for the Hasse invariants of a form over ℚ.
• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 71:18, and 72:1 for the conditions satisfied by the local invariants of a global form.

theorem TauCeti.hilbertSymbol_productFormula {K : Type u_1} [Field K] [NumberField K] (a b : Kˣ) : (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b)) * ∏ w : { w : NumberField.InfinitePlace K // w.IsReal }, hilbertSymbol ((unitAtRealPlace w) a) ((unitAtRealPlace w) b) = 1

Hilbert's product formula. For a, b ∈ Kˣ in a number field K, the product of the norm-equation Hilbert symbols (a_v, b_v)_v over the finite places and of the real Hilbert symbols (a_w, b_w)_w over the real places of K is 1.

theorem TauCeti.finprod_hilbertSymbol_padic_mul_hilbertSymbol_real_eq_one (a b : ℚˣ) : (∏ᶠ (ℓ : Nat.Primes), hilbertSymbol ((Units.map ↑(algebraMap ℚ ℚ_[↑ℓ])) a) ((Units.map ↑(algebraMap ℚ ℚ_[↑ℓ])) b)) * hilbertSymbol ((Units.map ↑(algebraMap ℚ ℝ)) a) ((Units.map ↑(algebraMap ℚ ℝ)) b) = 1

Hilbert's product formula over ℚ. For a, b ∈ ℚˣ, the product over the primes ℓ of the Hilbert symbols (a, b)_ℓ computed in ℚ_ℓ, times the Hilbert symbol (a, b)_∞ computed in ℝ, is 1.

@[simp]

theorem QuadraticForm.globalInvariants_hasseProduct_eq_one {K : Type u_1} [Field K] [NumberField K] {V : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : (Q.globalInvariants hQ).hasseProduct = 1

The Hasse product formula. For every regular form Q over a number field K, the product of the finite Hasse signs and of the real Hasse signs of Q is 1.

theorem QuadraticForm.isAdmissible_globalInvariants {K : Type u_1} [Field K] [NumberField K] {V : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hn : 1 ≤ Module.finrank K V) : (Q.globalInvariants hQ).IsAdmissible

The local invariants of a global form are admissible. The system of local invariants of every regular form of positive rank over a number field K is admissible.