Module

ArithmeticIdealArtin.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.ArithmeticIdealArtin

11 declarations indexed from sourceView source ↗

Module documentation

The ideal Artin map in arithmetic Frobenius normalization

For a defining modulus of a genuine finite abelian class field, this module composes the ideal ray-class quotient with the topological arithmetic global norm-residue equivalence. The resulting map sends an ordinary prime ideal to arithmetic Frobenius, has the genuine idèle norm kernel, and induces the canonical ideal class-field isomorphism.

Imports5

Imported by3

def

arithmeticIdealArtinGaloisMap

L45 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap

Documentation

The genuine Galois-valued ideal Artin map in arithmetic Frobenius normalization.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

def arithmeticIdealArtinGaloisMap
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    RayClass.primeToModulusIdeals m →*
      (L ≃ₐ[K] L)

theorem

arithmeticIdealArtinGaloisMap_apply

L60 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap_apply

Documentation

Evaluating the arithmetic ideal Artin map is evaluation of the ideal class map followed by arithmetic global reciprocity.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

theorem arithmeticIdealArtinGaloisMap_apply
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.primeToModulusIdeals m) :
    arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm a =
      Reciprocity.arithmeticGlobalNormResidueContinuousMulEquiv
        K L
        (idealArtinMap m
          ((_root_.ideleClassNorm K L).range) hm a)

theorem

arithmeticIdealArtinGaloisMap_eq_inv_idealArtinGaloisMap

L77 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap_eq_inv_idealArtinGaloisMap

Documentation

The arithmetic ideal Artin map is exactly the inverse of the geometrically normalized map on every ideal.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

theorem arithmeticIdealArtinGaloisMap_eq_inv_idealArtinGaloisMap
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.primeToModulusIdeals m) :
    arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm a =
      (idealArtinGaloisMap
        (K := K) (L := L) m hm a)⁻¹

theorem

arithmeticIdealArtinGaloisMap_surjective

L93 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap_surjective

Documentation

The arithmetic ideal Artin map is surjective.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

theorem arithmeticIdealArtinGaloisMap_surjective
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    Function.Surjective
      (arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm)

theorem

arithmeticIdealArtinGaloisMap_ker

L109 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap_ker

Documentation

Arithmetic normalization leaves the defining ideal group unchanged.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

theorem arithmeticIdealArtinGaloisMap_ker
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    (arithmeticIdealArtinGaloisMap
      (K := K) (L := L) m hm).ker =
      idealArtinKernel m
        ((_root_.ideleClassNorm K L).range) hm

def

arithmeticIdealClassQuotientEquivGaloisGroup

L136 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealClassQuotientEquivGaloisGroup

Documentation

The canonical ideal class-field isomorphism in arithmetic Frobenius normalization.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

def arithmeticIdealClassQuotientEquivGaloisGroup
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    RayClass.primeToModulusIdeals m ⧸
        idealArtinKernel m
          ((_root_.ideleClassNorm K L).range) hm ≃*
      (L ≃ₐ[K] L)

theorem

arithmeticIdealClassQuotientEquivGaloisGroup_mk

L153 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealClassQuotientEquivGaloisGroup_mk

Documentation

The arithmetic ideal class-field equivalence sends a quotient representative to its arithmetic ideal Artin symbol.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

theorem arithmeticIdealClassQuotientEquivGaloisGroup_mk
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.primeToModulusIdeals m) :
    arithmeticIdealClassQuotientEquivGaloisGroup
        (K := K) (L := L) m hm
        (QuotientGroup.mk'
          (idealArtinKernel m
            ((_root_.ideleClassNorm K L).range) hm) a) =
      arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm a

theorem

arithmeticIdealArtinGaloisMap_primeToIdealMap_eq_globalArtin

L170 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap_primeToIdealMap_eq_globalArtin

Documentation

The arithmetic ideal Artin map and the arithmetic idèlic Artin map form the genuine ideal/idèle compatibility square.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

theorem
    arithmeticIdealArtinGaloisMap_primeToIdealMap_eq_globalArtin
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.idelePrimeToModulusSubgroup m) :
    arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm
        (RayClass.primeToIdealMap m a) =
      Reciprocity.arithmeticGlobalArtinMonoidHom
        K L (a : IdeleGroup K)

theorem

arithmeticIdealArtinGaloisMap_primeIdeal_eq_arithmeticFinitePlacePrimeArtin

L199 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap_primeIdeal_eq_arithmeticFinitePlacePrimeArtin

Documentation

A prime ideal outside the defining modulus maps to its genuine arithmetic prime Artin element.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

theorem
    arithmeticIdealArtinGaloisMap_primeIdeal_eq_arithmeticFinitePlacePrimeArtin
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm
        (RayClass.primeToModulusIdeal m v hv) =
      GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := L) v

theorem

arithmeticIdealArtinGaloisMap_primeIdeal_eq_arithmeticChosenFinitePlaceArtin

L222 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap_primeIdeal_eq_arithmeticChosenFinitePlaceArtin

Documentation

Direct local form: a prime ideal outside the modulus maps to the arithmetic chosen local Artin value of normalized order one.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

theorem
    arithmeticIdealArtinGaloisMap_primeIdeal_eq_arithmeticChosenFinitePlaceArtin
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm
        (RayClass.primeToModulusIdeal m v hv) =
      Reciprocity.arithmeticChosenFinitePlaceArtinMonoidHom
        K L v (FiniteIdeleGroup.chosenLocalOrderSection v 1)

theorem

arithmeticIdealClassQuotientEquivGaloisGroup_primeIdeal

L241 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealClassQuotientEquivGaloisGroup_primeIdeal

Documentation

The arithmetic ideal class-field equivalence sends the class of a prime ideal to its arithmetic Frobenius automorphism.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

theorem
    arithmeticIdealClassQuotientEquivGaloisGroup_primeIdeal
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    arithmeticIdealClassQuotientEquivGaloisGroup
        (K := K) (L := L) m hm
        (QuotientGroup.mk'
          (idealArtinKernel m
            ((_root_.ideleClassNorm K L).range) hm)
          (RayClass.primeToModulusIdeal m v hv)) =
      GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := L) v

Module documentation

The ideal Artin map in arithmetic Frobenius normalization

Declarations