Module

RayClassIdealNormImageLeArtinKer.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassIdealNormImageLeArtinKer

1 declaration indexed from sourceView source ↗

Module documentation

Ideal norms are killed by the ray-class Artin map

This is the forward direction of the ideal-theoretic norm-kernel formula. The subgroup is formed from actual fractional-ideal norms, not from idèle norms. Equality requires the separate reverse approximation theorem.

Imports3

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

rayClassIdealNormImage_le_artinKer

L27 ↗

ClassFieldTheory.rayClassIdealNormImage_le_artinKer

Documentation

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

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 rayClassIdealNormImage_le_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

Ideal norms are killed by the ray-class Artin map

Declarations

rayClassIdealNormImage_le_artinKer