The cohomological Hilbert invariants at all places

Let K be a number field and a, b ∈ Kˣ. At a finite place v of K, the Hilbert invariant finiteHilbertInvariantAt K v a b ∈ ZMod 2 is the cohomological local symbol of the images of a and b in the completion K_v: the cup product of their Kummer classes in H¹(G_{K_v}, μ₂) along the pairing of the primitive square root of unity -1, followed by the normalized local invariant H²(G_{K_v}, μ₂) ≃+ ZMod 2, which sends a class of Brauer invariant 1/2 to 1. It is the additive form of the quadratic Hilbert symbol (a, b)_v.

The finite invariant is bilinear and symmetric in a and b, and vanishes at every finite place v not above 2 at which a and b are both units: there K_v(√b) is unramified, so every unit is a norm from it. Only finitely many places are excluded, so the finite invariants of a fixed pair have finite support, the finite set finiteHilbertSupport K a b. The sum of the invariants over that set, together with the archimedean invariants, is the left-hand side of Hilbert's reciprocity law. The comparison finiteInvAt_kummerBrauerClass identifies every finite term with the localization of the global Kummer-cup Brauer class, so this sum can be read in the global Brauer sequence. At an infinite place, the corresponding invariant is defined by the same local cup product and the archimedean invariant map; infiniteInvAt_kummerBrauerClass identifies it with the localization of that same global class. At a real place it is 1 exactly when a and b are both negative there, while at a complex place it is 0; it is again bilinear and symmetric.

Main definitions

• TauCeti.ClassFieldTheory.finiteHilbertInvariantAt K v a b: the cohomological Hilbert invariant of a and b at the finite place v.
• TauCeti.ClassFieldTheory.finiteHilbertSupport K a b: the finite set of the finite places at which it is nonzero.
• TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt K w a b: the cohomological Hilbert invariant at an infinite place, with values in ZMod 2.

Main results

• TauCeti.ClassFieldTheory.toRatAddCircle_finiteHilbertInvariantAt: the invariant, read in ℚ/ℤ, is the Brauer invariant of the cup product of the two Kummer classes.
• TauCeti.ClassFieldTheory.infiniteInvAt_kummerBrauerClass: the infinite-place invariant of the global Kummer-cup Brauer class is the image of infiniteHilbertInvariantAt in ℚ/ℤ.
• TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt_eq_ite_of_isReal: at a real place the invariant is 1 exactly when both arguments are negative.
• TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt_eq_zero_of_isComplex: at a complex place the invariant is 0.
• TauCeti.ClassFieldTheory.finiteHilbertInvariantAt_mul_left, TauCeti.ClassFieldTheory.finiteHilbertInvariantAt_mul_right, TauCeti.ClassFieldTheory.finiteHilbertInvariantAt_comm: bilinearity and symmetry.
• TauCeti.ClassFieldTheory.finiteHilbertInvariantAt_eq_zero_of_valuation_eq_one: the invariant vanishes at a place not above 2 at which a and b are units.
• TauCeti.ClassFieldTheory.hasFiniteSupport_finiteHilbertInvariantAt: it vanishes at all but finitely many finite places.
• TauCeti.ClassFieldTheory.finiteHilbertInvariantAt_eq_zero_of_notMem: it vanishes outside finiteHilbertSupport K a b.

References

• J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer (1979), Chapter XIV, §§2–3.
• J. Neukirch, Algebraic Number Theory, Springer (1999), Chapter V, §3 and Chapter VI, §8.

noncomputable def TauCeti.ClassFieldTheory.finiteHilbertInvariantAt (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a b : Kˣ) : ZMod 2

The cohomological Hilbert invariant at a finite place v of a number field K: the local symbol of the images of a, b ∈ Kˣ in the completion K_v, that is, the cup product of their Kummer classes along the pairing of the primitive square root of unity -1, followed by the normalized local invariant H²(G_{K_v}, μ₂) ≃+ ZMod 2.

theorem TauCeti.ClassFieldTheory.finiteHilbertInvariantAt_def (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a b : Kˣ) (hζ : IsPrimitiveRoot (-1) 2) (h2 : IsUnit 2) : finiteHilbertInvariantAt K v a b = ((localSymbol (kummerCupPairing (-1) hζ) (h2MuEquivZMod (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) h2)) (kummerClass (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) h2 ((Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))) a))) (kummerClass (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) h2 ((Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))) b))

The Hilbert invariant at a finite place is the local symbol of the localized elements, for any proofs that -1 is a primitive square root of unity and that 2 is a unit in K_v.

theorem TauCeti.ClassFieldTheory.toRatAddCircle_finiteHilbertInvariantAt (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a b : Kˣ) (hζ : IsPrimitiveRoot (-1) 2) (h2 : IsUnit 2) : (ZMod.toRatAddCircle 2) (finiteHilbertInvariantAt K v a b) = (invMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((h2MuToBr 2 (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((((kummerCupPairing (-1) hζ).cup 1 1) (kummerClass (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) h2 ((Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))) a))) (kummerClass (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) h2 ((Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))) b))))

The normalization of the Hilbert invariant. Read in ℚ/ℤ through k ↦ k/2, the Hilbert invariant at a finite place is the Brauer invariant of the cup product of the Kummer classes of the localized elements.

theorem TauCeti.ClassFieldTheory.finiteInvAt_kummerBrauerClass (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a b : Kˣ) : (finiteInvAt K v) (kummerBrauerClass (-1) ⋯ a b) = (ZMod.toRatAddCircle 2) (finiteHilbertInvariantAt K v a b)

The finite Hilbert invariant is the local invariant of one global Kummer-cup Brauer class. This identifies the finite terms of Hilbert reciprocity with Brauer localization.

noncomputable def TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt (K : Type) [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (a b : Kˣ) : ZMod 2

The cohomological Hilbert invariant at an infinite place w of a number field K. It is the ZMod 2-valued invariant of the localized global Kummer-cup Brauer class at a real place, and zero at a complex place.

theorem TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt_of_isReal (K : Type) [Field K] [NumberField K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) (a b : Kˣ) : infiniteHilbertInvariantAt K w a b = realInvEquiv ((brCongr (NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal hw)) (kummerBrauerClass ((algebraMap K w.Completion) (-1)) ⋯ ((Units.map ↑(algebraMap K w.Completion)) a) ((Units.map ↑(algebraMap K w.Completion)) b)))

At a real place w, the infinite Hilbert invariant of a and b is the invariant, in Br ℝ ≃ ZMod 2, of the Kummer-cup Brauer class of their images in K_w, carried to ℝ along the isomorphism K_w ≃ ℝ.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt_eq_zero_of_isComplex (K : Type) [Field K] [NumberField K] {w : NumberField.InfinitePlace K} (hw : w.IsComplex) (a b : Kˣ) : infiniteHilbertInvariantAt K w a b = 0

The infinite Hilbert invariant vanishes at a complex place.

theorem TauCeti.ClassFieldTheory.infiniteInvAt_kummerBrauerClass (K : Type) [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (a b : Kˣ) : (infiniteInvAt K w) (kummerBrauerClass (-1) ⋯ a b) = (ZMod.toRatAddCircle 2) (infiniteHilbertInvariantAt K w a b)

The infinite Hilbert invariant is the invariant of the global Kummer-cup Brauer class: localizing kummerBrauerClass (-1) hζ a b at w and applying infiniteInvMap gives the ℚ/ℤ-image of infiniteHilbertInvariantAt.

theorem TauCeti.ClassFieldTheory.toRatAddCircle_infiniteHilbertInvariantAt (K : Type) [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (a b : Kˣ) (hζ : IsPrimitiveRoot (-1) 2) (h2 : IsUnit 2) : (ZMod.toRatAddCircle 2) (infiniteHilbertInvariantAt K w a b) = (infiniteInvMap w) ((h2MuToBr 2 w.Completion) ((((kummerCupPairing (-1) hζ).cup 1 1) (kummerClass w.Completion h2 ((Units.map ↑(algebraMap K w.Completion)) a))) (kummerClass w.Completion h2 ((Units.map ↑(algebraMap K w.Completion)) b))))

The normalization of the Hilbert invariant at an infinite place. Read in ℚ/ℤ through k ↦ k/2, the Hilbert invariant is the archimedean Brauer invariant of the cup product of the localized Kummer classes.

theorem TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt_eq_ite (K : Type) [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (a b : Kˣ) (hζ : IsPrimitiveRoot (-1) 2) (h2 : IsUnit 2) : infiniteHilbertInvariantAt K w a b = if (((kummerCupPairing (-1) hζ).cup 1 1) (kummerClass w.Completion h2 ((Units.map ↑(algebraMap K w.Completion)) a))) (kummerClass w.Completion h2 ((Units.map ↑(algebraMap K w.Completion)) b)) = 0 then 0 else 1

The Hilbert invariant at an infinite place, expressed directly in terms of the cup product of the localized Kummer classes: it is 0 when that cup product vanishes and 1 otherwise.

theorem TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt_eq_zero_iff (K : Type) [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (a b : Kˣ) (hζ : IsPrimitiveRoot (-1) 2) (h2 : IsUnit 2) : infiniteHilbertInvariantAt K w a b = 0 ↔ (((kummerCupPairing (-1) hζ).cup 1 1) (kummerClass w.Completion h2 ((Units.map ↑(algebraMap K w.Completion)) a))) (kummerClass w.Completion h2 ((Units.map ↑(algebraMap K w.Completion)) b)) = 0

The Hilbert invariant at an infinite place vanishes exactly when the cup product of the localized Kummer classes does.

@[simp]

theorem TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt_eq_ite_of_isReal (K : Type) [Field K] [NumberField K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) (a b : Kˣ) : infiniteHilbertInvariantAt K w a b = if (NumberField.InfinitePlace.embedding_of_isReal hw) ↑a < 0 ∧ (NumberField.InfinitePlace.embedding_of_isReal hw) ↑b < 0 then 1 else 0

The Hilbert invariant at a real place is 1 exactly when both a and b are negative there.

theorem TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt_comm (K : Type) [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (a b : Kˣ) : infiniteHilbertInvariantAt K w a b = infiniteHilbertInvariantAt K w b a

The Hilbert invariant at an infinite place is symmetric.

theorem TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt_mul_left (K : Type) [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (a a' b : Kˣ) : infiniteHilbertInvariantAt K w (a * a') b = infiniteHilbertInvariantAt K w a b + infiniteHilbertInvariantAt K w a' b

The Hilbert invariant at an infinite place is additive in its first argument.

theorem TauCeti.ClassFieldTheory.infiniteHilbertInvariantAt_mul_right (K : Type) [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (a b b' : Kˣ) : infiniteHilbertInvariantAt K w a (b * b') = infiniteHilbertInvariantAt K w a b + infiniteHilbertInvariantAt K w a b'

The Hilbert invariant at an infinite place is additive in its second argument.

theorem TauCeti.ClassFieldTheory.finiteHilbertInvariantAt_mul_left (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a a' b : Kˣ) : finiteHilbertInvariantAt K v (a * a') b = finiteHilbertInvariantAt K v a b + finiteHilbertInvariantAt K v a' b

The Hilbert invariant at a finite place is additive in its first argument.

theorem TauCeti.ClassFieldTheory.finiteHilbertInvariantAt_mul_right (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a b b' : Kˣ) : finiteHilbertInvariantAt K v a (b * b') = finiteHilbertInvariantAt K v a b + finiteHilbertInvariantAt K v a b'

The Hilbert invariant at a finite place is additive in its second argument.

theorem TauCeti.ClassFieldTheory.finiteHilbertInvariantAt_comm (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a b : Kˣ) : finiteHilbertInvariantAt K v a b = finiteHilbertInvariantAt K v b a

The Hilbert invariant at a finite place is symmetric.

theorem TauCeti.ClassFieldTheory.finiteHilbertInvariantAt_eq_zero_of_valuation_eq_one (K : Type) [Field K] [NumberField K] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {a b : 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) : finiteHilbertInvariantAt K v a b = 0

The Hilbert invariant at a good finite place. If 2, a and b are units at the finite place v, then the Hilbert invariant of a and b at v vanishes.

theorem TauCeti.ClassFieldTheory.hasFiniteSupport_finiteHilbertInvariantAt (K : Type) [Field K] [NumberField K] (a b : Kˣ) : Function.HasFiniteSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => finiteHilbertInvariantAt K v a b

The Hilbert invariants of a fixed pair have finite support: for a, b ∈ Kˣ, the Hilbert invariant of a and b vanishes at all but finitely many finite places.

noncomputable def TauCeti.ClassFieldTheory.finiteHilbertSupport (K : Type) [Field K] [NumberField K] (a b : Kˣ) : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))

The support of the Hilbert invariants of a, b ∈ Kˣ: the finite set of the finite places at which their Hilbert invariant is nonzero.

@[simp]

theorem TauCeti.ClassFieldTheory.mem_finiteHilbertSupport (K : Type) [Field K] [NumberField K] {a b : Kˣ} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} : v ∈ finiteHilbertSupport K a b ↔ finiteHilbertInvariantAt K v a b ≠ 0

A finite place lies in the support of the Hilbert invariants of a and b exactly when their Hilbert invariant there is nonzero.

theorem TauCeti.ClassFieldTheory.finiteHilbertInvariantAt_eq_zero_of_notMem (K : Type) [Field K] [NumberField K] {a b : Kˣ} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hv : v ∉ finiteHilbertSupport K a b) : finiteHilbertInvariantAt K v a b = 0

Outside its support, the Hilbert invariant of a and b vanishes.