Nyll | Reservoir

ClassFieldTheory (Lean 4.35.0-rc2)

Developed as part of NYLL, this Lean library treats class field theory for nonarchimedean local fields, number fields and function fields over finite fields. The mathematical guide presents reciprocity, existence and the other selected results with their mathematical hypotheses and links to the formal proofs.

Main results

Local class field theory

Let K be a nonarchimedean local field.

Result	Mathematical content
Finite abelian reciprocity	For each finite abelian extension L/K, a continuous surjective Artin map Kˣ → Gal(L/K) has kernel N(Lˣ).
Existence and classification	Finite abelian extensions in a fixed separable closure correspond, with reversed inclusion, to open finite-index subgroups of Kˣ via norms.

Global class field theory: number fields

Let K be a number field.

Result	Mathematical content
Finite abelian reciprocity	Each finite abelian extension L/K admits a modulus and a surjective ray-class Artin map to Gal(L/K), sending prime classes away from the modulus to arithmetic Frobenius.
Class-field existence	Every subgroup of a ray class group is the kernel of the Frobenius-normalized Artin map of a finite abelian extension.

Global class field theory: function fields

Let K be a function field in one variable over a finite field k.

Result	Mathematical content
Finite abelian reciprocity	For each finite abelian extension L/K, the Artin map identifies C_K / N(C_L) with Gal(L/K), where C denotes the idèle class group.
Class-field existence and uniqueness	Every open finite-index subgroup of C_K in its usual topology is the norm subgroup of a unique finite abelian extension in a fixed separable closure.

Public API

Use leanprover/lean4:v4.35.0-rc2 and the Mathlib revision pinned in lake-manifest.json. Add this dependency to your project’s lakefile.toml:

[[require]]
name = "Nyll"
git = "https://github.com/n-yamaguchi-0729/ClassFieldTheory.git"
rev = "main"

Run lake update Nyll, then commit your generated lake-manifest.json to retain the resolved revisions. Import the library in a Lean file:

import Nyll.ClassFieldTheory.All

The standalone distributions share the package name Nyll. Choose one distribution; for several libraries together, use NYLL.

To build a checkout of this repository, run from its root:

lake exe cache get
lake --wfail build

Nyll0.1.0-dev