Module

ConductorPrimeArtin.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ConductorPrimeArtin

11 declarations indexed from sourceView source ↗

Module documentation

Prime Artin classes at an exact narrow finite conductor

For a conductorial idèle-class subgroup H, a normalized one-place prime idèle determines compatible classes in the ray class group at H.narrowFiniteConductor, in C_K / H, and—away from that finite conductor—in the ideal Artin quotient. This file proves their compatibility, order relations, and maximal ray-class criteria.

Imports3

Imported by1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.All

def

subgroupQuotientPrimeClass

L39 ↗

GlobalClassFieldTheory.GlobalClassFields.subgroupQuotientPrimeClass

Documentation

The class of a normalized one-place prime idèle in an arbitrary idèle-class 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 : Type} [Field K] [NumberField K]

-- Keep quotient witnesses definitionally aligned with the imported
-- ideal-Artin construction and avoid repeating generic normality search.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal

Lean source · statement

def subgroupQuotientPrimeClass
    (H : Subgroup (IdeleClassGroup K))
    (v : HeightOneSpectrum (𝓞 K)) :
    IdeleClassGroup K ⧸ H

def

narrowFiniteConductorRayPrimeClass

L52 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayPrimeClass

Documentation

The ray class of a normalized one-place prime idèle at the exact narrow finite conductor of H.

Source context 8 commands

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

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

-- Keep quotient witnesses definitionally aligned with the imported
-- ideal-Artin construction and avoid repeating generic normality search.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
namespace ConductorialSubgroup

Lean source · statement

def narrowFiniteConductorRayPrimeClass
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    RayClass.RayClassGroup
      (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)

theorem

narrowFiniteConductorRayClassGroupToQuotient_rayPrimeClass

L67 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayClassGroupToQuotient_rayPrimeClass

Documentation

The exact narrow finite conductor ray-class map sends the ray prime class to the corresponding class in C_K / H.

Source context 8 commands

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

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

-- Keep quotient witnesses definitionally aligned with the imported
-- ideal-Artin construction and avoid repeating generic normality search.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
namespace ConductorialSubgroup

Lean source · statement

theorem narrowFiniteConductorRayClassGroupToQuotient_rayPrimeClass
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    H.narrowFiniteConductorRayClassGroupToQuotient
        (H.narrowFiniteConductorRayPrimeClass v) =
      subgroupQuotientPrimeClass H.1 v

theorem

narrowFiniteConductorRayClassGroupEquivQuotientOfCardEq_rayPrimeClass

L79 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayClassGroupEquivQuotientOfCardEq_rayPrimeClass

Documentation

Under maximal exact narrow finite conductor cardinality, the canonical ray-class equivalence sends the ray prime class to its class in C_K / H.

Source context 8 commands

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

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

-- Keep quotient witnesses definitionally aligned with the imported
-- ideal-Artin construction and avoid repeating generic normality search.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
namespace ConductorialSubgroup

Lean source · statement

theorem narrowFiniteConductorRayClassGroupEquivQuotientOfCardEq_rayPrimeClass
    (H : ConductorialSubgroup K)
    (hcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ H.1))
    (v : HeightOneSpectrum (𝓞 K)) :
    H.narrowFiniteConductorRayClassGroupEquivQuotientOfCardEq
        hcard
        (H.narrowFiniteConductorRayPrimeClass v) =
      subgroupQuotientPrimeClass H.1 v

theorem

narrowFiniteConductorIdealFrobeniusClass_eq_quotientPrimeClass

L94 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorIdealFrobeniusClass_eq_quotientPrimeClass

Documentation

Away from the exact narrow finite conductor of H, the ideal Artin Frobenius class equals the normalized prime idèle class in C_K / H.

Source context 8 commands

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

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

-- Keep quotient witnesses definitionally aligned with the imported
-- ideal-Artin construction and avoid repeating generic normality search.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
namespace ConductorialSubgroup

Lean source · statement

theorem narrowFiniteConductorIdealFrobeniusClass_eq_quotientPrimeClass
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ H.narrowFiniteConductor.support) :
    IdealClassFieldTheory.idealFrobeniusClass
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor) H.1
        H.narrowFiniteConductor_isDefiningModulus
        v hv =
      subgroupQuotientPrimeClass H.1 v

theorem

subgroupQuotientPrimeClass_eq_one_iff_primeIdeal_mem_idealArtinKernel

L147 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.subgroupQuotientPrimeClass_eq_one_iff_primeIdeal_mem_idealArtinKernel

Documentation

Triviality of the prime class in C_K / H is equivalent to membership of its prime ideal in the ideal Artin kernel.

Source context 8 commands

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

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

-- Keep quotient witnesses definitionally aligned with the imported
-- ideal-Artin construction and avoid repeating generic normality search.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
namespace ConductorialSubgroup

Lean source · statement

theorem subgroupQuotientPrimeClass_eq_one_iff_primeIdeal_mem_idealArtinKernel
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ H.narrowFiniteConductor.support) :
    subgroupQuotientPrimeClass H.1 v = 1 ↔
      RayClass.primeToModulusIdeal
          (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)
          v hv ∈
        IdealClassFieldTheory.idealArtinKernel
          (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor) H.1
          H.narrowFiniteConductor_isDefiningModulus

theorem

orderOf_subgroupQuotientPrimeClass_eq_orderOf_idealArtinPrimeClass

L163 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.orderOf_subgroupQuotientPrimeClass_eq_orderOf_idealArtinPrimeClass

Documentation

The order of the prime class in C_K / H is the order of its prime ideal modulo the ideal Artin kernel.

Source context 8 commands

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

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

-- Keep quotient witnesses definitionally aligned with the imported
-- ideal-Artin construction and avoid repeating generic normality search.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
namespace ConductorialSubgroup

Lean source · statement

theorem orderOf_subgroupQuotientPrimeClass_eq_orderOf_idealArtinPrimeClass
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ H.narrowFiniteConductor.support) :
    orderOf (subgroupQuotientPrimeClass H.1 v) =
      orderOf
        (QuotientGroup.mk'
          (IdealClassFieldTheory.idealArtinKernel
            (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor) H.1
            H.narrowFiniteConductor_isDefiningModulus)
          (RayClass.primeToModulusIdeal
            (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)
            v hv))

theorem

orderOf_subgroupQuotientPrimeClass_dvd_orderOf_narrowFiniteConductorRayPrimeClass

L185 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.orderOf_subgroupQuotientPrimeClass_dvd_orderOf_narrowFiniteConductorRayPrimeClass

Documentation

The order of the prime class in C_K / H divides the order of its lift to the exact narrow finite conductor ray class group.

Source context 8 commands

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

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

-- Keep quotient witnesses definitionally aligned with the imported
-- ideal-Artin construction and avoid repeating generic normality search.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
namespace ConductorialSubgroup

Lean source · statement

theorem orderOf_subgroupQuotientPrimeClass_dvd_orderOf_narrowFiniteConductorRayPrimeClass
    (H : ConductorialSubgroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf (subgroupQuotientPrimeClass H.1 v) ∣
      orderOf (H.narrowFiniteConductorRayPrimeClass v)

theorem

narrowFiniteConductorRayPrimeClass_eq_one_iff_quotientPrimeClass_eq_one

L198 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayPrimeClass_eq_one_iff_quotientPrimeClass_eq_one

Documentation

Under maximal exact narrow finite conductor ray-class cardinality, triviality of the ray prime class is equivalent to triviality of its class in C_K / H.

Source context 8 commands

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

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

-- Keep quotient witnesses definitionally aligned with the imported
-- ideal-Artin construction and avoid repeating generic normality search.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
namespace ConductorialSubgroup

Lean source · statement

theorem narrowFiniteConductorRayPrimeClass_eq_one_iff_quotientPrimeClass_eq_one
    (H : ConductorialSubgroup K)
    (hcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ H.1))
    (v : HeightOneSpectrum (𝓞 K)) :
    H.narrowFiniteConductorRayPrimeClass v = 1 ↔
      subgroupQuotientPrimeClass H.1 v = 1

theorem

orderOf_narrowFiniteConductorRayPrimeClass_eq_orderOf_quotientPrimeClass

L226 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.orderOf_narrowFiniteConductorRayPrimeClass_eq_orderOf_quotientPrimeClass

Documentation

Under maximal exact narrow finite conductor ray-class cardinality, the ray prime class and its image in C_K / H have the same order.

Source context 8 commands

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

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

-- Keep quotient witnesses definitionally aligned with the imported
-- ideal-Artin construction and avoid repeating generic normality search.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
namespace ConductorialSubgroup

Lean source · statement

theorem orderOf_narrowFiniteConductorRayPrimeClass_eq_orderOf_quotientPrimeClass
    (H : ConductorialSubgroup K)
    (hcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ H.1))
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf (H.narrowFiniteConductorRayPrimeClass v) =
      orderOf (subgroupQuotientPrimeClass H.1 v)

theorem

narrowFiniteConductorRayPrimeClass_eq_one_iff_primeIdeal_mem_idealArtinKernel

L248 ↗

GlobalClassFieldTheory.GlobalClassFields.ConductorialSubgroup.narrowFiniteConductorRayPrimeClass_eq_one_iff_primeIdeal_mem_idealArtinKernel

Documentation

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

Source context 8 commands

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

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

-- Keep quotient witnesses definitionally aligned with the imported
-- ideal-Artin construction and avoid repeating generic normality search.
attribute [local instance]
  IdealClassFieldTheory.ideleClassSubgroupNormal
namespace ConductorialSubgroup

Lean source · statement

theorem narrowFiniteConductorRayPrimeClass_eq_one_iff_primeIdeal_mem_idealArtinKernel
    (H : ConductorialSubgroup K)
    (hcard :
      Nat.card (RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)) =
        Nat.card (IdeleClassGroup K ⧸ H.1))
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ H.narrowFiniteConductor.support) :
    H.narrowFiniteConductorRayPrimeClass v = 1 ↔
      RayClass.primeToModulusIdeal
          (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor)
          v hv ∈
        IdealClassFieldTheory.idealArtinKernel
          (RayClass.Modulus.narrowOfFinite H.narrowFiniteConductor) H.1
          H.narrowFiniteConductor_isDefiningModulus

Module documentation

Prime Artin classes at an exact narrow finite conductor

Declarations