Module

FiniteAbelianGlobalReciprocity.lean

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FiniteAbelianGlobalReciprocity

1 declaration indexed from sourceView source ↗

Module documentation

Finite abelian global reciprocity

For a finite abelian extension L/K, global reciprocity supplies a modulus and a surjective Artin map from its ray class group to Gal(L/K). The extension is unramified away from that modulus, and prime classes are sent to Mathlib's arithmetic Frobenius elements.

The statement is ideal-theoretic; its proof transports the existing idelic reciprocity construction through the ray class comparison.

Imports3

Imported by1

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.All

theorem

finiteAbelianGlobalReciprocity

L31 ↗

ClassFieldTheory.finiteAbelianGlobalReciprocity

Documentation

A finite abelian extension admits a Frobenius-normalized finite Artin map through a ray class group.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
noncomputable section
namespace ClassFieldTheory

Lean source · statement

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

Module documentation

Finite abelian global reciprocity

Declarations

finiteAbelianGlobalReciprocity