Module

PublicIdealNormArtinKernel.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.PublicIdealNormArtinKernel

3 declarations indexed from sourceView source ↗

Module documentation

Ideal norms lie in the normalized Artin kernel

The forward inclusion of the ideal-theoretic norm-kernel formula follows prime by prime. The reverse inclusion needs a separate approximation argument and is not asserted here.

Imports5

Imported by2

theorem

publicIdealNormDomain_eq_source

L28 ↗

ClassFieldTheory.GlobalClassFieldComparison.publicIdealNormDomain_eq_source

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.GlobalClassFieldComparison

Lean source · statement

theorem publicIdealNormDomain_eq_source
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
    (m : RayClassModulus K) :
    rayClassPrimeToIdealNormDomain K L m =
      RayClass.primeToModulusIdeals
        (RayClass.idealNormLiftedModulus (K := K) (L := L)
          (rayClassModulusToOriginal K m))

theorem

fractionalIdealNorm_prime

L64 ↗

ClassFieldTheory.GlobalClassFieldComparison.fractionalIdealNorm_prime

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.GlobalClassFieldComparison

Lean source · statement

theorem fractionalIdealNorm_prime
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
    (W : HeightOneSpectrum (𝓞 L)) :
    fractionalIdealNorm K L (finitePrimeFractionalIdeal W) =
      finitePrimeFractionalIdeal (fractionalIdealNormPrimeBelow K L W) ^
        (W.asIdeal.inertiaDeg (𝓞 K) : ℤ)

theorem

idealNormImage_le_finiteAbelianReciprocityArtinKer

L112 ↗

ClassFieldTheory.GlobalClassFieldComparison.idealNormImage_le_finiteAbelianReciprocityArtinKer

Documentation

Every ideal norm prime to a modulus is killed by the Frobenius-normalized Artin map. This is the forward half of the ideal-theoretic norm-kernel formula, with no idèle norm substituted for an ideal norm.

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.GlobalClassFieldComparison

Lean source · statement

theorem idealNormImage_le_finiteAbelianReciprocityArtinKer
    (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 lie in the normalized Artin kernel

Declarations

publicIdealNormDomain_eq_source

fractionalIdealNorm_prime

idealNormImage_le_finiteAbelianReciprocityArtinKer