NYLL
Module

ArithmeticUnramifiedPrimeArtin.lean

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

Module documentation

Arithmetic Frobenius at an unramified finite place

The pre-existing local class-formation coordinate has geometric Frobenius normalization. This file supplies the canonical prime Artin element used in the ideal-theoretic formulation: the ordinary normalized prime idèle maps to arithmetic Frobenius.

Imports5
Imported by11

Declarations

def

arithmeticFinitePlacePrimeArtin

L41 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
Documentation

The arithmetic global Artin element of the ordinary normalized one-place prime idèle.

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 arithmeticFinitePlacePrimeArtin
    (v : HeightOneSpectrum (𝓞 K)) :
    L ≃ₐ[K] L
theorem

arithmeticFinitePlacePrimeArtin_eq_arithmeticChosenFinitePlaceArtin

L50 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin_eq_arithmeticChosenFinitePlaceArtin
Documentation

The arithmetic prime Artin element is the arithmetic chosen local Artin value of the normalized order-one 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 arithmeticFinitePlacePrimeArtin_eq_arithmeticChosenFinitePlaceArtin
    (v : HeightOneSpectrum (𝓞 K)) :
    arithmeticFinitePlacePrimeArtin (K := K) (L := L) v =
      Reciprocity.arithmeticChosenFinitePlaceArtinMonoidHom
        K L v (FiniteIdeleGroup.chosenLocalOrderSection v 1)
theorem

arithmeticFinitePlacePrimeArtin_eq_inv

L61 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin_eq_inv
Documentation

Arithmetic and geometric prime Artin elements are inverse automorphisms.

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 arithmeticFinitePlacePrimeArtin_eq_inv
    (v : HeightOneSpectrum (𝓞 K)) :
    arithmeticFinitePlacePrimeArtin (K := K) (L := L) v =
      (finitePlacePrimeArtin (K := K) (L := L) v)⁻¹
def

chosenFinitePlaceArithmeticFrobenius

L73 ↗
GlobalClassFieldTheory.GlobalClassFields.chosenFinitePlaceArithmeticFrobenius
Documentation

The arithmetic Frobenius of the actual chosen completed extension, transported through its decomposition group into the global Galois group. The unramifiedness hypothesis concerns this chosen extension, not an unrelated abstract local field.

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 chosenFinitePlaceArithmeticFrobenius
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    L ≃ₐ[K] L
theorem

arithmeticFinitePlacePrimeArtin_eq_chosenFinitePlaceArithmeticFrobenius

L90 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin_eq_chosenFinitePlaceArithmeticFrobenius
Documentation

At an unramified chosen finite place, the arithmetic prime Artin element really is the global decomposition-group transport of local arithmetic Frobenius. The local input has valuation -1 in the construction's convention, and arithmetic global reciprocity inverts that geometric local Artin value.

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 arithmeticFinitePlacePrimeArtin_eq_chosenFinitePlaceArithmeticFrobenius
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    arithmeticFinitePlacePrimeArtin (K := K) (L := L) v =
      chosenFinitePlaceArithmeticFrobenius
        (K := K) (L := L) v hunram
theorem

orderOf_arithmeticFinitePlacePrimeArtin_eq_finitePlaceLocalDegree_of_chosenUnramified

L122 ↗
GlobalClassFieldTheory.GlobalClassFields.orderOf_arithmeticFinitePlacePrimeArtin_eq_finitePlaceLocalDegree_of_chosenUnramified
Documentation

At an unramified chosen place, the arithmetic prime Artin element has order equal to 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_arithmeticFinitePlacePrimeArtin_eq_finitePlaceLocalDegree_of_chosenUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    orderOf
        (arithmeticFinitePlacePrimeArtin
          (K := K) (L := L) v) =
      _root_.finitePlaceLocalDegree
        (K := K) (L := L) v
theorem

arithmeticFinitePlacePrimeArtin_eq_one_iff_splitsCompletely_of_chosenUnramified

L141 ↗
GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin_eq_one_iff_splitsCompletely_of_chosenUnramified
Documentation

An unramified finite place splits completely exactly when its arithmetic Frobenius is trivial.

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
    arithmeticFinitePlacePrimeArtin_eq_one_iff_splitsCompletely_of_chosenUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    arithmeticFinitePlacePrimeArtin
          (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.