The local symbol of two units at a tame exponent

Let K be a nonarchimedean local field containing a primitive n-th root of unity ζ, where the residue characteristic of K does not divide n. Then the local symbol (a, b) along kummerCupPairing ζ hζ vanishes whenever a and b are units of the valuation ring. The extension K(ⁿ√b) is unramified, because an n-th root of a unit lies in the maximal unramified extension, and every unit is a norm from an unramified extension; the symbol–norm criterion then gives (a, b) = 0.

This is the local input for the finiteness of the Hilbert symbols of two global elements: away from the places above n and the places at which a or b is not a unit, their local symbols vanish.

Main results

• TauCeti.ClassFieldTheory.localSymbol_kummerClass_eq_zero_of_mem_unitFiltration: the local symbol of two units vanishes when the residue characteristic does not divide n.

References

• J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer (1979), Chapter XIV, §3, Proposition 8.
• J. Neukirch, Algebraic Number Theory, Springer (1999), Chapter V, §3, Proposition 3.4.

theorem TauCeti.ClassFieldTheory.localSymbol_kummerClass_eq_zero_of_mem_unitFiltration {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) (hp : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n) {a b : Kˣ} (ha : a ∈ unitFiltration K 0) (hb : b ∈ unitFiltration K 0) : ((localSymbol (kummerCupPairing ζ hζ) tr) (kummerClass K ⋯ a)) (kummerClass K ⋯ b) = 0

The local symbol of two units vanishes at a tame exponent. Let K be a nonarchimedean local field containing a primitive n-th root of unity ζ, with n prime to the residue characteristic. If a and b are units of the valuation ring of K, then their local symbol along kummerCupPairing ζ hζ is 0, for every identification tr : H²(G_K, μₙ) ≃+ ZMod n.