NYLL
Module

UnramifiedPrimeArtin.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.UnramifiedPrimeArtin
7 declarations indexed from sourceView source ↗

Module documentation

Prime Artin elements at unramified finite places

For a finite abelian extension of number fields, the global Artin image of the normalized one-place prime idèle is the chosen local Artin image of an element of normalized order one.

At a chosen unramified finite place, integral units lie in the local norm group. Consequently the local Artin symbol depends only on normalized order, the prime Artin element generates the full decomposition group, and its order is the local degree. This gives the genuine decomposition law: the prime Artin element is trivial exactly when the place splits completely.

Imports5
Imported by4

Declarations

def

finitePlacePrimeArtin

L47 ↗
GlobalClassFieldTheory.GlobalClassFields.finitePlacePrimeArtin
Documentation

The actual global Artin element of the normalized one-place prime idèle at a finite place.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
def finitePlacePrimeArtin
    (v : HeightOneSpectrum (𝓞 K)) :
    L ≃ₐ[K] L
theorem

finitePlacePrimeArtin_eq_chosenFinitePlaceArtin

L56 ↗
GlobalClassFieldTheory.GlobalClassFields.finitePlacePrimeArtin_eq_chosenFinitePlaceArtin
Documentation

The global prime Artin element is the chosen local Artin image of the normalized order-one local element.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem finitePlacePrimeArtin_eq_chosenFinitePlaceArtin
    (v : HeightOneSpectrum (𝓞 K)) :
    finitePlacePrimeArtin (K := K) (L := L) v =
      Reciprocity.chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v
        (FiniteIdeleGroup.chosenLocalOrderSection v 1)
theorem

chosenFinitePlaceArtin_eq_of_localOrder_eq_of_chosenUnramified

L67 ↗
GlobalClassFieldTheory.GlobalClassFields.chosenFinitePlaceArtin_eq_of_localOrder_eq_of_chosenUnramified
Documentation

At a chosen unramified finite place, two local elements of equal normalized order have the same local Artin symbol.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem
    chosenFinitePlaceArtin_eq_of_localOrder_eq_of_chosenUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v)
    {x y : (v.adicCompletion K)ˣ}
    (hxy :
      FiniteIdeleGroup.localOrder v x =
        FiniteIdeleGroup.localOrder v y) :
    Reciprocity.chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v x =
      Reciprocity.chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v y
theorem

chosenFinitePlaceArtin_eq_primeArtin_zpow_of_chosenUnramified

L108 ↗
GlobalClassFieldTheory.GlobalClassFields.chosenFinitePlaceArtin_eq_primeArtin_zpow_of_chosenUnramified
Documentation

At a chosen unramified finite place, every local Artin symbol is a power of the normalized prime Artin element, with exponent its normalized local order.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem
    chosenFinitePlaceArtin_eq_primeArtin_zpow_of_chosenUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v)
    (x : (v.adicCompletion K)ˣ) :
    Reciprocity.chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v x =
      finitePlacePrimeArtin (K := K) (L := L) v ^
        (FiniteIdeleGroup.localOrder v x).toAdd
theorem

finitePlaceDecompositionGroup_eq_zpowers_finitePlacePrimeArtin_of_chosenUnramified

L145 ↗
GlobalClassFieldTheory.GlobalClassFields.finitePlaceDecompositionGroup_eq_zpowers_finitePlacePrimeArtin_of_chosenUnramified
Documentation

At a chosen unramified finite place, the prime Artin element generates the actual decomposition group.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem
    finitePlaceDecompositionGroup_eq_zpowers_finitePlacePrimeArtin_of_chosenUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    _root_.finitePlaceDecompositionGroup
        (K := K) (L := L) v =
      Subgroup.zpowers
        (finitePlacePrimeArtin
          (K := K) (L := L) v)
theorem

orderOf_finitePlacePrimeArtin_eq_finitePlaceLocalDegree_of_chosenUnramified

L180 ↗
GlobalClassFieldTheory.GlobalClassFields.orderOf_finitePlacePrimeArtin_eq_finitePlaceLocalDegree_of_chosenUnramified
Documentation

At a chosen unramified finite place, the order of the actual prime Artin element is the local extension degree.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem
    orderOf_finitePlacePrimeArtin_eq_finitePlaceLocalDegree_of_chosenUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    orderOf
        (finitePlacePrimeArtin
          (K := K) (L := L) v) =
      _root_.finitePlaceLocalDegree
        (K := K) (L := L) v
theorem

finitePlacePrimeArtin_eq_one_iff_splitsCompletely_of_chosenUnramified

L217 ↗
GlobalClassFieldTheory.GlobalClassFields.finitePlacePrimeArtin_eq_one_iff_splitsCompletely_of_chosenUnramified
Documentation

At a chosen unramified finite place, the actual prime Artin element is trivial exactly when the place splits completely.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem
    finitePlacePrimeArtin_eq_one_iff_splitsCompletely_of_chosenUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    finitePlacePrimeArtin
          (K := K) (L := L) v =
        1 ↔
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.