Kummer-cup Brauer classes

A primitive root of unity selects a pairing on Kummer coefficients. The cup of two Kummer classes, followed by the coefficient inclusion into the Brauer group, defines kummerBrauerClass. This file records its bilinearity, torsion and Steinberg relation.

References

• J.-P. Serre, Local Fields, Chapter XIV, §2.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, (6.2.1).

noncomputable def TauCeti.ClassFieldTheory.kummerBrauerClass {K : Type u} [Field K] {n : ℕ} [NeZero n] (ζ : K) (hζ : IsPrimitiveRoot ζ n) (a b : Kˣ) : Br K

The Brauer class of the cup of two Kummer classes, using the pairing selected by ζ.

theorem TauCeti.ClassFieldTheory.kummerBrauerClass_def {K : Type u} [Field K] {n : ℕ} [NeZero n] (ζ : K) (hζ : IsPrimitiveRoot ζ n) (a b : Kˣ) : kummerBrauerClass ζ hζ a b = (h2MuToBr n K) ((((kummerCupPairing ζ hζ).cup 1 1) (kummerClass K ⋯ a)) (kummerClass K ⋯ b))

The Kummer-cup Brauer class is the canonical cup followed by the coefficient inclusion.

@[simp]

theorem TauCeti.ClassFieldTheory.kummerBrauerClass_one_left {K : Type u} [Field K] {n : ℕ} [NeZero n] (ζ : K) (hζ : IsPrimitiveRoot ζ n) (b : Kˣ) : kummerBrauerClass ζ hζ 1 b = 0

The argument 1 on the left gives the zero Brauer class.

@[simp]

theorem TauCeti.ClassFieldTheory.kummerBrauerClass_one_right {K : Type u} [Field K] {n : ℕ} [NeZero n] (ζ : K) (hζ : IsPrimitiveRoot ζ n) (a : Kˣ) : kummerBrauerClass ζ hζ a 1 = 0

The argument 1 on the right gives the zero Brauer class.

theorem TauCeti.ClassFieldTheory.kummerBrauerClass_mul_left {K : Type u} [Field K] {n : ℕ} [NeZero n] (ζ : K) (hζ : IsPrimitiveRoot ζ n) (a a' b : Kˣ) : kummerBrauerClass ζ hζ (a * a') b = kummerBrauerClass ζ hζ a b + kummerBrauerClass ζ hζ a' b

The Kummer-cup Brauer class is additive in its first unit argument.

theorem TauCeti.ClassFieldTheory.kummerBrauerClass_mul_right {K : Type u} [Field K] {n : ℕ} [NeZero n] (ζ : K) (hζ : IsPrimitiveRoot ζ n) (a b b' : Kˣ) : kummerBrauerClass ζ hζ a (b * b') = kummerBrauerClass ζ hζ a b + kummerBrauerClass ζ hζ a b'

The Kummer-cup Brauer class is additive in its second unit argument.

theorem TauCeti.ClassFieldTheory.nsmul_kummerBrauerClass_eq_zero {K : Type u} [Field K] {n : ℕ} [NeZero n] (ζ : K) (hζ : IsPrimitiveRoot ζ n) (a b : Kˣ) : n • kummerBrauerClass ζ hζ a b = 0

The Kummer-cup Brauer class is killed by its exponent.

theorem TauCeti.ClassFieldTheory.kummerBrauerClass_eq_zero_of_add_eq_one {K : Type u} [Field K] {n : ℕ} [NeZero n] (ζ : K) (hζ : IsPrimitiveRoot ζ n) {a b : Kˣ} (hab : ↑a + ↑b = 1) : kummerBrauerClass ζ hζ a b = 0

The Kummer-cup Brauer class satisfies the Steinberg relation.