Module

RationalCyclotomicArithmeticReciprocity.lean

Nyll.ClassFieldTheory.KroneckerWeber.RationalCyclotomicArithmeticReciprocity

13 declarations indexed from sourceView source ↗

Module documentation

Arithmetic reciprocity for rational cyclotomic ray class fields

This module uses an ordinary rational uniformizer, not its inverse, and the arithmetic global norm-residue map. Consequently an unramified prime q acts on roots of unity by the direct power q. The finite Galois/ray-class comparison is retained as a ContinuousMulEquiv with the native quotient and finite Krull topologies.

Imports2

Imported by2

def

rationalPrimeUniformizerLocalInput

L32 ↗

KroneckerWeber.rationalPrimeUniformizerLocalInput

Documentation

The ordinary rational uniformizer at q, transported to the adic-completion model used by idèles.

Source context 6 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity

Lean source · statement

def rationalPrimeUniformizerLocalInput
    (q : Nat.Primes) :
    ((RayClass.rationalPrime q).adicCompletion ℚ)ˣ

theorem

rationalPrimeUniformizerLocalInput_valuationMap

L41 ↗

KroneckerWeber.rationalPrimeUniformizerLocalInput_valuationMap

Documentation

In the absolute-value logarithmic coordinate, an ordinary uniformizer has value -1.

Source context 6 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity

Lean source · statement

theorem rationalPrimeUniformizerLocalInput_valuationMap
    (q : Nat.Primes) :
    LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap
        (NumberField.HeightOneSpectrum.adicAbv ℚ
          (RayClass.rationalPrime q)).Completion
        (Additive.ofMul
          ((finitePlaceCompletionUnitsContinuousMulEquiv
            (RayClass.rationalPrime q)).symm
            (rationalPrimeUniformizerLocalInput q))) =
      -1

theorem

rationalPrimeArithmeticFrobeniusLocalInput_eq_inv_uniformizer

L58 ↗

KroneckerWeber.rationalPrimeArithmeticFrobeniusLocalInput_eq_inv_uniformizer

Documentation

The previously used value-one absolute-logarithmic input is the inverse of the ordinary uniformizer.

Source context 6 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity

Lean source · statement

theorem rationalPrimeArithmeticFrobeniusLocalInput_eq_inv_uniformizer
    (q : Nat.Primes) :
    rationalPrimeArithmeticFrobeniusLocalInput q =
      (rationalPrimeUniformizerLocalInput q)⁻¹

instance

(anonymous instance)

L69 ↗

Source context 8 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity
section NonzeroOrder
variable (m : ℕ) [NeZero m]

Lean source · statement

instance : NeZero (m : ℚ)

instance

(anonymous instance)

L72 ↗

Source context 9 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity
section NonzeroOrder
variable (m : ℕ) [NeZero m]
local instance : NeZero (m : ℚ) :=
  ⟨by exact_mod_cast (NeZero.ne m)⟩

Lean source · statement

instance :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)

instance

rationalCyclotomicArithmeticLevelIsCyclotomicExtension

L79 ↗

KroneckerWeber.rationalCyclotomicArithmeticLevelIsCyclotomicExtension

Source context 10 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity
section NonzeroOrder
variable (m : ℕ) [NeZero m]
local instance : NeZero (m : ℚ) :=
  ⟨by exact_mod_cast (NeZero.ne m)⟩
noncomputable local instance :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨m, NeZero.pos m⟩

Lean source · statement

instance
    rationalCyclotomicArithmeticLevelIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)

instance

rationalCyclotomicArithmeticLevelIsAbelianGalois

L92 ↗

KroneckerWeber.rationalCyclotomicArithmeticLevelIsAbelianGalois

Source context 11 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity
section NonzeroOrder
variable (m : ℕ) [NeZero m]
local instance : NeZero (m : ℚ) :=
  ⟨by exact_mod_cast (NeZero.ne m)⟩
noncomputable local instance :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨m, NeZero.pos m⟩
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) := by
  change
    IsCyclotomicExtension
      {((⟨m, NeZero.pos m⟩ : ℕ+) : ℕ)} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)
  exact
    KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension _

Lean source · statement

instance
    rationalCyclotomicArithmeticLevelIsAbelianGalois :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)

theorem

arithmeticGlobalNormResidue_uniformizer_eq_globalNormResidue_inverseUniformizer

L102 ↗

KroneckerWeber.arithmeticGlobalNormResidue_uniformizer_eq_globalNormResidue_inverseUniformizer

Documentation

Arithmetic reciprocity on the ordinary uniformizer agrees literally with geometric reciprocity on its inverse. This equality fixes the normalization independently of the cyclotomic character.

Source context 12 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity
section NonzeroOrder
variable (m : ℕ) [NeZero m]
local instance : NeZero (m : ℚ) :=
  ⟨by exact_mod_cast (NeZero.ne m)⟩
noncomputable local instance :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨m, NeZero.pos m⟩
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) := by
  change
    IsCyclotomicExtension
      {((⟨m, NeZero.pos m⟩ : ℕ+) : ℕ)} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)
  exact
    KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension _
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsAbelianGalois :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ _

Lean source · statement

theorem
    arithmeticGlobalNormResidue_uniformizer_eq_globalNormResidue_inverseUniformizer
    (q : Nat.Primes) :
    arithmeticGlobalNormResidueMonoidHom
        ℚ
        (KummerTheory.rationalCyclotomicLevel
          ⟨m, NeZero.pos m⟩)
        (IdeleGroup.finitePlaceIdeleClass
          (RayClass.rationalPrime q)
          (rationalPrimeUniformizerLocalInput q)) =
      globalNormResidueMonoidHom
        ℚ
        (KummerTheory.rationalCyclotomicLevel
          ⟨m, NeZero.pos m⟩)
        (IdeleGroup.finitePlaceIdeleClass
          (RayClass.rationalPrime q)
          (rationalPrimeArithmeticFrobeniusLocalInput q))

theorem

rationalCyclotomicLevel_arithmeticGlobalNormResidue_at_unramifiedPrime

L141 ↗

KroneckerWeber.rationalCyclotomicLevel_arithmeticGlobalNormResidue_at_unramifiedPrime

Documentation

At q ∤ m, the arithmetic global norm-residue symbol of the ordinary one-place uniformizer is arithmetic Frobenius ζ ↦ ζ ^ q.

Source context 12 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity
section NonzeroOrder
variable (m : ℕ) [NeZero m]
local instance : NeZero (m : ℚ) :=
  ⟨by exact_mod_cast (NeZero.ne m)⟩
noncomputable local instance :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨m, NeZero.pos m⟩
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) := by
  change
    IsCyclotomicExtension
      {((⟨m, NeZero.pos m⟩ : ℕ+) : ℕ)} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)
  exact
    KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension _
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsAbelianGalois :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ _

Lean source · statement

theorem
    rationalCyclotomicLevel_arithmeticGlobalNormResidue_at_unramifiedPrime
    (q : Nat.Primes) (hq : ¬ q.1 ∣ m) :
    IsCyclotomicExtension.Rat.galEquivZMod
        m
        (KummerTheory.rationalCyclotomicLevel
          ⟨m, NeZero.pos m⟩)
        (arithmeticGlobalNormResidueMonoidHom
          ℚ
          (KummerTheory.rationalCyclotomicLevel
            ⟨m, NeZero.pos m⟩)
          (IdeleGroup.finitePlaceIdeleClass
            (RayClass.rationalPrime q)
            (rationalPrimeUniformizerLocalInput q))) =
      ZMod.unitOfCoprime q.1
        (q.2.coprime_iff_not_dvd.mpr hq)

def

rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup

L165 ↗

KroneckerWeber.rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup

Documentation

Arithmetic-Frobenius-normalized topological reciprocity for the actual finite cyclotomic level inside the fixed rational separable closure.

Source context 12 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity
section NonzeroOrder
variable (m : ℕ) [NeZero m]
local instance : NeZero (m : ℚ) :=
  ⟨by exact_mod_cast (NeZero.ne m)⟩
noncomputable local instance :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨m, NeZero.pos m⟩
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) := by
  change
    IsCyclotomicExtension
      {((⟨m, NeZero.pos m⟩ : ℕ+) : ℕ)} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)
  exact
    KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension _
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsAbelianGalois :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ _

Lean source · statement

def
    rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup
    :
    Gal(
        KummerTheory.rationalCyclotomicLevel
          ⟨m, NeZero.pos m⟩ / ℚ) ≃ₜ*
      RayClass.RayClassGroup (RayClass.rationalModulus m)

theorem

rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup_arithmeticGlobalNormResidue

L181 ↗

KroneckerWeber.rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup_arithmeticGlobalNormResidue

Documentation

Arithmetic reciprocity sends the arithmetic norm-residue symbol of an idèle class to its genuine rational ray class.

Source context 12 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity
section NonzeroOrder
variable (m : ℕ) [NeZero m]
local instance : NeZero (m : ℚ) :=
  ⟨by exact_mod_cast (NeZero.ne m)⟩
noncomputable local instance :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨m, NeZero.pos m⟩
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) := by
  change
    IsCyclotomicExtension
      {((⟨m, NeZero.pos m⟩ : ℕ+) : ℕ)} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)
  exact
    KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension _
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsAbelianGalois :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ _

Lean source · statement

theorem
  rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup_arithmeticGlobalNormResidue
    (c : IdeleClassGroup ℚ) :
    rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup
        m
        (arithmeticGlobalNormResidueMonoidHom
          ℚ
          (KummerTheory.rationalCyclotomicLevel
            ⟨m, NeZero.pos m⟩) c) =
      QuotientGroup.mk'
        (RayClass.Modulus.congruenceSubgroup
          (RayClass.rationalModulus m)) c

theorem

rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup_symm_mk

L209 ↗

KroneckerWeber.rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup_symm_mk

Documentation

Inverse arithmetic ray reciprocity sends the ray class of an idèle class back to its arithmetic global norm-residue symbol.

Source context 12 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity
section NonzeroOrder
variable (m : ℕ) [NeZero m]
local instance : NeZero (m : ℚ) :=
  ⟨by exact_mod_cast (NeZero.ne m)⟩
noncomputable local instance :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨m, NeZero.pos m⟩
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) := by
  change
    IsCyclotomicExtension
      {((⟨m, NeZero.pos m⟩ : ℕ+) : ℕ)} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)
  exact
    KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension _
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsAbelianGalois :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ _

Lean source · statement

theorem
    rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup_symm_mk
    (c : IdeleClassGroup ℚ) :
    (rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup
        m).symm
        (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup
            (RayClass.rationalModulus m)) c) =
      arithmeticGlobalNormResidueMonoidHom
        ℚ
        (KummerTheory.rationalCyclotomicLevel
          ⟨m, NeZero.pos m⟩) c

theorem

rationalCyclotomicLevel_arithmeticRayReciprocity_at_unramifiedPrime

L232 ↗

KroneckerWeber.rationalCyclotomicLevel_arithmeticRayReciprocity_at_unramifiedPrime

Documentation

The inverse arithmetic ray reciprocity image of the ordinary uniformizer class at q ∤ m has direct cyclotomic exponent q.

Source context 12 commands

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

open scoped IsMulCommutative NumberField Cyclotomic
noncomputable section
namespace KroneckerWeber
open GlobalClassFieldTheory
open GlobalClassFieldTheory.GlobalClassFields
open GlobalClassFieldTheory.Reciprocity
section NonzeroOrder
variable (m : ℕ) [NeZero m]
local instance : NeZero (m : ℚ) :=
  ⟨by exact_mod_cast (NeZero.ne m)⟩
noncomputable local instance :
    NumberField
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  KummerTheory.rationalCyclotomicLevel_numberField
    ⟨m, NeZero.pos m⟩
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) := by
  change
    IsCyclotomicExtension
      {((⟨m, NeZero.pos m⟩ : ℕ+) : ℕ)} ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)
  exact
    KummerTheory.rationalCyclotomicLevel_isCyclotomicExtension _
noncomputable local instance
    rationalCyclotomicArithmeticLevelIsAbelianGalois :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ _

Lean source · statement

theorem
    rationalCyclotomicLevel_arithmeticRayReciprocity_at_unramifiedPrime
    (q : Nat.Primes) (hq : ¬ q.1 ∣ m) :
    IsCyclotomicExtension.Rat.galEquivZMod
        m
        (KummerTheory.rationalCyclotomicLevel
          ⟨m, NeZero.pos m⟩)
        ((rationalCyclotomicLevelArithmeticGaloisContinuousMulEquivRayClassGroup
            m).symm
          (QuotientGroup.mk'
            (RayClass.Modulus.congruenceSubgroup
              (RayClass.rationalModulus m))
            (IdeleGroup.finitePlaceIdeleClass
              (RayClass.rationalPrime q)
              (rationalPrimeUniformizerLocalInput q)))) =
      ZMod.unitOfCoprime q.1
        (q.2.coprime_iff_not_dvd.mpr hq)

Module documentation

Arithmetic reciprocity for rational cyclotomic ray class fields

Declarations