Module

RationalRayClassFieldCyclotomic.lean

Nyll.ClassFieldTheory.KroneckerWeber.RationalRayClassFieldCyclotomic

36 declarations indexed from sourceView source ↗

Module documentation

The rational ray class field as an actual cyclotomic field

For a nonzero natural number m, the selected ray class field for the rational modulus (m) is isomorphic over ℚ to the actual cyclotomic field CyclotomicField m ℚ.

The field comparison is obtained from the exact idèle-class norm-range equality. We also retain the topological content of global reciprocity:

Gal(ℚ(μ_m) / ℚ) ≃ₜ* C_ℚ / C_ℚ^m.

Thus the result is an equality of actual class fields and not merely an equality of degrees or an abstract comparison of finite groups.

Imports3

Imported by3

instance

rationalCyclotomicLevelIsAbelianGalois

L38 ↗

KroneckerWeber.rationalCyclotomicLevelIsAbelianGalois

Source context 7 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
open NumberField IsDedekindDomain

Lean source · statement

instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n)

def

galoisContinuousMulEquivRayClassGroupOfNormRangeEq

L44 ↗

KroneckerWeber.galoisContinuousMulEquivRayClassGroupOfNormRangeEq

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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)

Lean source · statement

def
    galoisContinuousMulEquivRayClassGroupOfNormRangeEq
    (L : Type) [Field L] [NumberField L] [Algebra ℚ L]
    [FiniteDimensional ℚ L] [IsAbelianGalois ℚ L]
    (r : RayClass.Modulus ℚ)
    (h : (_root_.ideleClassNorm ℚ L).range =
      RayClass.Modulus.congruenceSubgroup r) :
    Gal(L / ℚ) ≃ₜ* RayClass.RayClassGroup r

theorem

quotientMulEquivOfNormRangeEq_globalNormResidue

L68 ↗

KroneckerWeber.quotientMulEquivOfNormRangeEq_globalNormResidue

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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)

Lean source · statement

theorem quotientMulEquivOfNormRangeEq_globalNormResidue
    (L : Type) [Field L] [NumberField L] [Algebra ℚ L]
    [FiniteDimensional ℚ L] [IsAbelianGalois ℚ L]
    (H : Subgroup (IdeleClassGroup ℚ))
    [(_root_.ideleClassNorm ℚ L).range.Normal] [H.Normal]
    (h : (_root_.ideleClassNorm ℚ L).range = H)
    (c : IdeleClassGroup ℚ) :
    QuotientGroup.quotientMulEquivOfEq h
        (Additive.toMul
          ((globalNormResidueEquiv ℚ L).symm
            (Additive.ofMul
              (globalNormResidueMonoidHom ℚ L c)))) =
      QuotientGroup.mk' H c

theorem

galoisContinuousMulEquivRayClassGroupOfNormRangeEq_globalNormResidue

L107 ↗

KroneckerWeber.galoisContinuousMulEquivRayClassGroupOfNormRangeEq_globalNormResidue

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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)

Lean source · statement

theorem
    galoisContinuousMulEquivRayClassGroupOfNormRangeEq_globalNormResidue
    (L : Type) [Field L] [NumberField L] [Algebra ℚ L]
    [FiniteDimensional ℚ L] [IsAbelianGalois ℚ L]
    (r : RayClass.Modulus ℚ)
    (h : (_root_.ideleClassNorm ℚ L).range =
      RayClass.Modulus.congruenceSubgroup r)
    (c : IdeleClassGroup ℚ) :
    galoisContinuousMulEquivRayClassGroupOfNormRangeEq L r h
        (globalNormResidueMonoidHom ℚ L c) =
      QuotientGroup.mk'
        (RayClass.Modulus.congruenceSubgroup r) c

theorem

rationalCyclotomicLevelIsCyclotomicExtensionAtOrder

L215 ↗

KroneckerWeber.rationalCyclotomicLevelIsCyclotomicExtensionAtOrder

Source context 13 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩

Lean source · statement

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

instance

rationalCyclotomicFieldIsCyclotomicExtension

L228 ↗

KroneckerWeber.rationalCyclotomicFieldIsCyclotomicExtension

Source context 14 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩

Lean source · statement

instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ)

instance

rationalCyclotomicFieldIsAbelianGalois

L232 ↗

KroneckerWeber.rationalCyclotomicFieldIsAbelianGalois

Source context 15 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ

Lean source · statement

instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ)

instance

rationalCyclotomicLevelIdeleClassNormRangeNormal

L237 ↗

KroneckerWeber.rationalCyclotomicLevelIdeleClassNormRangeNormal

Source context 16 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)

Lean source · statement

instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal

instance

rationalCyclotomicFieldIdeleClassNormRangeNormal

L246 ↗

KroneckerWeber.rationalCyclotomicFieldIdeleClassNormRangeNormal

Source context 17 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal

def

rationalCyclotomicLevelAlgEquivCyclotomicField

L256 ↗

KroneckerWeber.rationalCyclotomicLevelAlgEquivCyclotomicField

Documentation

The internal finite level of the rational cyclotomic closure is isomorphic over ℚ to mathlib's concrete cyclotomic field of the same order.

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

def rationalCyclotomicLevelAlgEquivCyclotomicField
    :
    KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩ ≃ₐ[ℚ]
      CyclotomicField m ℚ

def

rationalPrimeArithmeticFrobeniusLocalInput

L270 ↗

KroneckerWeber.rationalPrimeArithmeticFrobeniusLocalInput

Documentation

A normalized local element of order one at the rational prime q. It is the inverse of the rational uniformizer in the absolute-value completion, transported to the adic-completion model used by idèles.

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

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

theorem

rationalPrimeArithmeticFrobeniusLocalInput_valuationMap

L279 ↗

KroneckerWeber.rationalPrimeArithmeticFrobeniusLocalInput_valuationMap

Documentation

The normalized local input for prime-ideal Artin reciprocity has inverse-standard valuation exponent one.

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

theorem rationalPrimeArithmeticFrobeniusLocalInput_valuationMap
    (q : Nat.Primes) :
    LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap
        (HeightOneSpectrum.adicAbv ℚ
          (RayClass.rationalPrime q)).Completion
        (Additive.ofMul
          ((finitePlaceCompletionUnitsContinuousMulEquiv
            (RayClass.rationalPrime q)).symm
            (rationalPrimeArithmeticFrobeniusLocalInput q))) =
      1

theorem

rationalCyclotomicLevel_chosenFinitePlaceArtin_at_unramifiedPrime

L297 ↗

KroneckerWeber.rationalCyclotomicLevel_chosenFinitePlaceArtin_at_unramifiedPrime

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

theorem
    rationalCyclotomicLevel_chosenFinitePlaceArtin_at_unramifiedPrime
    (m : ℕ) [NeZero m]
    (q : Nat.Primes) (hq : ¬ q.1 ∣ m) :
    IsCyclotomicExtension.Rat.galEquivZMod
        m
        (KummerTheory.rationalCyclotomicLevel
          ⟨m, NeZero.pos m⟩)
        (chosenFinitePlaceArtinMonoidHom
          (K := ℚ)
          (L := KummerTheory.rationalCyclotomicLevel
            ⟨m, NeZero.pos m⟩)
          (RayClass.rationalPrime q)
          (rationalPrimeArithmeticFrobeniusLocalInput q)) =
      ZMod.unitOfCoprime q.1
        (q.2.coprime_iff_not_dvd.mpr hq)

theorem

rationalCyclotomicLevel_globalNormResidue_at_unramifiedPrime

L346 ↗

KroneckerWeber.rationalCyclotomicLevel_globalNormResidue_at_unramifiedPrime

Documentation

At an unramified rational prime q ∤ m, the actual global norm-residue symbol on the normalized one-place prime idèle acts on the internal m-th cyclotomic level by the direct exponent q.

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

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

def

rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup

L407 ↗

KroneckerWeber.rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup

Documentation

Topological global reciprocity for the actual finite level inside the rational cyclotomic closure. The target is the idelic rational ray class group modulo (m), transported along the exact norm-range equality.

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

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

theorem

rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup_apply

L425 ↗

KroneckerWeber.rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup_apply

Documentation

Evaluation of finite-level rational cyclotomic reciprocity is inverse global norm-residue reciprocity followed by the exact ray norm-range transport.

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

theorem
    rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup_apply
    (σ : Gal(KummerTheory.rationalCyclotomicLevel ⟨m, NeZero.pos m⟩/ℚ)) :
    rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup
        m σ =
      QuotientGroup.quotientMulEquivOfEq
          (rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
            m (NeZero.ne m))
        (Additive.toMul
          ((globalNormResidueEquiv
              ℚ
              (KummerTheory.rationalCyclotomicLevel
                ⟨m, NeZero.pos m⟩)).symm
            (Additive.ofMul σ)))

theorem

rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup_globalNormResidue

L444 ↗

KroneckerWeber.rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup_globalNormResidue

Documentation

On an idèle-class representative, finite-level cyclotomic reciprocity is the actual global norm-residue symbol followed by its rational ray class modulo (m).

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

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

theorem

rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup_symm_mk

L463 ↗

KroneckerWeber.rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup_symm_mk

Documentation

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

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

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

theorem

rationalCyclotomicLevel_rayReciprocity_at_unramifiedPrime

L487 ↗

KroneckerWeber.rationalCyclotomicLevel_rayReciprocity_at_unramifiedPrime

Documentation

The inverse ray reciprocity image of the normalized one-place class at an unramified rational prime has direct cyclotomic exponent q. This places the actual global map, its ray quotient, and the Frobenius normalization on one literal finite cyclotomic field.

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

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

def

rationalCyclotomicPrimeArithmeticFrobenius

L512 ↗

KroneckerWeber.rationalCyclotomicPrimeArithmeticFrobenius

Documentation

The actual arithmetic Frobenius at q on the concrete cyclotomic field, obtained by transporting the genuine global one-place Artin symbol from the internal cyclotomic level.

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

def rationalCyclotomicPrimeArithmeticFrobenius
    (q : Nat.Primes) :
    Gal(CyclotomicField m ℚ / ℚ)

theorem

rationalCyclotomicPrimeArithmeticFrobenius_galEquivZMod

L535 ↗

KroneckerWeber.rationalCyclotomicPrimeArithmeticFrobenius_galEquivZMod

Documentation

For q ∤ m, the actual arithmetic Frobenius on CyclotomicField m ℚ is the direct-q automorphism ζ ↦ ζ ^ q; no inverse appears.

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

theorem rationalCyclotomicPrimeArithmeticFrobenius_galEquivZMod
    (q : Nat.Primes) (hq : ¬ q.1 ∣ m) :
    IsCyclotomicExtension.Rat.galEquivZMod
        m (CyclotomicField m ℚ)
        (rationalCyclotomicPrimeArithmeticFrobenius m q) =
      ZMod.unitOfCoprime q.1
        (q.2.coprime_iff_not_dvd.mpr hq)

def

rationalRayClassFieldCyclotomicRingEquiv

L575 ↗

KroneckerWeber.rationalRayClassFieldCyclotomicRingEquiv

Documentation

The selected rational ray class field is the actual cyclotomic field of the same modulus, as an equivalence of fields over ℚ.

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

def rationalRayClassFieldCyclotomicRingEquiv
    :
    rayClassField ℚ (RayClass.rationalModulus m) ≃+*
      CyclotomicField m ℚ

def

rationalRayClassFieldCyclotomicAlgEquiv

L593 ↗

KroneckerWeber.rationalRayClassFieldCyclotomicAlgEquiv

Documentation

A chosen ℚ-algebra equivalence from the selected rational ray class field to the cyclotomic field of the same modulus.

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

def rationalRayClassFieldCyclotomicAlgEquiv
    :
    rayClassField ℚ (RayClass.rationalModulus m) ≃ₐ[ℚ]
      CyclotomicField m ℚ

instance

rationalRayClassFieldIsCyclotomicExtension

L602 ↗

KroneckerWeber.rationalRayClassFieldIsCyclotomicExtension

Source context 18 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance

Lean source · statement

instance rationalRayClassFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (rayClassField ℚ (RayClass.rationalModulus m))

instance

rationalRayClassFieldIsAbelianGalois

L608 ↗

KroneckerWeber.rationalRayClassFieldIsAbelianGalois

Source context 19 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalRayClassFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.equiv {m} ℚ (CyclotomicField m ℚ)
    (rationalRayClassFieldCyclotomicAlgEquiv m).symm

Lean source · statement

instance rationalRayClassFieldIsAbelianGalois :
    IsAbelianGalois ℚ
      (rayClassField ℚ (RayClass.rationalModulus m))

theorem

rationalRayClassFieldCyclotomicAlgEquiv_autCongr_globalNormResidue_character

L618 ↗

KroneckerWeber.rationalRayClassFieldCyclotomicAlgEquiv_autCongr_globalNormResidue_character

Documentation

Transporting the actual norm-residue symbol of the selected rational ray class field to the concrete cyclotomic realization preserves its cyclotomic character. The left side uses the literal conjugation map on Galois automorphisms, not an abstract identification of finite groups.

Source context 20 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalRayClassFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.equiv {m} ℚ (CyclotomicField m ℚ)
    (rationalRayClassFieldCyclotomicAlgEquiv m).symm
noncomputable local instance rationalRayClassFieldIsAbelianGalois :
    IsAbelianGalois ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (rayClassField ℚ (RayClass.rationalModulus m))

Lean source · statement

theorem
    rationalRayClassFieldCyclotomicAlgEquiv_autCongr_globalNormResidue_character
    (c : IdeleClassGroup ℚ) :
    IsCyclotomicExtension.Rat.galEquivZMod
        m (CyclotomicField m ℚ)
        (AlgEquiv.autCongr
          (rationalRayClassFieldCyclotomicAlgEquiv m)
          (globalNormResidueMonoidHom
            ℚ (rayClassField ℚ (RayClass.rationalModulus m)) c)) =
      IsCyclotomicExtension.Rat.galEquivZMod
        m (rayClassField ℚ (RayClass.rationalModulus m))
        (globalNormResidueMonoidHom
          ℚ (rayClassField ℚ (RayClass.rationalModulus m)) c)

theorem

rationalRayClassFieldCyclotomicAlgEquiv_autCongr_globalNormResidue_character_hom

L640 ↗

KroneckerWeber.rationalRayClassFieldCyclotomicAlgEquiv_autCongr_globalNormResidue_character_hom

Documentation

Monoid-hom form of cyclotomic-character invariance under the selected ray-class-field/cyclotomic-field realization.

Source context 20 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalRayClassFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.equiv {m} ℚ (CyclotomicField m ℚ)
    (rationalRayClassFieldCyclotomicAlgEquiv m).symm
noncomputable local instance rationalRayClassFieldIsAbelianGalois :
    IsAbelianGalois ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (rayClassField ℚ (RayClass.rationalModulus m))

Lean source · statement

theorem
    rationalRayClassFieldCyclotomicAlgEquiv_autCongr_globalNormResidue_character_hom
    :
    ((IsCyclotomicExtension.Rat.galEquivZMod
        m (CyclotomicField m ℚ)).toMonoidHom.comp
      ((AlgEquiv.autCongr
        (rationalRayClassFieldCyclotomicAlgEquiv m)).toMonoidHom.comp
        (globalNormResidueMonoidHom
          ℚ (rayClassField ℚ (RayClass.rationalModulus m))))) =
      ((IsCyclotomicExtension.Rat.galEquivZMod
        m (rayClassField ℚ (RayClass.rationalModulus m))).toMonoidHom.comp
        (globalNormResidueMonoidHom
          ℚ (rayClassField ℚ (RayClass.rationalModulus m))))

def

rationalCyclotomicGaloisContinuousMulEquivRayClassGroup

L661 ↗

KroneckerWeber.rationalCyclotomicGaloisContinuousMulEquivRayClassGroup

Documentation

Topological global reciprocity for the actual rational cyclotomic field, with target the rational ray class group modulo (m).

Source context 20 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalRayClassFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.equiv {m} ℚ (CyclotomicField m ℚ)
    (rationalRayClassFieldCyclotomicAlgEquiv m).symm
noncomputable local instance rationalRayClassFieldIsAbelianGalois :
    IsAbelianGalois ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (rayClassField ℚ (RayClass.rationalModulus m))

Lean source · statement

def
    rationalCyclotomicGaloisContinuousMulEquivRayClassGroup
    :
    Gal(CyclotomicField m ℚ / ℚ) ≃ₜ*
      RayClass.RayClassGroup (RayClass.rationalModulus m)

def

rationalCyclotomicGaloisContinuousMulEquivZModUnits

L674 ↗

KroneckerWeber.rationalCyclotomicGaloisContinuousMulEquivZModUnits

Documentation

The ordinary cyclotomic character, retaining the finite Krull topology on the actual Galois group and the discrete topology on (ℤ/mℤ)ˣ.

Source context 20 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalRayClassFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.equiv {m} ℚ (CyclotomicField m ℚ)
    (rationalRayClassFieldCyclotomicAlgEquiv m).symm
noncomputable local instance rationalRayClassFieldIsAbelianGalois :
    IsAbelianGalois ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (rayClassField ℚ (RayClass.rationalModulus m))

Lean source · statement

def
    rationalCyclotomicGaloisContinuousMulEquivZModUnits
    :
    Gal(CyclotomicField m ℚ / ℚ) ≃ₜ*
      (ZMod m)ˣ

theorem

rationalCyclotomicGaloisContinuousMulEquivZModUnits_apply

L688 ↗

KroneckerWeber.rationalCyclotomicGaloisContinuousMulEquivZModUnits_apply

Documentation

Forgetting topology from the cyclotomic character recovers the standard galEquivZMod map literally.

Source context 20 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalRayClassFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.equiv {m} ℚ (CyclotomicField m ℚ)
    (rationalRayClassFieldCyclotomicAlgEquiv m).symm
noncomputable local instance rationalRayClassFieldIsAbelianGalois :
    IsAbelianGalois ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (rayClassField ℚ (RayClass.rationalModulus m))

Lean source · statement

theorem
    rationalCyclotomicGaloisContinuousMulEquivZModUnits_apply
    (σ : Gal(CyclotomicField m ℚ/ℚ)) :
    rationalCyclotomicGaloisContinuousMulEquivZModUnits
        m σ =
      IsCyclotomicExtension.Rat.galEquivZMod
        m (CyclotomicField m ℚ) σ

theorem

rationalCyclotomicGaloisContinuousMulEquivRayClassGroup_apply

L701 ↗

KroneckerWeber.rationalCyclotomicGaloisContinuousMulEquivRayClassGroup_apply

Documentation

Evaluation of rational cyclotomic reciprocity is inverse global norm-residue reciprocity followed by transport along the exact cyclotomic norm-range equality.

Source context 20 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalRayClassFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.equiv {m} ℚ (CyclotomicField m ℚ)
    (rationalRayClassFieldCyclotomicAlgEquiv m).symm
noncomputable local instance rationalRayClassFieldIsAbelianGalois :
    IsAbelianGalois ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (rayClassField ℚ (RayClass.rationalModulus m))

Lean source · statement

theorem
    rationalCyclotomicGaloisContinuousMulEquivRayClassGroup_apply
    (σ : Gal(CyclotomicField m ℚ/ℚ)) :
    rationalCyclotomicGaloisContinuousMulEquivRayClassGroup
        m σ =
      QuotientGroup.quotientMulEquivOfEq
          (rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
            m (NeZero.ne m))
        (Additive.toMul
          ((globalNormResidueEquiv
              ℚ (CyclotomicField m ℚ)).symm
            (Additive.ofMul σ)))

theorem

rationalCyclotomicGaloisContinuousMulEquivRayClassGroup_globalNormResidue

L718 ↗

KroneckerWeber.rationalCyclotomicGaloisContinuousMulEquivRayClassGroup_globalNormResidue

Documentation

On an idèle-class representative, rational cyclotomic reciprocity sends the actual global norm-residue symbol to its ray class modulo (m).

Source context 20 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
open NumberField IsDedekindDomain
noncomputable local instance rationalCyclotomicLevelIsAbelianGalois
    (n : ℕ+) :
    IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel n) :=
  IsCyclotomicExtension.isAbelianGalois {(n : ℕ)} ℚ
    (KummerTheory.rationalCyclotomicLevel n)
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 :
    IsAbelianGalois ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩) :=
  rationalCyclotomicLevelIsAbelianGalois
    ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicLevelIsCyclotomicExtensionAtOrder :
    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
      ⟨m, NeZero.pos m⟩
noncomputable local instance rationalCyclotomicFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ) :=
  CyclotomicField.isCyclotomicExtension m ℚ
noncomputable local instance rationalCyclotomicFieldIsAbelianGalois :
    IsAbelianGalois ℚ (CyclotomicField m ℚ) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (CyclotomicField m ℚ)
noncomputable local instance rationalCyclotomicLevelIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ
      (KummerTheory.rationalCyclotomicLevel
        ⟨m, NeZero.pos m⟩)).range.Normal := by
  rw [
    rationalCyclotomicLevel_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalCyclotomicFieldIdeleClassNormRangeNormal :
    (_root_.ideleClassNorm ℚ (CyclotomicField m ℚ)).range.Normal := by
  rw [
    rationalCyclotomicField_ideleClassNorm_range_eq_rationalCongruenceSubgroup
      m (NeZero.ne m)]
  infer_instance
noncomputable local instance rationalRayClassFieldIsCyclotomicExtension :
    IsCyclotomicExtension {m} ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.equiv {m} ℚ (CyclotomicField m ℚ)
    (rationalRayClassFieldCyclotomicAlgEquiv m).symm
noncomputable local instance rationalRayClassFieldIsAbelianGalois :
    IsAbelianGalois ℚ
      (rayClassField ℚ (RayClass.rationalModulus m)) :=
  IsCyclotomicExtension.isAbelianGalois {m} ℚ
    (rayClassField ℚ (RayClass.rationalModulus m))

Lean source · statement

theorem
    rationalCyclotomicGaloisContinuousMulEquivRayClassGroup_globalNormResidue
    (c : IdeleClassGroup ℚ) :
    rationalCyclotomicGaloisContinuousMulEquivRayClassGroup
        m
        (globalNormResidueMonoidHom
          ℚ (CyclotomicField m ℚ) c) =
      QuotientGroup.mk'
        (RayClass.Modulus.congruenceSubgroup
          (RayClass.rationalModulus m)) c

RationalRayClassFieldCyclotomic.lean

Module documentation

The rational ray class field as an actual cyclotomic field

rationalCyclotomicLevelIsAbelianGalois

galoisContinuousMulEquivRayClassGroupOfNormRangeEq

quotientMulEquivOfNormRangeEq_globalNormResidue

galoisContinuousMulEquivRayClassGroupOfNormRangeEq_globalNormResidue

galEquivZMod_autCongr

(anonymous instance)

(anonymous instance)

(anonymous instance)

rationalCyclotomicLevelIsCyclotomicExtensionAtOrder

rationalCyclotomicFieldIsCyclotomicExtension

rationalCyclotomicFieldIsAbelianGalois

rationalCyclotomicLevelIdeleClassNormRangeNormal

rationalCyclotomicFieldIdeleClassNormRangeNormal

rationalCyclotomicLevelAlgEquivCyclotomicField

rationalPrimeArithmeticFrobeniusLocalInput

rationalPrimeArithmeticFrobeniusLocalInput_valuationMap

rationalCyclotomicLevel_chosenFinitePlaceArtin_at_unramifiedPrime

rationalCyclotomicLevel_globalNormResidue_at_unramifiedPrime

rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup

rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup_apply

rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup_globalNormResidue

rationalCyclotomicLevelGaloisContinuousMulEquivRayClassGroup_symm_mk

rationalCyclotomicLevel_rayReciprocity_at_unramifiedPrime

rationalCyclotomicPrimeArithmeticFrobenius

rationalCyclotomicPrimeArithmeticFrobenius_galEquivZMod

rationalRayClassFieldCyclotomicRingEquiv

rationalRayClassFieldCyclotomicAlgEquiv

rationalRayClassFieldIsCyclotomicExtension

rationalRayClassFieldIsAbelianGalois

rationalRayClassFieldCyclotomicAlgEquiv_autCongr_globalNormResidue_character

rationalRayClassFieldCyclotomicAlgEquiv_autCongr_globalNormResidue_character_hom

rationalCyclotomicGaloisContinuousMulEquivRayClassGroup

rationalCyclotomicGaloisContinuousMulEquivZModUnits

rationalCyclotomicGaloisContinuousMulEquivZModUnits_apply

rationalCyclotomicGaloisContinuousMulEquivRayClassGroup_apply

rationalCyclotomicGaloisContinuousMulEquivRayClassGroup_globalNormResidue

Module documentation

The rational ray class field as an actual cyclotomic field

Declarations