Finite global reciprocity

Mathematical statement

Let $L/K$ be a finite abelian extension of number fields. There are a modulus $\mathfrak m$ and a surjective homomorphism

$$\operatorname{Art}_{L/K,\mathfrak m}:\mathrm{Cl}_{\mathfrak m}(K)\longrightarrow\operatorname{Gal}(L/K).$$

Here $\mathrm{Cl}_{\mathfrak m}(K)$ is the ray class group of modulus $\mathfrak m$.

The extension is unramified away from $\mathfrak m$. For a finite prime $\mathfrak p$ outside its finite support and a prime $\mathfrak P$ above $\mathfrak p$, the map sends $[\mathfrak p]$ to the arithmetic Frobenius at $\mathfrak P$.

Lean code

`ClassFieldTheory.finiteAbelianGlobalReciprocity`

Published library source ↗Same source in NYLL ↗

theorem finiteAbelianGlobalReciprocity
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L] :
    Nonempty (FiniteAbelianReciprocityData K L)

In-scope Lean context

open scoped NumberField

noncomputable section

namespace ClassFieldTheory

Full declaration and proof

/-- A finite abelian extension admits a Frobenius-normalized finite Artin map
through a ray class group. -/
theorem finiteAbelianGlobalReciprocity
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L] :
    Nonempty (FiniteAbelianReciprocityData K L) := by
  let m := GlobalClassFieldComparison.normConductorRayClassModulus K L
  let hram : IsUnramifiedOutsideModulus K L m :=
    GlobalClassFieldComparison.normConductorRayClassModulus_unramifiedOutside K L
  refine ⟨{
    modulus := m
    unramifiedOutsideModulus := hram
    artin := GlobalClassFieldComparison.normConductorArtin K L
    artin_surjective := GlobalClassFieldComparison.normConductorArtin_surjective K L
    artin_frobenius := ?_
  }⟩
  intro v hv w hw
  calc
    GlobalClassFieldComparison.normConductorArtin K L (rayClassOfFinitePrime m v hv) =
        GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
          (K := K) (L := L) v :=
      GlobalClassFieldComparison.normConductorArtin_prime K L v hv
    _ = arithmeticFrobeniusAt (K := K) w :=
      GlobalClassFieldComparison.arithmeticPrimeArtin_eq_arithmeticFrobeniusAt
        (K := K) (L := L) v w hw (hram.1 v hv w.asIdeal inferInstance hw)

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

J. S. Milne. Class Field Theory, version 4.03. 2020. Author's notes, dated 6 August 2020. Chapters I, III, V, VII, and VIII give complementary formulations and historical notes.