NYLL
Module

UnramifiedPrimeNormClass.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.UnramifiedPrimeNormClass
8 declarations indexed from sourceView source ↗

Module documentation

Prime norm classes at unramified finite places

For a finite abelian extension of number fields, the normalized order-one element at a finite place defines a class in the chosen local norm quotient. Under local reciprocity this class is the actual prime Artin element in the chosen decomposition group.

At a chosen unramified place, its order is therefore the local degree, and its triviality is equivalent to complete splitting. The one-place local-to-global norm map sends this local class to the corresponding prime class in the global idèle-class norm quotient, so the order of the global class divides the local degree.

Imports4
Imported by1

Declarations

theorem

unramifiedPrimeNormClassGroupIsMulCommutative

L36 ↗
GlobalClassFieldTheory.GlobalClassFields.unramifiedPrimeNormClassGroupIsMulCommutative
Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
Lean source · statement
theorem unramifiedPrimeNormClassGroupIsMulCommutative
    (F : Type) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
def

finitePlacePrimeNormClass

L54 ↗
GlobalClassFieldTheory.GlobalClassFields.finitePlacePrimeNormClass
Documentation

The class of the normalized order-one local element in the chosen finite-place norm quotient.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
attribute [local instance] unramifiedPrimeNormClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FiniteGalois
variable [IsGalois K L]
Lean source · statement
def finitePlacePrimeNormClass
    (v : HeightOneSpectrum (𝓞 K)) :
    _root_.ChosenFinitePlaceNormQuotient
      (K := K) (L := L) v
theorem

finitePlaceNormQuotientToGlobalClass_finitePlacePrimeNormClass

L66 ↗
GlobalClassFieldTheory.GlobalClassFields.finitePlaceNormQuotientToGlobalClass_finitePlacePrimeNormClass
Documentation

The one-place local-to-global norm map sends the local prime norm class to the corresponding prime class in the global idèle-class norm quotient.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
attribute [local instance] unramifiedPrimeNormClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FiniteGalois
variable [IsGalois K L]
Lean source · statement
theorem finitePlaceNormQuotientToGlobalClass_finitePlacePrimeNormClass
    (v : HeightOneSpectrum (𝓞 K)) :
    Reciprocity.finitePlaceNormQuotientToGlobalClass
        (K := K) (L := L) v
        (finitePlacePrimeNormClass
          (K := K) (L := L) v) =
      ideleClassNormFrobeniusClass
        (K := K) (L := L) v
theorem

coe_chosenFinitePlaceNormQuotientEquivDecompositionGroup_finitePlacePrimeNormClass

L94 ↗
GlobalClassFieldTheory.GlobalClassFields.coe_chosenFinitePlaceNormQuotientEquivDecompositionGroup_finitePlacePrimeNormClass
Documentation

The local prime norm class corresponds to the actual prime Artin element under the finite-place reciprocity equivalence.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
attribute [local instance] unramifiedPrimeNormClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
variable [IsAbelianGalois K L]
Lean source · statement
theorem
    coe_chosenFinitePlaceNormQuotientEquivDecompositionGroup_finitePlacePrimeNormClass
    (v : HeightOneSpectrum (𝓞 K)) :
    ((chosenFinitePlaceNormQuotientEquivDecompositionGroup
          (K := K) (L := L) v
          (finitePlacePrimeNormClass
            (K := K) (L := L) v) :
        _root_.finitePlaceDecompositionGroup
          (K := K) (L := L) v) :
      L ≃ₐ[K] L) =
      finitePlacePrimeArtin (K := K) (L := L) v
theorem

orderOf_finitePlacePrimeNormClass_dvd_finitePlaceLocalDegree

L128 ↗
GlobalClassFieldTheory.GlobalClassFields.orderOf_finitePlacePrimeNormClass_dvd_finitePlaceLocalDegree
Documentation

The order of the local prime norm class always divides the local extension degree.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
attribute [local instance] unramifiedPrimeNormClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
variable [IsAbelianGalois K L]
Lean source · statement
theorem orderOf_finitePlacePrimeNormClass_dvd_finitePlaceLocalDegree
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf
        (finitePlacePrimeNormClass
          (K := K) (L := L) v) ∣
      _root_.finitePlaceLocalDegree
        (K := K) (L := L) v
theorem

orderOf_finitePlacePrimeNormClass_eq_finitePlaceLocalDegree_of_chosenUnramified

L146 ↗
GlobalClassFieldTheory.GlobalClassFields.orderOf_finitePlacePrimeNormClass_eq_finitePlaceLocalDegree_of_chosenUnramified
Documentation

At a chosen unramified finite place, the order of the local prime norm class is the local extension degree.

Source context 8 commands

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

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

finitePlacePrimeNormClass_eq_one_iff_splitsCompletely_of_chosenUnramified

L205 ↗
GlobalClassFieldTheory.GlobalClassFields.finitePlacePrimeNormClass_eq_one_iff_splitsCompletely_of_chosenUnramified
Documentation

At a chosen unramified finite place, the local prime norm class is trivial exactly when the place splits completely.

Source context 8 commands

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

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

orderOf_ideleClassNormFrobeniusClass_dvd_finitePlaceLocalDegree

L225 ↗
GlobalClassFieldTheory.GlobalClassFields.orderOf_ideleClassNormFrobeniusClass_dvd_finitePlaceLocalDegree
Documentation

The order of the global idèle-class norm prime class always divides the local extension degree.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
attribute [local instance] unramifiedPrimeNormClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
variable [IsAbelianGalois K L]
Lean source · statement
theorem orderOf_ideleClassNormFrobeniusClass_dvd_finitePlaceLocalDegree
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf
        (ideleClassNormFrobeniusClass
          (K := K) (L := L) v) ∣
      _root_.finitePlaceLocalDegree
        (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.