Module

IdealFrobenius.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.IdealFrobenius

3 declarations indexed from sourceView source ↗

Module documentation

Ideal Frobenius classes and the decomposition law

This file records the ideal-class-field ingredient of the decomposition law. A prime outside a defining modulus gives an element of the ideal Artin quotient, and the first isomorphism theorem preserves its order. The general unramified Galois identity r * f = n belongs to RamificationTheory.HilbertRamification.Dedekind.Basic.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.IdealArtinQuotient

Imported by4

def

idealFrobeniusClass

L38 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealFrobeniusClass

Documentation

The ideal-theoretic Frobenius class attached to a prime outside the defining modulus. Under global reciprocity this is the usual Frobenius automorphism.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable {K : Type} [Field K] [NumberField K]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

def idealFrobeniusClass
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    IdeleClassGroup K ⧸ N

theorem

orderOf_idealFrobeniusClass

L50 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.orderOf_idealFrobeniusClass

Documentation

The order of the Artin image of v is the order of v modulo the ideal group H_m.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable {K : Type} [Field K] [NumberField K]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

theorem orderOf_idealFrobeniusClass
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    orderOf (idealFrobeniusClass m N hm v hv) =
      orderOf
        (QuotientGroup.mk' (idealArtinKernel m N hm)
          (RayClass.primeToModulusIdeal m v hv))

theorem

primeIdeal_pow_mem_idealArtinKernel_iff_orderOf_dvd

L70 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.primeIdeal_pow_mem_idealArtinKernel_iff_orderOf_dvd

Documentation

A power of a prime ideal lies in the defining ideal group exactly when the order of its class in J_K^m / H_m divides the exponent.

This is the precise group-theoretic form of the "smallest positive f with p^f ∈ H_m" clause in the unramified decomposition law.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable {K : Type} [Field K] [NumberField K]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal

Lean source · statement

theorem primeIdeal_pow_mem_idealArtinKernel_iff_orderOf_dvd
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support)
    (n : ℕ) :
    (RayClass.primeToModulusIdeal m v hv) ^ n ∈
        idealArtinKernel m N hm ↔
      orderOf
        (QuotientGroup.mk' (idealArtinKernel m N hm)
            (RayClass.primeToModulusIdeal m v hv)) ∣
        n

Module documentation

Ideal Frobenius classes and the decomposition law

Declarations

idealFrobeniusClass

orderOf_idealFrobeniusClass

primeIdeal_pow_mem_idealArtinKernel_iff_orderOf_dvd