The Steinberg relation for cup products of Kummer classes

Let K be a field and n a natural number invertible in K. Cupping the Kummer classes (a), (b) ∈ H¹(G_K, μₙ) along an equivariant biadditive pairing μ : μₙ × μₙ → P into a discrete G_K-module gives a class (a) ⌣ (b) ∈ H²(G_K, P). This file proves the Steinberg relation: (a) ⌣ (b) = 0 whenever a + b = 1. It holds for every such pairing, in particular for the pairing μₙ × μₙ → μₙ attached to a primitive nth root of unity of K, through which the local Hilbert symbol is defined.

The proof is Tate's. Factor Xⁿ - a over K into monic irreducible polynomials f. In the field L_f = K[X]/(f) the root θ_f of f satisfies θ_fⁿ = a, so a becomes an nth power in L_f, while f(1) = N_{L_f/K}(1 - θ_f). Hence b = 1 - a = ∏_f N_{L_f/K}(1 - θ_f) is a product of norms. For a finite extension L/K in which a is an nth power, the Kummer class of a norm is a corestriction (TauCeti.kummerCor_kummerMap), so by the projection formula TauCeti.ContCohomology.explicitCup_projection11

(a) ⌣ (N_{L/K} c) = (a) ⌣ cor (c) = cor (res (a) ⌣ (c)) = 0,

because the restriction of (a) to G_L is the Kummer class of an nth power.

Everything is stated on the explicit low-degree cohomology of G_K = Gal(Kˢ/K), where the Kummer map TauCeti.kummerMap and the projection formula live.

Main results

• TauCeti.explicitRes1_kummerMap_eq_zero: the Kummer class of a restricts to zero on the subgroup fixing the image of an extension in which a is an nth power.
• TauCeti.explicitCup11_kummerMap_normUnits_eq_zero: (a) ⌣ (N_{L/K} c) = 0 for a finite extension L/K in which a is an nth power.
• TauCeti.explicitCup11_kummerMap_eq_zero_of_add_eq_one: the Steinberg relation (a) ⌣ (b) = 0 for a + b = 1.

References

• J. Tate, Relations between K₂ and Galois cohomology, Invent. Math. 36 (1976), 257–274.
• J.-P. Serre, Local Fields, GTM 67, Chapter XIV, §2.

theorem TauCeti.explicitRes1_kummerMap_eq_zero {K : Type u} [Field K] {n : ℕ} (hn : IsUnit ↑n) {L : Type v} [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) {a : Kˣ} {β : Lˣ} (hβ : β ^ n = (Units.map ↑(algebraMap K L)) a) : (ContCohomology.explicitRes1 (AbsoluteGaloisGroup K) (KummerCoeff K n) σ.fieldRange.fixingSubgroup) (Multiplicative.toAdd ((kummerMap K n hn) a)) = 0

The Kummer class of a dies where a becomes an nth power: if a = βⁿ in an extension L of K, then the Kummer class of a restricts to zero on the subgroup of G_K fixing the image of any K-embedding σ : L →ₐ[K] Kˢ. It is represented there by the cocycle g ↦ g (σ β) / σ β, which is identically 1.

theorem TauCeti.explicitCup11_kummerMap_normUnits_eq_zero {K : Type u} [Field K] {n : ℕ} {P : Type u_1} [AddCommGroup P] [TopologicalSpace P] [DiscreteTopology P] [DistribMulAction (AbsoluteGaloisGroup K) P] [ContinuousSMul (AbsoluteGaloisGroup K) P] (μ : KummerCoeff K n →+ KummerCoeff K n →+ P) (hμ : ∀ (g : AbsoluteGaloisGroup K) (x y : KummerCoeff K n), (μ (g • x)) (g • y) = g • (μ x) y) (hn : IsUnit ↑n) {L : Type v} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) {a : Kˣ} {β : Lˣ} (hβ : β ^ n = (Units.map ↑(algebraMap K L)) a) (c : Lˣ) : ((ContCohomology.explicitCup11 (AbsoluteGaloisGroup K) (KummerCoeff K n) (KummerCoeff K n) P μ ⋯ hμ) (Multiplicative.toAdd ((kummerMap K n hn) a))) (Multiplicative.toAdd ((kummerMap K n hn) ((Algebra.normUnits K) c))) = 0

The Kummer class of a cups to zero with every norm from an extension in which a is an nth power: if a = βⁿ in a finite extension L/K, then (a) ⌣ (N_{L/K} c) = 0 for every c ∈ Lˣ. The Kummer class of the norm is the corestriction of the Kummer class of c, and by the projection formula (a) ⌣ cor (c) = cor (res (a) ⌣ (c)), where res (a) = 0 by TauCeti.explicitRes1_kummerMap_eq_zero.

theorem TauCeti.explicitCup11_kummerMap_eq_zero_of_add_eq_one {K : Type u} [Field K] {n : ℕ} {P : Type u_1} [AddCommGroup P] [TopologicalSpace P] [DiscreteTopology P] [DistribMulAction (AbsoluteGaloisGroup K) P] [ContinuousSMul (AbsoluteGaloisGroup K) P] (μ : KummerCoeff K n →+ KummerCoeff K n →+ P) (hμ : ∀ (g : AbsoluteGaloisGroup K) (x y : KummerCoeff K n), (μ (g • x)) (g • y) = g • (μ x) y) (hn : IsUnit ↑n) {a b : Kˣ} (hab : ↑a + ↑b = 1) : ((ContCohomology.explicitCup11 (AbsoluteGaloisGroup K) (KummerCoeff K n) (KummerCoeff K n) P μ ⋯ hμ) (Multiplicative.toAdd ((kummerMap K n hn) a))) (Multiplicative.toAdd ((kummerMap K n hn) b)) = 0

The Steinberg relation (Tate): for n invertible in K and units a, b of K with a + b = 1, the cup product (a) ⌣ (b) ∈ H²(G_K, P) of their Kummer classes vanishes, for every equivariant biadditive pairing μ : μₙ × μₙ → P.