theorem · Class Field Theory

A perfect local Hilbert pairing

Power classes are dual to their roots-of-unity-valued characters.

A nontrivial power class is detected by pairing it with a suitable second class, while a trivial pairing value expresses a norm condition. This turns local norm equations into orthogonality tests and connects Kummer extensions with multiplicative characters. These connections are the classical role of local norm-residue symbols, which Serre treats together with the existence theorem in Local Fields.

ClassFieldTheory on GitHub ↗

Mathematical statement

Let $K$ be a nonarchimedean local field, let $n>0$ be nonzero in $K$, and assume that $K$ contains a primitive $n$th root of unity. Set $P=K^\times/(K^\times)^n$. There exists a bimultiplicative pairing

$$B:P\times P\longrightarrow\mu_n(K),\qquad P\xrightarrow{\;\sim\;}\operatorname{Hom}(P,\mu_n(K)),\quad a\longmapsto B(a,-).$$

It is skew-symmetric, nondegenerate, and satisfies the Steinberg relation. For representatives $a,b\in K^\times$, one has $B([a],[b])=1$ exactly when $b$ is a norm from the Kummer algebra $K[T]/(T^n-a)$.

Lean code

`ClassFieldTheory.exists_perfectLocalHilbertPairing`

Published library source ↗Same source in NYLL ↗

theorem exists_perfectLocalHilbertPairing
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    ∃ B : HilbertPairing K n,
      B.IsLocalHilbertPairing ∧ Function.Bijective B

In-scope Lean context

namespace ClassFieldTheory

universe u

Full declaration and proof

/-- There is a local Hilbert pairing whose adjoint map to the full
`μₙ`-valued character group is bijective. -/
theorem exists_perfectLocalHilbertPairing
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    ∃ B : HilbertPairing K n,
      B.IsLocalHilbertPairing ∧ Function.Bijective B := by
  let : Finite (PowerClassGroup K n) :=
    powerClassGroup_finite K n hnK
  obtain ⟨B, hB⟩ := exists_localHilbertPairing K n hnK hmu
  refine ⟨B, hB, ?_⟩
  exact hB.2.2.1.bijective hmu

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

Jean-Pierre Serre. Local Fields. Springer, New York, Graduate Texts in Mathematics 67, 1979. English translation of Corps locaux; local reciprocity, ramification, local symbols, and the existence theorem.

Published source: 26f52ca8.

← All selected results in Class Field Theory