The cohomological local symbol

Let F be a field and n a natural number invertible in F. Two Kummer classes (a), (b) ∈ H¹(G_F, μₙ) cup naturally into H²(G_F, μₙ ⊗ μₙ), not into H²(G_F, μₙ): multiplication of roots of unity is not biadditive. A primitive nth root of unity ζ ∈ F supplies the missing coefficient pairing kummerCupPairing ζ hζ : μₙ × μₙ → μₙ, (ζ ^ i, y) ↦ y ^ i, which is equivariant because G_F acts trivially on μₙ once ζ ∈ F.

The local symbol localSymbol P tr is the cup product along a coefficient pairing P : μₙ × μₙ → μₙ followed by an identification tr : H²(G_F, μₙ) ≃+ ZMod n, as a ZMod n-bilinear map on H¹(G_F, μₙ). For a local field, with P = kummerCupPairing ζ hζ and tr the local invariant, its values on Kummer classes are the cohomological Hilbert symbol (a, b) = inv ((a) ⌣ (b)). Bilinearity is carried by the type; on Kummer classes it reads (a a', b) = (a, b) + (a', b) and (a, b b') = (a, b) + (a, b').

The Steinberg relation (a, b) = 0 for a + b = 1 is proved for the cup product along every coefficient pairing (cup_kummerClass_eq_zero_of_add_eq_one), by computing the cup product of Kummer classes on explicit cocycles and applying Tate's argument TauCeti.explicitCup11_kummerMap_eq_zero_of_add_eq_one. It is recorded for the local symbol along every coefficient pairing, in particular at the pairing of a primitive root (localSymbol_kummerClass_eq_zero_of_add_eq_one).

The explicit computation goes through kummerCoeffPairing P, the pairing P read on the Kummer coefficients TauCeti.KummerCoeff F n of Gal(Fˢ/F): on classes transported by muNRepH1Equiv, the cup product along P is the transported explicit cup product along kummerCoeffPairing P (cup_muNRepH1Equiv).

Main definitions

• TauCeti.ClassFieldTheory.kummerCoeffPairing: a coefficient pairing on muNRep n F, read on TauCeti.KummerCoeff F n.
• TauCeti.ClassFieldTheory.kummerCupPairing: the coefficient pairing μₙ × μₙ → μₙ of a primitive nth root of unity ζ ∈ F.
• TauCeti.ClassFieldTheory.localSymbol: cup product along a coefficient pairing followed by an identification H²(G_F, μₙ) ≃+ ZMod n.

Main results

• TauCeti.ClassFieldTheory.kummerCoeffPairing_smul: kummerCoeffPairing P is equivariant for Gal(Fˢ/F).
• TauCeti.ClassFieldTheory.cup_muNRepH1Equiv: the cup product along P of transported classes is the transported explicit cup product along kummerCoeffPairing P.
• TauCeti.ClassFieldTheory.kummerCupPairing_bil: the pairing is scalar multiplication by the chosen-root coordinate.
• TauCeti.ClassFieldTheory.kummerCupPairing_bil_apply: the pairing sends (ζ ^ i, y) to i • y.
• TauCeti.ClassFieldTheory.kummerCupPairing_flip: the chosen-root pairing is symmetric as a coefficient pairing.
• TauCeti.ClassFieldTheory.localSymbol_antisymm: the chosen-root local symbol is antisymmetric.
• TauCeti.ClassFieldTheory.muNRepCohomologyEquivTrivialFp_kummerCupPairing_cup: through the chosen-root identification of μₙ with the trivial coefficients ℤ/n, the cup product along kummerCupPairing ζ hζ is the cup square cupFp.
• TauCeti.ClassFieldTheory.localSymbol_kummerClass_mul, TauCeti.ClassFieldTheory.localSymbol_kummerClass_mul_right: bilinearity on Kummer classes.
• TauCeti.ClassFieldTheory.cup_kummerClass_eq_zero_of_add_eq_one: the Steinberg relation for the cup product of Kummer classes along any coefficient pairing.
• TauCeti.ClassFieldTheory.localSymbol_kummerClass_eq_zero_of_add_eq_one: the Steinberg relation for the local symbol along any coefficient pairing.

References

• J.-P. Serre, Local Fields, GTM 67, Chapter XIV, §2, for the cohomological definition of the Hilbert symbol and its Steinberg relation.
• J. Tate, Relations between K₂ and Galois cohomology, Invent. Math. 36 (1976), 257–274.

Cup products on μₙ computed on explicit cocycles

noncomputable def TauCeti.ClassFieldTheory.kummerCoeffPairing {n : ℕ} {F : Type u} [Field F] (P : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)) : KummerCoeff F n →+ KummerCoeff F n →+ KummerCoeff F n

The coefficient pairing P on muNRep n F, read on the Kummer coefficients TauCeti.KummerCoeff F n through the dictionary kummerCoeffEquivMuNRep (kummerCoeffEquivMuNRep_kummerCoeffPairing). It is the pairing along which cup products on muNRep n F are computed on explicit cocycles of Gal(Fˢ/F) (cup_muNRepH1Equiv).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.ClassFieldTheory.kummerCoeffEquivMuNRep_kummerCoeffPairing {n : ℕ} {F : Type u} [Field F] (P : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)) (x y : KummerCoeff F n) : (kummerCoeffEquivMuNRep n F) (((kummerCoeffPairing P) x) y) = (P.bil ((kummerCoeffEquivMuNRep n F) x)) ((kummerCoeffEquivMuNRep n F) y)

kummerCoeffPairing P is P under the dictionary kummerCoeffEquivMuNRep.

theorem TauCeti.ClassFieldTheory.kummerCoeffPairing_smul {n : ℕ} {F : Type u} [Field F] (P : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)) (g : AbsoluteGaloisGroup F) (x y : KummerCoeff F n) : ((kummerCoeffPairing P) (g • x)) (g • y) = g • ((kummerCoeffPairing P) x) y

kummerCoeffPairing P is equivariant for Gal(Fˢ/F), since P is equivariant for G_F.

theorem TauCeti.ClassFieldTheory.cup_muNRepH1Equiv {n : ℕ} {F : Type u} [Field F] (P : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)) (x y : ContCohomology.H1 (AbsoluteGaloisGroup F) (KummerCoeff F n)) : ((P.cup 1 1) ((muNRepH1Equiv n F) x)) ((muNRepH1Equiv n F) y) = (muNRepH2Equiv n F) (((ContCohomology.explicitCup11 (AbsoluteGaloisGroup F) (KummerCoeff F n) (KummerCoeff F n) (KummerCoeff F n) (kummerCoeffPairing P) ⋯ ⋯) x) y)

The cup product along P on explicit cocycles: the cup product along P of classes transported by muNRepH1Equiv is the transport by muNRepH2Equiv of their explicit cup product along kummerCoeffPairing P.

theorem TauCeti.ClassFieldTheory.cup_kummerClass_eq_zero_of_add_eq_one {n : ℕ} {F : Type u} [Field F] (P : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)) (hn : IsUnit ↑n) {a b : Fˣ} (hab : ↑a + ↑b = 1) : ((P.cup 1 1) (kummerClass F hn a)) (kummerClass F hn b) = 0

The Steinberg relation on the coefficient object μₙ: for n invertible in F, units a, b of F with a + b = 1, and any coefficient pairing P : μₙ × μₙ → μₙ, the cup product of the Kummer classes of a and b vanishes.

The coefficient pairing of a primitive root

noncomputable def TauCeti.ClassFieldTheory.kummerCupPairing {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)

The coefficient pairing μₙ × μₙ → μₙ selected by a primitive nth root of unity ζ ∈ F: (ζ ^ i, y) ↦ y ^ i, written additively (ζ ^ i, y) ↦ i • y (kummerCupPairing_bil_apply). It is equivariant because G_F acts trivially on μₙ once ζ ∈ F (muNRep_ρ_apply_eq_self). It is the identification μₙ ⊗ μₙ ≅ μₙ, ζ ⊗ ζ ↦ ζ, through which two Kummer classes cup into μₙ.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.ClassFieldTheory.kummerCupPairing_bil_apply {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) {x : ↑(muNRep n F)} {i : ℤ} (hx : ↑↑(Additive.toMul ((kummerCoeffEquivMuNRep n F).symm x)) = (algebraMap F (SeparableClosure F)) ζ ^ i) (y : ↑(muNRep n F)) : ((kummerCupPairing ζ hζ).bil x) y = i • y

The pairing of a primitive root on powers of it: if x is the root of unity ζ ^ i, then kummerCupPairing ζ hζ pairs x with y to i • y, that is y ^ i multiplicatively. Every x ∈ μₙ is a power of ζ, so this determines the pairing.

@[simp]

theorem TauCeti.ClassFieldTheory.kummerCupPairing_bil {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) (x y : ↑(muNRep n F)) : ((kummerCupPairing ζ hζ).bil x) y = (muNRepEquivZMod ζ hζ) x • y

The Kummer coefficient pairing is scalar multiplication by the chosen-root coordinate.

theorem TauCeti.ClassFieldTheory.kummerCupPairing_bil_comm {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) (x y : ↑(muNRep n F)) : ((kummerCupPairing ζ hζ).bil x) y = ((kummerCupPairing ζ hζ).bil y) x

The coefficient pairing selected by a primitive root is symmetric.

@[simp]

theorem TauCeti.ClassFieldTheory.kummerCupPairing_flip {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) : (kummerCupPairing ζ hζ).flip = kummerCupPairing ζ hζ

The opposite of the chosen-root pairing is itself.

theorem TauCeti.ClassFieldTheory.muNRepCohomologyEquivTrivialFp_kummerCupPairing_cup {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) (x y : ↑(continuousCohomology 1 (muNRep n F)).toModuleCat) : (muNRepCohomologyEquivTrivialFp n F hζ 2) ((((kummerCupPairing ζ hζ).cup 1 1) x) y) = ((cupFp n (Field.absoluteGaloisGroup F)) ((muNRepCohomologyEquivTrivialFp n F hζ 1) x)) ((muNRepCohomologyEquivTrivialFp n F hζ 1) y)

The cup product along the pairing of a primitive root is the cup square with trivial coefficients: under the chosen-root identification muNRepCohomologyEquivTrivialFp of μₙ with the trivial coefficients ℤ/n, the cup product along kummerCupPairing ζ hζ on H¹(G_F, μₙ) is cupFp on H¹(G_F, ℤ/n).

The local symbol

noncomputable def TauCeti.ClassFieldTheory.localSymbol {n : ℕ} {F : Type u} [Field F] (P : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)) (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) : ↑(continuousCohomology 1 (muNRep n F)).toModuleCat →ₗ[ZMod n] ↑(continuousCohomology 1 (muNRep n F)).toModuleCat →ₗ[ZMod n] ZMod n

The cohomological local symbol: the cup product H¹(G_F, μₙ) × H¹(G_F, μₙ) → H²(G_F, μₙ) along a coefficient pairing P, followed by an identification tr : H²(G_F, μₙ) ≃+ ZMod n, as a ZMod n-bilinear map. For a local field, at P = kummerCupPairing ζ hζ and with tr the local invariant, its values on Kummer classes are the cohomological Hilbert symbol.

Equations

• TauCeti.ClassFieldTheory.localSymbol P tr = (P.cup 1 1).compr₂ (AddMonoidHom.toZModLinearMap n tr.toAddMonoidHom)

@[simp]

theorem TauCeti.ClassFieldTheory.localSymbol_apply {n : ℕ} {F : Type u} [Field F] (P : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)) (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (x y : ↑(continuousCohomology 1 (muNRep n F)).toModuleCat) : ((localSymbol P tr) x) y = tr (((P.cup 1 1) x) y)

The local symbol is the cup product followed by tr.

theorem TauCeti.ClassFieldTheory.localSymbol_antisymm_of_flip_eq {n : ℕ} {F : Type u} [Field F] (P : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)) (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (hP : P.flip = P) (x y : ↑(continuousCohomology 1 (muNRep n F)).toModuleCat) : ((localSymbol P tr) x) y = -((localSymbol P tr) y) x

A local symbol whose coefficient pairing is symmetric is antisymmetric.

theorem TauCeti.ClassFieldTheory.localSymbol_kummerClass_mul {n : ℕ} {F : Type u} [Field F] (P : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)) (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (hn : IsUnit ↑n) (a a' b : Fˣ) : ((localSymbol P tr) (kummerClass F hn (a * a'))) (kummerClass F hn b) = ((localSymbol P tr) (kummerClass F hn a)) (kummerClass F hn b) + ((localSymbol P tr) (kummerClass F hn a')) (kummerClass F hn b)

The local symbol is multiplicative in the first unit: (a a', b) = (a, b) + (a', b).

theorem TauCeti.ClassFieldTheory.localSymbol_kummerClass_mul_right {n : ℕ} {F : Type u} [Field F] (P : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)) (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (hn : IsUnit ↑n) (a b b' : Fˣ) : ((localSymbol P tr) (kummerClass F hn a)) (kummerClass F hn (b * b')) = ((localSymbol P tr) (kummerClass F hn a)) (kummerClass F hn b) + ((localSymbol P tr) (kummerClass F hn a)) (kummerClass F hn b')

The local symbol is multiplicative in the second unit: (a, b b') = (a, b) + (a, b').

theorem TauCeti.ClassFieldTheory.localSymbol_kummerClass_eq_zero_of_add_eq_one {n : ℕ} {F : Type u} [Field F] (P : TopPairing (muNRep n F) (muNRep n F) (muNRep n F)) (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (hn : IsUnit ↑n) {a b : Fˣ} (hab : ↑a + ↑b = 1) : ((localSymbol P tr) (kummerClass F hn a)) (kummerClass F hn b) = 0

The Steinberg relation for the local symbol along any coefficient pairing P, in particular along the pairing kummerCupPairing ζ hζ of a primitive nth root of unity ζ ∈ F: (a, b) = 0 whenever a + b = 1.

theorem TauCeti.ClassFieldTheory.localSymbol_antisymm {n : ℕ} {F : Type u} [Field F] [NeZero n] (ζ : F) (hζ : IsPrimitiveRoot ζ n) (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (x y : ↑(continuousCohomology 1 (muNRep n F)).toModuleCat) : ((localSymbol (kummerCupPairing ζ hζ) tr) x) y = -((localSymbol (kummerCupPairing ζ hζ) tr) y) x

Antisymmetry of the chosen-root local symbol: the local symbol along the coefficient pairing of a primitive nth root of unity is antisymmetric, for any identification tr.