NYLL
Module

IdealDecompositionLaw.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.IdealDecompositionLaw
16 declarations indexed from sourceView source ↗

Module documentation

The ideal-theoretic unramified decomposition law

This file identifies the ideal Artin symbol of a prime with the genuine global and local Frobenius automorphism. For an unramified prime it then combines this identification with the Dedekind-domain fundamental identity to give the complete decomposition law:

  • the order of the prime class modulo the defining ideal group;
  • the order of the actual Frobenius automorphism;
  • the common inertia degree of the primes above it; and
  • the number of primes above it

are related by the global ideal decomposition law.

Imports5
Imported by3

Declarations

theorem

idealArtinGaloisMap_primeToIdealMap_eq_globalArtin

L55 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinGaloisMap_primeToIdealMap_eq_globalArtin
Documentation

The actual idèlic and ideal-theoretic Artin maps form the commutative square of the ideal formulation of global reciprocity.

For every idèle prime to the defining modulus, applying the ideal Artin map to its fractional ideal gives its genuine global Artin automorphism.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem idealArtinGaloisMap_primeToIdealMap_eq_globalArtin
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.idelePrimeToModulusSubgroup m) :
    idealArtinGaloisMap (K := K) (L := L) m hm
        (RayClass.primeToIdealMap m a) =
      Reciprocity.globalArtinMonoidHom
        (K := K) (L := L) (a : IdeleGroup K)
theorem

idealArtinGaloisMap_primeIdeal_eq_finitePlacePrimeArtin

L84 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinGaloisMap_primeIdeal_eq_finitePlacePrimeArtin
Documentation

The Galois-valued ideal Artin map sends a prime ideal outside a defining modulus to the actual global prime Artin element. The latter is, by finite-place local-global compatibility, the genuine chosen local Frobenius value of a normalized order-one element.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem idealArtinGaloisMap_primeIdeal_eq_finitePlacePrimeArtin
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    idealArtinGaloisMap (K := K) (L := L) m hm
        (RayClass.primeToModulusIdeal m v hv) =
      GlobalClassFields.finitePlacePrimeArtin
        (K := K) (L := L) v
theorem

idealArtinGaloisMap_primeIdeal_eq_chosenFinitePlaceArtin

L106 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinGaloisMap_primeIdeal_eq_chosenFinitePlaceArtin
Documentation

Direct local form of the prime-ideal Artin identification: the ideal Artin symbol is the chosen finite-place Artin value of the normalized order-one local element.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem idealArtinGaloisMap_primeIdeal_eq_chosenFinitePlaceArtin
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    idealArtinGaloisMap (K := K) (L := L) m hm
        (RayClass.primeToModulusIdeal m v hv) =
      Reciprocity.chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v
        (FiniteIdeleGroup.chosenLocalOrderSection v 1)
theorem

idealClassQuotientEquivGaloisGroup_primeIdeal

L124 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.idealClassQuotientEquivGaloisGroup_primeIdeal
Documentation

The actual ideal class-field equivalence sends the class of a prime ideal to the genuine finite-place Frobenius automorphism.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem idealClassQuotientEquivGaloisGroup_primeIdeal
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    idealClassQuotientEquivGaloisGroup
        (K := K) (L := L) m hm
        (QuotientGroup.mk'
          (idealArtinKernel m
            ((_root_.ideleClassNorm K L).range) hm)
          (RayClass.primeToModulusIdeal m v hv)) =
      GlobalClassFields.finitePlacePrimeArtin
        (K := K) (L := L) v
theorem

ramificationIndex_eq_one_of_chosenFinitePlaceUnramified

L145 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.ramificationIndex_eq_one_of_chosenFinitePlaceUnramified
Documentation

Completed unramifiedness at the chosen place gives ramification index one in the integral Dedekind extension.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem ramificationIndex_eq_one_of_chosenFinitePlaceUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    Ideal.ramificationIdxIn v.asIdeal (𝓞 L) = 1
theorem

finitePlaceLocalDegree_eq_inertiaDegree_of_chosenUnramified

L179 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.finitePlaceLocalDegree_eq_inertiaDegree_of_chosenUnramified
Documentation

At an unramified finite place, the chosen completion degree equals the common ideal-theoretic inertia degree of the primes above it.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem finitePlaceLocalDegree_eq_inertiaDegree_of_chosenUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    _root_.finitePlaceLocalDegree
        (K := K) (L := L) v =
      Ideal.inertiaDegIn v.asIdeal (𝓞 L)
theorem

orderOf_idealPrimeClass_eq_inertiaDegree_of_chosenUnramified

L247 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.orderOf_idealPrimeClass_eq_inertiaDegree_of_chosenUnramified
Documentation

For an unramified prime, the order of its class modulo the ideal Artin kernel is the common inertia degree. Equivalently, it is the order of the genuine global/local Frobenius automorphism.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem orderOf_idealPrimeClass_eq_inertiaDegree_of_chosenUnramified
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support)
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    orderOf
        (QuotientGroup.mk'
          (idealArtinKernel m
            ((_root_.ideleClassNorm K L).range) hm)
          (RayClass.primeToModulusIdeal m v hv)) =
      Ideal.inertiaDegIn v.asIdeal (𝓞 L)
theorem

unramifiedPrime_pow_mem_idealArtinKernel_iff_inertiaDegree_dvd

L295 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.unramifiedPrime_pow_mem_idealArtinKernel_iff_inertiaDegree_dvd
Documentation

The ideal Artin kernel detects precisely the multiples of the unramified inertia degree among powers of the prime ideal.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem unramifiedPrime_pow_mem_idealArtinKernel_iff_inertiaDegree_dvd
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support)
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v)
    (n : ℕ) :
    (RayClass.primeToModulusIdeal m v hv) ^ n ∈
        idealArtinKernel m
          ((_root_.ideleClassNorm K L).range) hm ↔
      Ideal.inertiaDegIn v.asIdeal (𝓞 L) ∣ n
theorem

unramifiedPrime_numberOfPrimes_eq_extensionDegree_div_inertiaDegree

L317 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.unramifiedPrime_numberOfPrimes_eq_extensionDegree_div_inertiaDegree
Documentation

In an unramified Galois extension, the number of primes above v is the extension degree divided by their common inertia degree.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem unramifiedPrime_numberOfPrimes_eq_extensionDegree_div_inertiaDegree
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    (v.asIdeal.primesOver (𝓞 L)).ncard =
      Module.finrank K L /
        Ideal.inertiaDegIn v.asIdeal (𝓞 L)
theorem

unramifiedPrime_idealMap_eq_product_primesOver

L343 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.unramifiedPrime_idealMap_eq_product_primesOver
Documentation

In an unramified Galois extension, the extended base prime is the product of the distinct primes above it: every exponent is one.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem unramifiedPrime_idealMap_eq_product_primesOver
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    Ideal.map (algebraMap (𝓞 K) (𝓞 L)) v.asIdeal =
      ∏ P ∈ v.asIdeal.primesOver (𝓞 L), P
theorem

primeAbove_inertiaDegree_eq_common

L368 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.primeAbove_inertiaDegree_eq_common
Documentation

Every prime above an unramified base prime has the common inertia degree inertiaDegIn v (𝓞 L).

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem primeAbove_inertiaDegree_eq_common
    (v : HeightOneSpectrum (𝓞 K))
    (P : Ideal (𝓞 L))
    (hP : P ∈ v.asIdeal.primesOver (𝓞 L)) :
    P.inertiaDeg (𝓞 K) =
      Ideal.inertiaDegIn v.asIdeal (𝓞 L)
theorem

unramifiedPrime_numberOfPrimes_eq_extensionDegree_div_idealClassOrder

L390 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.unramifiedPrime_numberOfPrimes_eq_extensionDegree_div_idealClassOrder
Documentation

The number of prime factors above an unramified prime is the extension degree divided by the order of its ideal class modulo the defining ideal group.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · statement
theorem unramifiedPrime_numberOfPrimes_eq_extensionDegree_div_idealClassOrder
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support)
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    (v.asIdeal.primesOver (𝓞 L)).ncard =
      Module.finrank K L /
        orderOf
          (QuotientGroup.mk'
            (idealArtinKernel m
              ((_root_.ideleClassNorm K L).range) hm)
            (RayClass.primeToModulusIdeal m v hv))
theorem

unramifiedPrime_idealDecompositionLaw

L419 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.unramifiedPrime_idealDecompositionLaw
Documentation

Full ideal-theoretic decomposition law for an unramified prime.

The prime factors are distinct, all have inertia degree equal to the order of the prime class modulo the defining ideal group, and their number is the global degree divided by that order.

Source context 8 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
Lean source · full declaration
theorem unramifiedPrime_idealDecompositionLaw
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support)
    (hunram :
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    let f :=
      orderOf
        (QuotientGroup.mk'
          (idealArtinKernel m
            ((_root_.ideleClassNorm K L).range) hm)
          (RayClass.primeToModulusIdeal m v hv))
    Ideal.map (algebraMap (𝓞 K) (𝓞 L)) v.asIdeal =
        ∏ P ∈ v.asIdeal.primesOver (𝓞 L), P ∧
      (∀ P : Ideal (𝓞 L),
        P ∈ v.asIdeal.primesOver (𝓞 L) →
          P.inertiaDeg (𝓞 K) = f) ∧
      (v.asIdeal.primesOver (𝓞 L)).ncard =
        Module.finrank K L / f := by
  dsimp only
  refine
    ⟨unramifiedPrime_idealMap_eq_product_primesOver
        (K := K) (L := L) v hunram, ?_, ?_⟩
  · intro P hP
    rw [
      orderOf_idealPrimeClass_eq_inertiaDegree_of_chosenUnramified
        (K := K) (L := L) m hm v hv hunram]
    exact
      primeAbove_inertiaDegree_eq_common
        (K := K) (L := L) v P hP
  · exact
      unramifiedPrime_numberOfPrimes_eq_extensionDegree_div_idealClassOrder
        (K := K) (L := L) m hm v hv hunram
theorem

smallHilbertClassFieldGaloisEquivClassGroup_finitePlacePrimeArtin

L464 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldGaloisEquivClassGroup_finitePlacePrimeArtin
Documentation

Under actual reciprocity for the selected small Hilbert class field, its genuine prime Frobenius automorphism is the ordinary ideal class of the corresponding prime.

Source context 10 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
section SmallHilbertPrimeSplitting
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem
    smallHilbertClassFieldGaloisEquivClassGroup_finitePlacePrimeArtin
    (v : HeightOneSpectrum (𝓞 K)) :
    GlobalClassFields.smallHilbertClassFieldGaloisEquivClassGroupOverOriginal
          (K := K)
          (GlobalClassFields.finitePlacePrimeArtin
            (K := K)
            (L := GlobalClassFields.smallHilbertClassField K) v) =
      ClassGroup.mk K (FractionalIdealGroup.prime v)
theorem

smallHilbertClassField_chosenFinitePlaceIsUnramified

L488 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassField_chosenFinitePlaceIsUnramified
Documentation

Every finite place is unramified in the selected small Hilbert class field, in the completed chosen-place formulation used by the local Artin map.

Source context 10 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
section SmallHilbertPrimeSplitting
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem smallHilbertClassField_chosenFinitePlaceIsUnramified
    (v : HeightOneSpectrum (𝓞 K)) :
    _root_.ChosenFinitePlaceIsUnramified
      (K := K)
      (L := GlobalClassFields.smallHilbertClassField K) v
theorem

finitePlaceSplitsCompletelyInSmallHilbertClassField_iff_principal

L511 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.finitePlaceSplitsCompletelyInSmallHilbertClassField_iff_principal
Documentation

A prime of the original number field actually splits completely in the selected small Hilbert class field exactly when its prime ideal is principal.

Source context 10 commands

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

open scoped NumberField BigOperators
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance] idealArtinKernelNormal
section SmallHilbertPrimeSplitting
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceSplitsCompletelyInSmallHilbertClassField_iff_principal
    (v : HeightOneSpectrum (𝓞 K)) :
    _root_.FinitePlaceSplitsCompletely
          (K := K)
          (L := GlobalClassFields.smallHilbertClassField K) v ↔
      FractionalIdealGroup.prime v ∈
        (toPrincipalIdeal (𝓞 K) K).range

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.