Module

ConductorFrobenius.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorFrobenius

19 declarations indexed from sourceView source ↗

Module documentation

Prime classes at the narrow finite norm conductor

The one-place idèle of normalized order one defines two compatible prime classes: one in the ray class group at the exact narrow finite norm conductor, and one in the actual idele-class norm quotient. The canonical narrow-finite-conductor ray-class map sends the former to the latter.

For cyclic extensions the order of the norm-quotient class divides the extension degree. Complete splitting forces this class to be trivial; when the narrow-finite-conductor ray-class presentation is maximal, it also forces the narrow finite conductor ray prime class itself to be trivial.

Imports4

Imported by3

def

narrowFiniteConductorRayPrimeClass

L51 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayPrimeClass

Documentation

The class of the normalized one-place prime idèle in the ray class group at the exact narrow finite conductor of the actual norm subgroup.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

def narrowFiniteConductorRayPrimeClass
    (v : HeightOneSpectrum (𝓞 K)) :
    RayClass.RayClassGroup
      (RayClass.Modulus.narrowOfFinite
        (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))

def

ideleClassNormFrobeniusClass

L66 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormFrobeniusClass

Documentation

The class of the normalized one-place prime idèle in the actual idele-class norm quotient.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

def ideleClassNormFrobeniusClass
    (v : HeightOneSpectrum (𝓞 K)) :
    IdeleClassGroup K ⧸
      (_root_.ideleClassNorm K L).range

theorem

narrowFiniteConductorIdealFrobeniusClass_eq_ideleClassNormFrobeniusClass

L79 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorIdealFrobeniusClass_eq_ideleClassNormFrobeniusClass

Documentation

At a prime outside the exact narrow finite norm conductor, the ideal-theoretic Frobenius class agrees with the class of the normalized one-place idèle in the actual norm quotient.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
    narrowFiniteConductorIdealFrobeniusClass_eq_ideleClassNormFrobeniusClass
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∉
        (ideleClassNormNarrowFiniteConductor (K := K) (L := L)).support) :
    IdealClassFieldTheory.idealFrobeniusClass
        (RayClass.Modulus.narrowOfFinite
          (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
        ((_root_.ideleClassNorm K L).range)
        (ideleClassNorm_narrowFiniteConductor_isDefiningModulus
          (K := K) (L := L))
        v hv =
      ideleClassNormFrobeniusClass
        (K := K) (L := L) v

theorem

orderOf_ideleClassNormFrobeniusClass_eq_orderOf_idealArtinPrimeClass

L139 ↗

GlobalClassFieldTheory.GlobalClassFields.orderOf_ideleClassNormFrobeniusClass_eq_orderOf_idealArtinPrimeClass

Documentation

The order of a Frobenius class in the actual norm quotient is the order of its prime ideal modulo the ideal Artin kernel at the exact narrow finite norm conductor.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
    orderOf_ideleClassNormFrobeniusClass_eq_orderOf_idealArtinPrimeClass
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∉
        (ideleClassNormNarrowFiniteConductor (K := K) (L := L)).support) :
    orderOf
        (ideleClassNormFrobeniusClass
          (K := K) (L := L) v) =
      orderOf
        (QuotientGroup.mk'
          (IdealClassFieldTheory.idealArtinKernel
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
            ((_root_.ideleClassNorm K L).range)
            (ideleClassNorm_narrowFiniteConductor_isDefiningModulus
              (K := K) (L := L)))
          (RayClass.primeToModulusIdeal
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
            v hv))

theorem

ideleClassNormFrobeniusClass_eq_one_iff_narrowFiniteConductorPrimeIdeal_mem_idealArtinKernel

L175 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormFrobeniusClass_eq_one_iff_narrowFiniteConductorPrimeIdeal_mem_idealArtinKernel

Documentation

Triviality of the actual norm-quotient Frobenius class is equivalent to membership of the corresponding prime ideal in the ideal Artin kernel at the exact narrow finite conductor.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
    ideleClassNormFrobeniusClass_eq_one_iff_narrowFiniteConductorPrimeIdeal_mem_idealArtinKernel
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∉
        (ideleClassNormNarrowFiniteConductor (K := K) (L := L)).support) :
    ideleClassNormFrobeniusClass
          (K := K) (L := L) v =
        1 ↔
      RayClass.primeToModulusIdeal
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
          v hv ∈
        IdealClassFieldTheory.idealArtinKernel
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
          ((_root_.ideleClassNorm K L).range)
          (ideleClassNorm_narrowFiniteConductor_isDefiningModulus
            (K := K) (L := L))

theorem

narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_rayPrimeClass

L203 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_rayPrimeClass

Documentation

The canonical narrow-finite-conductor ray-class map sends the narrow finite conductor ray prime class to the corresponding actual norm-quotient Frobenius class.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
    narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient_rayPrimeClass
    (v : HeightOneSpectrum (𝓞 K)) :
    narrowFiniteConductorRayClassGroupToIdeleClassNormQuotient
        (K := K) (L := L)
        (narrowFiniteConductorRayPrimeClass
          (K := K) (L := L) v) =
      ideleClassNormFrobeniusClass
        (K := K) (L := L) v

theorem

orderOf_ideleClassNormFrobeniusClass_dvd_orderOf_narrowFiniteConductorRayPrimeClass

L216 ↗

GlobalClassFieldTheory.GlobalClassFields.orderOf_ideleClassNormFrobeniusClass_dvd_orderOf_narrowFiniteConductorRayPrimeClass

Documentation

The order of the actual norm-quotient Frobenius class divides the order of its lift to the exact narrow-finite-conductor ray class group.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
    orderOf_ideleClassNormFrobeniusClass_dvd_orderOf_narrowFiniteConductorRayPrimeClass
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf
        (ideleClassNormFrobeniusClass
          (K := K) (L := L) v) ∣
      orderOf
        (narrowFiniteConductorRayPrimeClass
          (K := K) (L := L) v)

theorem

narrowFiniteConductorRayPrimeClass_eq_one_iff_ideleClassNormFrobeniusClass_eq_one

L238 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayPrimeClass_eq_one_iff_ideleClassNormFrobeniusClass_eq_one

Documentation

Equal source and target orders make triviality of the narrow finite conductor ray prime class equivalent to triviality of its actual norm-quotient Frobenius class.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
    narrowFiniteConductorRayPrimeClass_eq_one_iff_ideleClassNormFrobeniusClass_eq_one
    (hcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range))
    (v : HeightOneSpectrum (𝓞 K)) :
    narrowFiniteConductorRayPrimeClass
        (K := K) (L := L) v = 1 ↔
      ideleClassNormFrobeniusClass
        (K := K) (L := L) v = 1

theorem

orderOf_narrowFiniteConductorRayPrimeClass_eq_orderOf_ideleClassNormFrobeniusClass

L281 ↗

GlobalClassFieldTheory.GlobalClassFields.orderOf_narrowFiniteConductorRayPrimeClass_eq_orderOf_ideleClassNormFrobeniusClass

Documentation

Equal source and target orders make the narrow finite conductor ray prime class and its actual norm-quotient image have the same order.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
    orderOf_narrowFiniteConductorRayPrimeClass_eq_orderOf_ideleClassNormFrobeniusClass
    (hcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range))
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf
        (narrowFiniteConductorRayPrimeClass
          (K := K) (L := L) v) =
      orderOf
        (ideleClassNormFrobeniusClass
          (K := K) (L := L) v)

theorem

narrowFiniteConductorRayPrimeClass_eq_one_iff_narrowFiniteConductorPrimeIdeal_mem_idealArtinKernel

L317 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayPrimeClass_eq_one_iff_narrowFiniteConductorPrimeIdeal_mem_idealArtinKernel

Documentation

When the exact narrow-finite-conductor ray presentation has the same order as the actual norm quotient, triviality of its ray prime class is equivalent to membership of the prime ideal in the ideal Artin kernel.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
  narrowFiniteConductorRayPrimeClass_eq_one_iff_narrowFiniteConductorPrimeIdeal_mem_idealArtinKernel
    (hcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range))
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∉
        (ideleClassNormNarrowFiniteConductor (K := K) (L := L)).support) :
    narrowFiniteConductorRayPrimeClass
          (K := K) (L := L) v =
        1 ↔
      RayClass.primeToModulusIdeal
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
          v hv ∈
        IdealClassFieldTheory.idealArtinKernel
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
          ((_root_.ideleClassNorm K L).range)
          (ideleClassNorm_narrowFiniteConductor_isDefiningModulus
            (K := K) (L := L))

theorem

finitePlaceSplitsCompletely_imp_ideleClassNormFrobeniusClass_eq_one

L352 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePlaceSplitsCompletely_imp_ideleClassNormFrobeniusClass_eq_one

Documentation

Complete splitting at a finite place forces the corresponding actual norm-quotient Frobenius class to be trivial.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
    finitePlaceSplitsCompletely_imp_ideleClassNormFrobeniusClass_eq_one
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    ideleClassNormFrobeniusClass
        (K := K) (L := L) v = 1

theorem

finitePlaceSplitsCompletely_imp_narrowFiniteConductorIdealFrobeniusClass_eq_one

L373 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePlaceSplitsCompletely_imp_narrowFiniteConductorIdealFrobeniusClass_eq_one

Documentation

Complete splitting at a finite place makes its ideal Frobenius class at the exact narrow finite norm conductor trivial.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
    finitePlaceSplitsCompletely_imp_narrowFiniteConductorIdealFrobeniusClass_eq_one
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    IdealClassFieldTheory.idealFrobeniusClass
        (RayClass.Modulus.narrowOfFinite
          (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
        ((_root_.ideleClassNorm K L).range)
        (ideleClassNorm_narrowFiniteConductor_isDefiningModulus
          (K := K) (L := L))
        v
        (not_mem_ideleClassNorm_narrowFiniteConductor_support_of_splitsCompletely
          (K := K) (L := L) v hsplit) =
      1

theorem

finitePlaceSplitsCompletely_imp_narrowFiniteConductorPrimeIdeal_mem_idealArtinKernel

L396 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePlaceSplitsCompletely_imp_narrowFiniteConductorPrimeIdeal_mem_idealArtinKernel

Documentation

A finite prime which splits completely belongs to the ideal Artin kernel at the exact narrow finite norm conductor.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
    finitePlaceSplitsCompletely_imp_narrowFiniteConductorPrimeIdeal_mem_idealArtinKernel
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    RayClass.primeToModulusIdeal
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
          v
          (not_mem_ideleClassNorm_narrowFiniteConductor_support_of_splitsCompletely
            (K := K) (L := L) v hsplit) ∈
        IdealClassFieldTheory.idealArtinKernel
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
          ((_root_.ideleClassNorm K L).range)
          (ideleClassNorm_narrowFiniteConductor_isDefiningModulus
            (K := K) (L := L))

theorem

orderOf_ideleClassNormFrobeniusClass_dvd_extensionDegree

L429 ↗

GlobalClassFieldTheory.GlobalClassFields.orderOf_ideleClassNormFrobeniusClass_dvd_extensionDegree

Documentation

For a finite cyclic extension, the order of every actual norm-quotient Frobenius class divides the extension degree.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
section Cyclic
variable [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem orderOf_ideleClassNormFrobeniusClass_dvd_extensionDegree
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf
        (ideleClassNormFrobeniusClass
          (K := K) (L := L) v) ∣
      Module.finrank K L

theorem

orderOf_narrowFiniteConductorIdealFrobeniusClass_dvd_extensionDegree

L444 ↗

GlobalClassFieldTheory.GlobalClassFields.orderOf_narrowFiniteConductorIdealFrobeniusClass_dvd_extensionDegree

Documentation

For a finite cyclic extension, the order of every ideal Frobenius class outside the exact narrow finite norm conductor divides the extension degree.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
section Cyclic
variable [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem
    orderOf_narrowFiniteConductorIdealFrobeniusClass_dvd_extensionDegree
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∉
        (ideleClassNormNarrowFiniteConductor (K := K) (L := L)).support) :
    orderOf
        (IdealClassFieldTheory.idealFrobeniusClass
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
          ((_root_.ideleClassNorm K L).range)
          (ideleClassNorm_narrowFiniteConductor_isDefiningModulus
            (K := K) (L := L))
          v hv) ∣
      Module.finrank K L

theorem

orderOf_narrowFiniteConductorPrimeIdealArtinClass_dvd_extensionDegree

L468 ↗

GlobalClassFieldTheory.GlobalClassFields.orderOf_narrowFiniteConductorPrimeIdealArtinClass_dvd_extensionDegree

Documentation

For a finite cyclic extension, the order of the prime ideal class modulo the ideal Artin kernel at the exact narrow finite conductor divides the extension degree.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
section Cyclic
variable [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem
    orderOf_narrowFiniteConductorPrimeIdealArtinClass_dvd_extensionDegree
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∉
        (ideleClassNormNarrowFiniteConductor (K := K) (L := L)).support) :
    orderOf
        (QuotientGroup.mk'
          (IdealClassFieldTheory.idealArtinKernel
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
            ((_root_.ideleClassNorm K L).range)
            (ideleClassNorm_narrowFiniteConductor_isDefiningModulus
              (K := K) (L := L)))
          (RayClass.primeToModulusIdeal
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
            v hv)) ∣
      Module.finrank K L

theorem

narrowRayPrimeClass_eq_one_iff_primeIdeal_mem_artinKernel_of_card_eq_degree

L497 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowRayPrimeClass_eq_one_iff_primeIdeal_mem_artinKernel_of_card_eq_degree

Documentation

At maximal cyclic ray-class cardinality, triviality of the exact narrow finite conductor ray prime class is equivalent to membership of the prime ideal in the ideal Artin kernel.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
section Cyclic
variable [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem
    narrowRayPrimeClass_eq_one_iff_primeIdeal_mem_artinKernel_of_card_eq_degree
    (hcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Module.finrank K L)
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∉
        (ideleClassNormNarrowFiniteConductor (K := K) (L := L)).support) :
    narrowFiniteConductorRayPrimeClass
          (K := K) (L := L) v =
        1 ↔
      RayClass.primeToModulusIdeal
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
          v hv ∈
        IdealClassFieldTheory.idealArtinKernel
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))
          ((_root_.ideleClassNorm K L).range)
          (ideleClassNorm_narrowFiniteConductor_isDefiningModulus
            (K := K) (L := L))

theorem

finitePlaceSplitsCompletely_imp_narrowFiniteConductorRayPrimeClass_eq_one_of_card_eq_extensionDegree

L539 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePlaceSplitsCompletely_imp_narrowFiniteConductorRayPrimeClass_eq_one_of_card_eq_extensionDegree

Documentation

If a cyclic extension reaches the full ray class number at its exact narrow finite conductor, complete splitting forces the corresponding ray prime class to be trivial.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
section Cyclic
variable [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem
finitePlaceSplitsCompletely_imp_narrowFiniteConductorRayPrimeClass_eq_one_of_card_eq_extensionDegree
    (hcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Module.finrank K L)
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      _root_.FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    narrowFiniteConductorRayPrimeClass
        (K := K) (L := L) v = 1

theorem

orderOf_narrowFiniteConductorRayPrimeClass_dvd_extensionDegree_of_card_eq

L572 ↗

GlobalClassFieldTheory.GlobalClassFields.orderOf_narrowFiniteConductorRayPrimeClass_dvd_extensionDegree_of_card_eq

Documentation

Under the maximal narrow-finite-conductor ray-class cardinality condition, the order of every corresponding ray prime class divides the extension degree.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

-- Reuse the normality witness embedded in the imported ideal-Artin maps.
-- Without it, every occurrence of the norm quotient repeats an expensive
-- unsuccessful instance search and builds a non-definitional witness.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

theorem
    orderOf_narrowFiniteConductorRayPrimeClass_dvd_extensionDegree_of_card_eq
    (hcard :
      Nat.card
          (RayClass.RayClassGroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor (K := K) (L := L)))) =
        Module.finrank K L)
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf
        (narrowFiniteConductorRayPrimeClass
          (K := K) (L := L) v) ∣
      Module.finrank K L

Module documentation

Prime classes at the narrow finite norm conductor

Declarations