theorem · Class Field Theory

Finite local reciprocity

A finite abelian extension is recovered as a quotient of the base field's multiplicative group by its norm subgroup.

The norm subgroup tells precisely when two elements of the base field induce the same Galois automorphism. This turns questions about an extension into multiplicative arithmetic within the base field. Serre's Local Fields presents this finite form of reciprocity through the cohomological approach associated with Hochschild and Artin–Tate, providing a starting point for the broader local theory.

ClassFieldTheory on GitHub ↗

Mathematical statement

Let $K$ be a nonarchimedean local field, with its valuative topology, and let $L/K$ be a finite abelian Galois extension. There exists a continuous surjective homomorphism

$$\operatorname{Art}_{L/K}:K^\times\longrightarrow\operatorname{Gal}(L/K),\qquad \ker(\operatorname{Art}_{L/K})=N_{L/K}(L^\times).$$

Here $N_{L/K}(L^\times)$ is the subgroup of field norms.

Lean code

`ClassFieldTheory.finiteAbelianLocalReciprocity`

Published library source ↗Same source in NYLL ↗

theorem finiteAbelianLocalReciprocity
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∃ artin : Kˣ →ₜ* (L ≃ₐ[K] L),
      Function.Surjective artin ∧
      ∀ x : Kˣ, artin x = 1 ↔ IsFieldNorm K L x

In-scope Lean context

noncomputable section

namespace ClassFieldTheory

Full declaration and proof

/-- A finite abelian local extension has a surjective continuous Artin map
whose kernel is its field-norm subgroup. -/
theorem finiteAbelianLocalReciprocity
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∃ artin : Kˣ →ₜ* (L ≃ₐ[K] L),
      Function.Surjective artin ∧
      ∀ x : Kˣ, artin x = 1 ↔ IsFieldNorm K L x := by
  exact LocalCFT.finiteAbelianLocalReciprocity K L

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