Base change of Kummer-cup Brauer classes

A primitive root of unity selects a pairing on Kummer coefficients. The cup product of two Kummer classes, followed by the inclusion into the Brauer group, commutes with arbitrary field extension, including extension to a completion. Thus the local symbols of a global pair are invariants of the localizations of one global Brauer class.

The construction uses the existing Kummer map, explicit cup product and coefficient dictionaries; it introduces no new cohomology carrier. The root of unity is transported along the field map, so the statement preserves the chosen normalization.

References

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

theorem TauCeti.ClassFieldTheory.brBaseChange_h2MuToBr_muNRepH2Equiv {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (n : ℕ) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (x : ContCohomology.H2 (AbsoluteGaloisGroup K) (KummerCoeff K n)) : (brBaseChange K L) ((h2MuToBr n K) ((muNRepH2Equiv n K) x)) = (h2MuToBr n L) ((muNRepH2Equiv n L) ((ContCohomology.explicitMap2 (AbsoluteGaloisGroup K) (KummerCoeff K n) (AbsoluteGaloisGroup L) (KummerCoeff L n) (absoluteGaloisGroupMap τ) (kummerCoeffBaseChange n τ) ⋯ ⋯) x))

Base change commutes with the inclusion of roots-of-unity cohomology into the Brauer group, read on the explicit roots-of-unity model.

theorem TauCeti.ClassFieldTheory.kummerCoeffBaseChange_kummerCoeffPairing {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {n : ℕ} [NeZero n] (ζ : K) (hζ : IsPrimitiveRoot ζ n) (x y : KummerCoeff K n) : (kummerCoeffBaseChange n τ) (((kummerCoeffPairing (kummerCupPairing ζ hζ)) x) y) = ((kummerCoeffPairing (kummerCupPairing ((algebraMap K L) ζ) ⋯)) ((kummerCoeffBaseChange n τ) x)) ((kummerCoeffBaseChange n τ) y)

Transporting roots of unity preserves the coefficient pairing selected by a primitive root, provided that root is transported along the field map as well.

theorem TauCeti.ClassFieldTheory.brBaseChange_kummerBrauerClass {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] {n : ℕ} [NeZero n] (ζ : K) (hζ : IsPrimitiveRoot ζ n) (a b : Kˣ) : (brBaseChange K L) (kummerBrauerClass ζ hζ a b) = kummerBrauerClass ((algebraMap K L) ζ) ⋯ ((Units.map ↑(algebraMap K L)) a) ((Units.map ↑(algebraMap K L)) b)

Kummer-cup Brauer classes commute with arbitrary field extension.