Nondegeneracy of the local Hilbert pairing

Let K be a nonarchimedean local field containing a primitive n-th root of unity ζ, with n invertible in K. The local symbol (a, b), the cup product of the Kummer classes of a and b along kummerCupPairing ζ hζ followed by an identification H²(G_K, μₙ) ≃+ ZMod n, is a ZMod n-bilinear pairing on H¹(G_K, μₙ) ≃ Kˣ / (Kˣ)ⁿ. This file proves that it is separating in the second variable: b pairs to zero with every a exactly when b is an n-th power.

The argument is Serre's. Let L = K(ⁿ√b). By the symbol–norm criterion (localSymbol_eq_zero_iff_mem_normGroup) every a pairs to zero with b exactly when every a ∈ Kˣ is a norm from L. The extension L/K is cyclic, so by the cyclic norm index [Kˣ : N_{L/K}(Lˣ)] = [L : K] (TauCeti.index_normGroup_of_isCyclic) this forces L = K, that is, b is an n-th power in K. No reciprocity is used, and the identification H²(G_K, μₙ) ≃+ ZMod n is arbitrary.

Main results

• TauCeti.ClassFieldTheory.forall_localSymbol_kummerClass_eq_zero_iff: (a, b) = 0 for every a ∈ Kˣ exactly when b ∈ (Kˣ)ⁿ.
• TauCeti.ClassFieldTheory.separatingRight_localSymbol: the local symbol along kummerCupPairing ζ hζ is separating in its second variable on H¹(G_K, μₙ).

References

• J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer (1979), Chapter XIV, §2.

theorem TauCeti.ClassFieldTheory.forall_localSymbol_kummerClass_eq_zero_iff {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (tr : ↑(continuousCohomology 2 (muNRep n K)).toModuleCat ≃+ ZMod n) (b : Kˣ) : (∀ (a : Kˣ), ((localSymbol (kummerCupPairing ζ hζ) tr) (kummerClass K ⋯ a)) (kummerClass K ⋯ b) = 0) ↔ b ∈ powerSubgroup Kˣ n

Nondegeneracy of the Hilbert pairing in the second variable. Let K be a nonarchimedean local field containing a primitive n-th root of unity ζ. Then b ∈ Kˣ pairs to zero under the local symbol along kummerCupPairing ζ hζ with every a ∈ Kˣ exactly when b is an n-th power. The identification tr : H²(G_K, μₙ) ≃+ ZMod n is arbitrary, and the Kummer classes use the invertibility of n in K supplied by ζ.

theorem TauCeti.ClassFieldTheory.separatingRight_localSymbol {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (tr : ↑(continuousCohomology 2 (muNRep n K)).toModuleCat ≃+ ZMod n) : (localSymbol (kummerCupPairing ζ hζ) tr).SeparatingRight

The Hilbert pairing is separating in the second variable. For a nonarchimedean local field K containing a primitive n-th root of unity ζ, with n invertible in K, the only class y ∈ H¹(G_K, μₙ) with (x, y) = 0 for every x under the local symbol along kummerCupPairing ζ hζ is y = 0. The identification tr : H²(G_K, μₙ) ≃+ ZMod n is arbitrary, and n is invertible in K because K contains a primitive n-th root of unity.