theorem · Class Field Theory

The local existence correspondence

Every open finite-index subgroup is a norm subgroup, with the correct reversal of inclusion.

Reciprocity associates a norm subgroup to an extension; the existence theorem supplies the converse and makes the classification complete. Larger extensions correspond to smaller subgroups, so inclusion questions become comparisons within the base field. This classical complement to reciprocity has an explicit construction through Lubin–Tate theory and is treated alongside local symbols in Serre's Local Fields.

ClassFieldTheory on GitHub ↗

Mathematical statement

Fix a nonarchimedean local field $K$ and a separable closure. Finite abelian intermediate extensions correspond to open finite-index subgroups of $K^\times$ through

$$L\longmapsto N_{L/K}(L^\times).$$

The correspondence reverses inclusion: $L_1\subseteq L_2$ exactly when $N_{L_2/K}(L_2^\times)\subseteq N_{L_1/K}(L_1^\times)$.

Lean code

`ClassFieldTheory.finiteAbelianLocalExistence_orderIso`

Published library source ↗Same source in NYLL ↗

theorem finiteAbelianLocalExistence_orderIso
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
  ∃ e : FiniteAbelianLocalExtension K ≃o
        (OpenFiniteIndexSubgroup K)ᵒᵈ,
      ∀ E : FiniteAbelianLocalExtension K,
        (OrderDual.ofDual (e E)).1 = E.normSubgroup

In-scope Lean context

noncomputable section

namespace ClassFieldTheory

universe u

Full declaration and proof

/-- Finite abelian local extensions correspond contravariantly to open
finite-index norm subgroups. -/
theorem finiteAbelianLocalExistence_orderIso
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
  ∃ e : FiniteAbelianLocalExtension K ≃o
        (OpenFiniteIndexSubgroup K)ᵒᵈ,
      ∀ E : FiniteAbelianLocalExtension K,
        (OrderDual.ofDual (e E)).1 = E.normSubgroup := by
  exact ⟨LocalFieldTheory.shrinkFiniteAbelianFieldNormSubgroupOrderIso K,
    LocalFieldTheory.shrinkFiniteAbelianFieldNormSubgroupOrderIso_apply 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