Module

RayClassPrimeIdele.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayClassPrimeIdele

14 declarations indexed from sourceView source ↗

Module documentation

Prime idèles and ideal ray classes

A normalized one-place prime idèle is prime to every modulus whose finite support omits that prime. Its fractional ideal is the corresponding prime ideal, so the idelic and ideal-theoretic ray-class constructions use exactly the same prime representative.

Imports4

Imported by8

theorem

rayClassPrimeIdeleClassGroupIsMulCommutative

L34 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassPrimeIdeleClassGroupIsMulCommutative

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain IdeleGroup
universe u

Lean source · statement

theorem rayClassPrimeIdeleClassGroupIsMulCommutative
    (F : Type u) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

theorem

finitePrimeIdele_mem_idelePrimeToModulusSubgroup

L47 ↗

GlobalClassFieldTheory.GlobalClassFields.finitePrimeIdele_mem_idelePrimeToModulusSubgroup

Documentation

A normalized one-place prime idèle is prime to a modulus whenever the supporting prime does not occur in the modulus.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
section GenericPrimeIdele
variable {K : Type u} [Field K] [NumberField K]

Lean source · statement

theorem finitePrimeIdele_mem_idelePrimeToModulusSubgroup
    (m : RayClass.Modulus K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    finitePrimeIdele v ∈
      RayClass.idelePrimeToModulusSubgroup m

theorem

primeToIdealMap_finitePrimeIdele

L77 ↗

GlobalClassFieldTheory.GlobalClassFields.primeToIdealMap_finitePrimeIdele

Documentation

The fractional-ideal image of a normalized one-place prime idèle, viewed as prime to a modulus, is the corresponding prime-to-modulus prime ideal.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
section GenericPrimeIdele
variable {K : Type u} [Field K] [NumberField K]

Lean source · statement

theorem primeToIdealMap_finitePrimeIdele
    (m : RayClass.Modulus K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    RayClass.primeToIdealMap m
        ⟨finitePrimeIdele v,
          finitePrimeIdele_mem_idelePrimeToModulusSubgroup
            m v hv⟩ =
      RayClass.primeToModulusIdeal m v hv

theorem

idealRayProjection_finitePrimeIdele

L93 ↗

GlobalClassFieldTheory.GlobalClassFields.idealRayProjection_finitePrimeIdele

Documentation

The ideal-ray projection of a normalized one-place prime idèle is the ideal ray class of the corresponding prime ideal.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
section GenericPrimeIdele
variable {K : Type u} [Field K] [NumberField K]

Lean source · statement

theorem idealRayProjection_finitePrimeIdele
    (m : RayClass.Modulus K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    RayClass.idealRayProjection m
        ⟨finitePrimeIdele v,
          finitePrimeIdele_mem_idelePrimeToModulusSubgroup
            m v hv⟩ =
      QuotientGroup.mk'
        (RayClass.principalRayIdealSubgroup m)
        (RayClass.primeToModulusIdeal m v hv)

theorem

rayClassGroupEquivIdeleQuotient_mk_mk

L112 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassGroupEquivIdeleQuotient_mk_mk

Documentation

The idèle-class/full-idèle ray-class equivalence evaluates on a double quotient representative by forgetting the intermediate principal-idèle quotient.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
section GenericPrimeIdele
variable {K : Type u} [Field K] [NumberField K]

Lean source · statement

theorem rayClassGroupEquivIdeleQuotient_mk_mk
    (m : RayClass.Modulus K)
    (a : IdeleGroup K) :
    RayClass.rayClassGroupEquivIdeleQuotient m
        (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup m)
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup K) a)) =
      QuotientGroup.mk'
        (RayClass.Modulus.ideleCongruenceSubgroup m ⊔
          IdeleGroup.principalSubgroup K) a

theorem

rayClassGroupEquivIdealRayClassGroup_mk_primeTo

L134 ↗

GlobalClassFieldTheory.GlobalClassFields.rayClassGroupEquivIdealRayClassGroup_mk_primeTo

Documentation

The canonical idelic-to-ideal ray-class equivalence sends a prime-to-modulus idèle class to the ideal ray class of its fractional ideal.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
section GenericPrimeIdele
variable {K : Type u} [Field K] [NumberField K]

Lean source · statement

theorem rayClassGroupEquivIdealRayClassGroup_mk_primeTo
    (m : RayClass.Modulus K)
    (a : RayClass.idelePrimeToModulusSubgroup m) :
    RayClass.rayClassGroupEquivIdealRayClassGroup m
        (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup m)
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup K)
            (a : IdeleGroup K))) =
      RayClass.idealRayProjection m a

theorem

idealArtinMap_primeToIdealMap

L173 ↗

GlobalClassFieldTheory.GlobalClassFields.idealArtinMap_primeToIdealMap

Documentation

The ideal Artin map of the fractional ideal attached to a prime-to-modulus idèle is its direct class in the idèle-class quotient. This is the commuting square between the idelic and ideal-theoretic ray-class constructions.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem idealArtinMap_primeToIdealMap
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N)
    (a : RayClass.idelePrimeToModulusSubgroup m) :
    IdealClassFieldTheory.idealArtinMap m N hm
        (RayClass.primeToIdealMap m a) =
      QuotientGroup.mk' N
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K)
          (a : IdeleGroup K))

theorem

idealFrobeniusClass_eq_finitePrimeIdeleClass

L210 ↗

GlobalClassFieldTheory.GlobalClassFields.idealFrobeniusClass_eq_finitePrimeIdeleClass

Documentation

Outside a defining modulus, the ideal-theoretic Frobenius class is the quotient class of the normalized one-place prime idèle.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem idealFrobeniusClass_eq_finitePrimeIdeleClass
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    IdealClassFieldTheory.idealFrobeniusClass
        m N hm v hv =
      QuotientGroup.mk' N
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K)
          (finitePrimeIdele v))

theorem

bigHilbertIdealFrobeniusClass_eq_bigHilbertFrobeniusClass

L228 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertIdealFrobeniusClass_eq_bigHilbertFrobeniusClass

Documentation

The ideal Artin Frobenius class for the big Hilbert norm subgroup is the canonical big-Hilbert Frobenius class.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]

Lean source · full declaration

theorem bigHilbertIdealFrobeniusClass_eq_bigHilbertFrobeniusClass
    (v : HeightOneSpectrum (𝓞 K)) :
    IdealClassFieldTheory.idealFrobeniusClass
        (RayClass.Modulus.narrowOfFinite
          (0 : RayClass.FiniteModulus K))
        (bigHilbertClassFieldNormSubgroup (K := K))
        (bigHilbertClassFieldNormSubgroup_isDefiningModulus
          (K := K))
        v (by simp) =
      bigHilbertFrobeniusClass v := by
  have hm :
      (RayClass.Modulus.narrowOfFinite
        (0 : RayClass.FiniteModulus K)).congruenceSubgroup ≤
          bigHilbertClassFieldNormSubgroup (K := K) := by
    simpa only [IsDefiningModulus] using
      (bigHilbertClassFieldNormSubgroup_isDefiningModulus (K := K))
  rw [idealFrobeniusClass_eq_finitePrimeIdeleClass (hm := hm)]
  apply
    (bigHilbertClassFieldQuotientEquivNarrowClassGroup
      (K := K)).injective
  simpa only [bigHilbertFrobeniusClass, MulEquiv.apply_symm_apply] using
    (bigHilbertClassFieldQuotientEquivNarrowClassGroup_mk
      (K := K) (finitePrimeIdele v))

theorem

orderOf_bigHilbertIdealFrobeniusClass

L254 ↗

GlobalClassFieldTheory.GlobalClassFields.orderOf_bigHilbertIdealFrobeniusClass

Documentation

The order of the big-Hilbert ideal Artin Frobenius is the order of the corresponding narrow ideal class.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]

Lean source · full declaration

theorem orderOf_bigHilbertIdealFrobeniusClass
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf
        (IdealClassFieldTheory.idealFrobeniusClass
          (RayClass.Modulus.narrowOfFinite
            (0 : RayClass.FiniteModulus K))
          (bigHilbertClassFieldNormSubgroup (K := K))
          (bigHilbertClassFieldNormSubgroup_isDefiningModulus
            (K := K))
          v (by simp)) =
      orderOf
        (QuotientGroup.mk'
          (RayClass.narrowDenominator (K := K))
          (finitePrimeIdele v)) := by
  rw [bigHilbertIdealFrobeniusClass_eq_bigHilbertFrobeniusClass]
  exact
    (bigHilbertClassFieldQuotientEquivNarrowClassGroup
      (K := K)).symm.orderOf_eq
        (QuotientGroup.mk'
          (RayClass.narrowDenominator (K := K))
          (finitePrimeIdele v))

theorem

bigHilbertIdealFrobeniusClass_eq_one_iff_exists_totallyPositiveGenerator

L278 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertIdealFrobeniusClass_eq_one_iff_exists_totallyPositiveGenerator

Documentation

The big-Hilbert ideal Artin Frobenius is trivial exactly when its prime ideal has a totally positive generator.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]

Lean source · full declaration

theorem
    bigHilbertIdealFrobeniusClass_eq_one_iff_exists_totallyPositiveGenerator
    (v : HeightOneSpectrum (𝓞 K)) :
    IdealClassFieldTheory.idealFrobeniusClass
        (RayClass.Modulus.narrowOfFinite
          (0 : RayClass.FiniteModulus K))
        (bigHilbertClassFieldNormSubgroup (K := K))
        (bigHilbertClassFieldNormSubgroup_isDefiningModulus
          (K := K))
        v (by simp) =
        1 ↔
      ∃ x : Kˣ,
        IdeleGroup.principalIdele K x ∈
            RayClass.idelePrimeToModulusSubgroup
              (RayClass.Modulus.narrowOfFinite
                (0 : RayClass.FiniteModulus K)) ∧
          toPrincipalIdeal (𝓞 K) K x =
            FractionalIdealGroup.prime v := by
  rw [
    bigHilbertIdealFrobeniusClass_eq_bigHilbertFrobeniusClass,
    bigHilbertFrobeniusClass_eq_one_iff_exists_totallyPositiveGenerator]

theorem

smallHilbertIdealFrobeniusClass_eq_smallHilbertFrobeniusClass

L302 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertIdealFrobeniusClass_eq_smallHilbertFrobeniusClass

Documentation

The ideal Artin Frobenius class for the small Hilbert norm subgroup is the canonical small-Hilbert Frobenius class.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]

Lean source · full declaration

theorem smallHilbertIdealFrobeniusClass_eq_smallHilbertFrobeniusClass
    (v : HeightOneSpectrum (𝓞 K)) :
    IdealClassFieldTheory.idealFrobeniusClass
        (0 : RayClass.Modulus K)
        (smallHilbertClassFieldNormSubgroup (K := K))
        (smallHilbertClassFieldNormSubgroup_isDefiningModulus
          (K := K))
        v (by simp) =
      IdealClassFieldTheory.smallHilbertFrobeniusClass v := by
  have hm :
      (0 : RayClass.Modulus K).congruenceSubgroup ≤
        smallHilbertClassFieldNormSubgroup (K := K) := by
    simpa only [IsDefiningModulus] using
      (smallHilbertClassFieldNormSubgroup_isDefiningModulus (K := K))
  rw [idealFrobeniusClass_eq_finitePrimeIdeleClass (hm := hm)]
  apply
    (smallHilbertClassFieldQuotientEquivClassGroup
      (K := K)).injective
  simpa only [IdealClassFieldTheory.smallHilbertFrobeniusClass,
    MulEquiv.apply_symm_apply,
    smallHilbertClassFieldQuotientEquivClassGroup_mk] using
      IdeleGroup.idealClass_finitePrimeIdele v

theorem

orderOf_smallHilbertIdealFrobeniusClass

L327 ↗

GlobalClassFieldTheory.GlobalClassFields.orderOf_smallHilbertIdealFrobeniusClass

Documentation

The order of the small-Hilbert ideal Artin Frobenius is the order of the corresponding ordinary ideal class.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]

Lean source · full declaration

theorem orderOf_smallHilbertIdealFrobeniusClass
    (v : HeightOneSpectrum (𝓞 K)) :
    orderOf
        (IdealClassFieldTheory.idealFrobeniusClass
          (0 : RayClass.Modulus K)
          (smallHilbertClassFieldNormSubgroup (K := K))
          (smallHilbertClassFieldNormSubgroup_isDefiningModulus
            (K := K))
          v (by simp)) =
      orderOf
        (ClassGroup.mk K
          (FractionalIdealGroup.prime v)) := by
  rw [smallHilbertIdealFrobeniusClass_eq_smallHilbertFrobeniusClass]
  exact
    (smallHilbertClassFieldQuotientEquivClassGroup
      (K := K)).symm.orderOf_eq
        (ClassGroup.mk K
          (FractionalIdealGroup.prime v))

theorem

smallHilbertIdealFrobeniusClass_eq_one_iff_principal

L348 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertIdealFrobeniusClass_eq_one_iff_principal

Documentation

The small-Hilbert ideal Artin Frobenius is trivial exactly when its prime ideal is principal.

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
universe u
attribute [local instance] rayClassPrimeIdeleClassGroupIsMulCommutative
variable {K : Type} [Field K] [NumberField K]

Lean source · full declaration

theorem smallHilbertIdealFrobeniusClass_eq_one_iff_principal
    (v : HeightOneSpectrum (𝓞 K)) :
    IdealClassFieldTheory.idealFrobeniusClass
        (0 : RayClass.Modulus K)
        (smallHilbertClassFieldNormSubgroup (K := K))
        (smallHilbertClassFieldNormSubgroup_isDefiningModulus
          (K := K))
        v (by simp) =
        1 ↔
      FractionalIdealGroup.prime v ∈
        (toPrincipalIdeal (𝓞 K) K).range := by
  rw [smallHilbertIdealFrobeniusClass_eq_smallHilbertFrobeniusClass]
  exact
    IdealClassFieldTheory.splitsCompletelyInSmallHilbertClassField_iff_principal v

Module documentation

Prime idèles and ideal ray classes

Declarations