Module

RayClassIdealNormImageEqArtinKer.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassIdealNormImageEqArtinKer

1 declaration indexed from sourceView source ↗

Module documentation

The ideal norm subgroup is the Artin kernel

This is the ideal-theoretic norm-kernel form of finite abelian reciprocity. The ideal norms are norms of fractional ideals prime to the modulus; the principal ray ideals are absorbed by the ray quotient.

Imports4

Imported by2

theorem

rayClassIdealNormImage_eq_artinKer

L29 ↗

ClassFieldTheory.rayClassIdealNormImage_eq_artinKer

Documentation

For finite abelian reciprocity data, the image of genuine ideal norms in the ideal ray class group equals the normalized Artin kernel.

Source context 4 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem rayClassIdealNormImage_eq_artinKer
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (D : FiniteAbelianReciprocityData K L) :
    rayClassIdealNormImage K L D.modulus = D.artin.ker

Module documentation

The ideal norm subgroup is the Artin kernel

Declarations

rayClassIdealNormImage_eq_artinKer