Module

RationalRayPrimeClass.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RationalRayPrimeClass

9 declarations indexed from sourceView source ↗

Module documentation

Rational prime classes in rational ray class groups

For a prime q away from a rational modulus (m), the normalized one-place prime idèle represents the direct residue unit q in (ZMod m)ˣ. This is the ideal-theoretic arithmetic input needed to compare rational ray reciprocity with the cyclotomic character.

Imports5

Imported by1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.All

def

rationalRayClassGroupContinuousMulEquivZModUnits

L36 ↗

GlobalClassFieldTheory.GlobalClassFields.rationalRayClassGroupContinuousMulEquivZModUnits

Documentation

The canonical rational ray-class identification, with the native quotient topology on the idèle-class quotient and the finite discrete topology on (ZMod m)ˣ. Thus this is the topological form of the rational ray-class computation, not only an abstract finite-group isomorphism.

Source context 5 commands

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

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

Lean source · statement

def rationalRayClassGroupContinuousMulEquivZModUnits
    (m : ℕ) (hm : m ≠ 0) :
    RayClass.RayClassGroup (RayClass.rationalModulus m) ≃ₜ*
      (ZMod m)ˣ

theorem

rationalRayClassGroupContinuousMulEquivZModUnits_apply

L55 ↗

GlobalClassFieldTheory.GlobalClassFields.rationalRayClassGroupContinuousMulEquivZModUnits_apply

Documentation

Forgetting topology from the canonical rational ray-class identification recovers the standard residue-class equivalence literally.

Source context 5 commands

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

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

Lean source · statement

theorem rationalRayClassGroupContinuousMulEquivZModUnits_apply
    (m : ℕ) (hm : m ≠ 0)
    (c : RayClass.RayClassGroup
      (RayClass.rationalModulus m)) :
    rationalRayClassGroupContinuousMulEquivZModUnits m hm c =
      RayClass.rationalRayClassGroupEquivZModUnits m hm c

theorem

rationalPrime_not_mem_rationalModulus_support

L65 ↗

GlobalClassFieldTheory.GlobalClassFields.rationalPrime_not_mem_rationalModulus_support

Documentation

A rational prime not dividing m is outside the finite support of the rational modulus (m).

Source context 5 commands

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

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

Lean source · statement

theorem rationalPrime_not_mem_rationalModulus_support
    (m : ℕ) (hm : m ≠ 0)
    (q : Nat.Primes) (hq : ¬ q.1 ∣ m) :
    RayClass.rationalPrime q ∉
      (RayClass.rationalModulus m).finitePart.support

theorem

rationalPrime_asIdeal_eq_span_integerGenerator

L82 ↗

GlobalClassFieldTheory.GlobalClassFields.rationalPrime_asIdeal_eq_span_integerGenerator

Documentation

The height-one prime of 𝓞 ℚ indexed by q is generated by the integer q, transported through the canonical equivalence 𝓞 ℚ ≃+* ℤ.

Source context 5 commands

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

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

Lean source · statement

theorem rationalPrime_asIdeal_eq_span_integerGenerator
    (q : Nat.Primes) :
    (RayClass.rationalPrime q).asIdeal =
      Ideal.span
        {Rat.ringOfIntegersEquiv.symm (q.1 : ℤ)}

theorem

rationalPrime_fractionalIdeal_eq_toPrincipalIdeal

L120 ↗

GlobalClassFieldTheory.GlobalClassFields.rationalPrime_fractionalIdeal_eq_toPrincipalIdeal

Documentation

The fractional prime ideal indexed by q is literally the principal fractional ideal generated by the positive rational integer q.

Source context 5 commands

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

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

Lean source · full declaration

theorem rationalPrime_fractionalIdeal_eq_toPrincipalIdeal
    (q : Nat.Primes) :
    FractionalIdealGroup.prime (RayClass.rationalPrime q) =
      toPrincipalIdeal (𝓞 ℚ) ℚ
        (Units.mk0 (q.1 : ℚ)
          (by exact_mod_cast q.2.ne_zero)) := by
  apply Units.ext
  rw [coe_toPrincipalIdeal]
  change
    ((RayClass.rationalPrime q).asIdeal :
        FractionalIdeal
          (nonZeroDivisors (𝓞 ℚ)) ℚ) =
      FractionalIdeal.spanSingleton
        (nonZeroDivisors (𝓞 ℚ)) (q.1 : ℚ)
  rw [rationalPrime_asIdeal_eq_span_integerGenerator,
    FractionalIdeal.coeIdeal_span_singleton]
  congr 1
  exact Rat.ringOfIntegersEquiv_symm_apply_coe (q.1 : ℤ)

def

rationalPrimePrincipalPrimeToModulusIdeal

L141 ↗

GlobalClassFieldTheory.GlobalClassFields.rationalPrimePrincipalPrimeToModulusIdeal

Documentation

The rational prime ideal, regarded as prime to (m), written using its positive principal generator q.

Source context 5 commands

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

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

Lean source · statement

def rationalPrimePrincipalPrimeToModulusIdeal
    (m : ℕ) (hm : m ≠ 0)
    (q : Nat.Primes) (hq : ¬ q.1 ∣ m) :
    RayClass.primeToModulusIdeals
      (RayClass.rationalModulus m)

theorem

primeToModulusIdeal_rationalPrime_eq_principal

L155 ↗

GlobalClassFieldTheory.GlobalClassFields.primeToModulusIdeal_rationalPrime_eq_principal

Documentation

The canonical prime-to-modulus ideal at q agrees with the principal ideal represented by the positive integer q.

Source context 5 commands

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

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

Lean source · statement

theorem primeToModulusIdeal_rationalPrime_eq_principal
    (m : ℕ) (hm : m ≠ 0)
    (q : Nat.Primes) (hq : ¬ q.1 ∣ m) :
    RayClass.primeToModulusIdeal
        (RayClass.rationalModulus m)
        (RayClass.rationalPrime q)
        (rationalPrime_not_mem_rationalModulus_support
          m hm q hq) =
      rationalPrimePrincipalPrimeToModulusIdeal
        m hm q hq

theorem

primeToIdealResidueHom_rationalPrime

L171 ↗

GlobalClassFieldTheory.GlobalClassFields.primeToIdealResidueHom_rationalPrime

Documentation

The ideal residue homomorphism sends the rational prime ideal at q ∤ m to the direct residue unit q.

Source context 5 commands

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

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

Lean source · statement

theorem primeToIdealResidueHom_rationalPrime
    (m : ℕ) (hm : m ≠ 0)
    (q : Nat.Primes) (hq : ¬ q.1 ∣ m) :
    RayClass.primeToIdealResidueHom m hm
        (RayClass.primeToModulusIdeal
          (RayClass.rationalModulus m)
          (RayClass.rationalPrime q)
          (rationalPrime_not_mem_rationalModulus_support
            m hm q hq)) =
      ZMod.unitOfCoprime q.1
        (q.2.coprime_iff_not_dvd.mpr hq)

theorem

rationalRayClassGroupEquivZModUnits_finitePrimeIdeleClass

L226 ↗

GlobalClassFieldTheory.GlobalClassFields.rationalRayClassGroupEquivZModUnits_finitePrimeIdeleClass

Documentation

The canonical normalized finite prime idèle class at q ∤ m has direct residue q under the rational ray-class equivalence with (ZMod m)ˣ.

Source context 5 commands

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

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

Lean source · statement

theorem rationalRayClassGroupEquivZModUnits_finitePrimeIdeleClass
    (m : ℕ) (hm : m ≠ 0)
    (q : Nat.Primes) (hq : ¬ q.1 ∣ m) :
    RayClass.rationalRayClassGroupEquivZModUnits m hm
        (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup
            (RayClass.rationalModulus m))
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup ℚ)
            (finitePrimeIdele
              (RayClass.rationalPrime q)))) =
      ZMod.unitOfCoprime q.1
        (q.2.coprime_iff_not_dvd.mpr hq)

Module documentation

Rational prime classes in rational ray class groups

Declarations