theorem · Class Field Theory

Profinite local reciprocity

All finite abelian local extensions fit into one topological isomorphism.

Passing to the inverse limit retains exactly the finite continuous quotients of the multiplicative group that matter for abelian Galois theory. The completion is therefore essential: it incorporates the topology while bringing all finite extensions into one description. Lubin and Tate's 1965 formal-group construction gives an explicit perspective on these extensions, complementary to the cohomological approach presented by Serre.

ClassFieldTheory on GitHub ↗

Mathematical statement

For a nonarchimedean local field $K$, let $\widehat{K^\times}_{\mathrm{top}}$ be the inverse limit of $K^\times/U$ over open normal subgroups $U$ of finite index. Then

$$\widehat{K^\times}_{\mathrm{top}}\ \simeq_{\mathrm{top}}\ G_K^{\mathrm{ab}},\qquad G_K=\operatorname{Gal}(K^{\mathrm{sep}}/K).$$

The right side is the topological abelianization: the quotient by the closure of the commutator subgroup.

Lean code

`ClassFieldTheory.profiniteLocalReciprocity`

Published library source ↗Same source in NYLL ↗

theorem profiniteLocalReciprocity
    (K : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Nonempty
      (LocalClassFieldTheory.TopologicalProfiniteCompletion Kˣ ≃ₜ*
        _root_.Field.absoluteGaloisGroupAbelianization K)

In-scope Lean context

noncomputable section

namespace ClassFieldTheory

Full declaration and proof

/-- **Profinite local reciprocity.** The topological profinite completion of
the multiplicative group of a nonarchimedean local field is continuously
multiplicatively equivalent to its absolute Galois abelianization. -/
theorem profiniteLocalReciprocity
    (K : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Nonempty
      (LocalClassFieldTheory.TopologicalProfiniteCompletion Kˣ ≃ₜ*
        _root_.Field.absoluteGaloisGroupAbelianization K) := by
  exact ⟨LocalClassFieldTheory.profiniteLocalReciprocity K⟩

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.
Jonathan Lubin and John Tate. Formal Complex Multiplication in Local Fields. Annals of Mathematics, Second Series, 81 (2), 380–387, 1965. Original paper on the explicit formal-group construction of local abelian extensions; included as historical context, not as a claim that every proof below follows this construction.

Published source: 26f52ca8.

← All selected results in Class Field Theory