Hilbert reciprocity

Let K be a number field and a, b ∈ Kˣ. Hilbert's reciprocity law says that the local Hilbert invariants of a and b at all the places of K sum to zero (hilbertProductFormula). In its cohomological form it is the statement that the local invariants of the Brauer class (a) ∪ (b), the cup product of the Kummer classes of a and b, sum to zero: by finiteInvAt_kummerBrauerClass and infiniteInvAt_kummerBrauerClass these local invariants are the Hilbert invariants read in ℚ/ℤ (sumLocalInv_brLocalization_kummerBrauerClass). The local invariants of every Brauer class of K sum to zero (sumLocalInv_brLocalization_eq_zero), and so Hilbert reciprocity holds.

Main results

• TauCeti.ClassFieldTheory.sumLocalInv_brLocalization_kummerBrauerClass: the sum of the local invariants of the quadratic Kummer-cup class is the sum of the Hilbert invariants, read in ℚ/ℤ.
• TauCeti.ClassFieldTheory.hilbertProductFormula: Hilbert reciprocity over every number field.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, Example 8.2, Lemmas 8.4 and 8.5, and Theorem 8.1.
• J. Neukirch, Algebraic Number Theory, Springer (1999), Chapter VI, §8.
• J.-P. Serre, A Course in Arithmetic, Springer (1973), Chapter III, §2, Theorem 3.

theorem TauCeti.ClassFieldTheory.sumLocalInv_brLocalization_kummerBrauerClass {K : Type} [Field K] [NumberField K] (a b : Kˣ) : (sumLocalInv K) ((brLocalization K) (kummerBrauerClass (-1) ⋯ a b)) = (ZMod.toRatAddCircle 2) (∑ v ∈ finiteHilbertSupport K a b, finiteHilbertInvariantAt K v a b + ∑ w : NumberField.InfinitePlace K, infiniteHilbertInvariantAt K w a b)

The sum of the local invariants of the quadratic Kummer-cup class is the sum of the Hilbert invariants. For a, b ∈ Kˣ, the sum of the local invariants of the Brauer class (a) ∪ (b) over all places of K is the sum of the Hilbert invariants of a and b, read in ℚ/ℤ through k ↦ k/2.

theorem TauCeti.ClassFieldTheory.hilbertProductFormula {K : Type} [Field K] [NumberField K] (a b : Kˣ) : ∑ v ∈ finiteHilbertSupport K a b, finiteHilbertInvariantAt K v a b + ∑ w : NumberField.InfinitePlace K, infiniteHilbertInvariantAt K w a b = 0

Hilbert reciprocity. For a, b ∈ Kˣ, the Hilbert invariants of a and b at all the finite and infinite places of the number field K sum to zero.