Module

IdealNormArtinExactness.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.IdealNormArtinExactness

19 declarations indexed from sourceView source ↗

Module documentation

Ideal norms and arithmetic Artin exactness

For a finite abelian extension L / K and a defining modulus m, the genuine ideal group

N_{L/K} J_L^m P_K^m

is RayClass.idealNormSubgroup. This module identifies it with the kernel of the arithmetic ideal Artin map, descends that map to the corresponding quotient, and states the unramified decomposition law entirely in terms of this norm-defined ideal group.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.ArithmeticIdealDecompositionLaw

Imported by1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.All

theorem

arithmeticIdealArtinGaloisMap_ker_eq_idealNormSubgroup

L43 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap_ker_eq_idealNormSubgroup

Documentation

The kernel of the arithmetic, Galois-valued ideal Artin map is the genuine norm-defined ideal group N_{L/K} J_L^m P_K^m.

Source context 7 commands

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

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

Lean source · statement

theorem arithmeticIdealArtinGaloisMap_ker_eq_idealNormSubgroup
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    (arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm).ker =
      RayClass.idealNormSubgroup
        (K := K) (L := L) m

theorem

arithmeticIdealArtinGaloisMap_eq_one_iff_mem_idealNormSubgroup

L57 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap_eq_one_iff_mem_idealNormSubgroup

Documentation

An ideal prime to m has trivial arithmetic Artin symbol exactly when it belongs to N_{L/K} J_L^m P_K^m.

Source context 7 commands

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

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

Lean source · statement

theorem arithmeticIdealArtinGaloisMap_eq_one_iff_mem_idealNormSubgroup
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.primeToModulusIdeals m) :
    arithmeticIdealArtinGaloisMap
          (K := K) (L := L) m hm a =
        1 ↔
      a ∈ RayClass.idealNormSubgroup
        (K := K) (L := L) m

theorem

arithmeticIdealArtin_norm_exact

L78 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtin_norm_exact

Documentation

Exactness of the arithmetic ideal Artin sequence with its kernel written as the actual norm-defined ideal group.

Source context 7 commands

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

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

Lean source · statement

theorem arithmeticIdealArtin_norm_exact
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    (arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm).ker =
        RayClass.idealNormSubgroup
          (K := K) (L := L) m ∧
      Function.Surjective
        (arithmeticIdealArtinGaloisMap
          (K := K) (L := L) m hm)

def

idealNormQuotientEquivIdeleClassNormQuotient

L100 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealNormQuotientEquivIdeleClassNormQuotient

Documentation

The vertical isomorphism in the ideal/idèle Artin diagram:

J_K^m / (N_{L/K} J_L^{m_L} P_K^m) ≃ C_K / N_{L/K} C_L.

It is the first-isomorphism-theorem comparison for the ideal Artin map, transported across the equality between its kernel and the genuine norm-defined ideal group.

Source context 7 commands

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

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

Lean source · statement

def idealNormQuotientEquivIdeleClassNormQuotient
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    RayClass.primeToModulusIdeals m ⧸
        RayClass.idealNormSubgroup
          (K := K) (L := L) m ≃*
      IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range

theorem

idealNormQuotientEquivIdeleClassNormQuotient_mk

L120 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealNormQuotientEquivIdeleClassNormQuotient_mk

Documentation

The ideal-norm quotient comparison sends an ideal representative to its class in the idèle-class norm quotient.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
attribute [local instance]
  ideleClassSubgroupNormal idealArtinKernelNormal
omit [IsAbelianGalois K L] in

Lean source · statement

theorem idealNormQuotientEquivIdeleClassNormQuotient_mk
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.primeToModulusIdeals m) :
    idealNormQuotientEquivIdeleClassNormQuotient
        (K := K) (L := L) m hm
        (QuotientGroup.mk'
          (RayClass.idealNormSubgroup
            (K := K) (L := L) m) a) =
      idealArtinMap m
        ((_root_.ideleClassNorm K L).range) hm a

def

arithmeticIdealNormQuotientArtinMap

L162 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealNormQuotientArtinMap

Documentation

The arithmetic ideal Artin map descended through the concrete norm-defined ideal group.

Source context 7 commands

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

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

Lean source · statement

def arithmeticIdealNormQuotientArtinMap
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    RayClass.primeToModulusIdeals m ⧸
        RayClass.idealNormSubgroup
          (K := K) (L := L) m →*
      (L ≃ₐ[K] L)

theorem

arithmeticIdealNormQuotientArtinMap_mk

L184 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealNormQuotientArtinMap_mk

Documentation

The descended arithmetic ideal Artin map evaluates on quotient representatives as the original arithmetic ideal Artin map.

Source context 7 commands

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

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

Lean source · statement

theorem arithmeticIdealNormQuotientArtinMap_mk
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.primeToModulusIdeals m) :
    arithmeticIdealNormQuotientArtinMap
        (K := K) (L := L) m hm
        (QuotientGroup.mk'
          (RayClass.idealNormSubgroup
            (K := K) (L := L) m) a) =
      arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm a

theorem

arithmeticIdealNormQuotientArtinMap_injective

L201 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealNormQuotientArtinMap_injective

Documentation

The arithmetic ideal Artin map on the concrete norm quotient is injective.

Source context 7 commands

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

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

Lean source · statement

theorem arithmeticIdealNormQuotientArtinMap_injective
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    Function.Injective
      (arithmeticIdealNormQuotientArtinMap
        (K := K) (L := L) m hm)

theorem

arithmeticIdealNormQuotientArtinMap_surjective

L235 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealNormQuotientArtinMap_surjective

Documentation

The arithmetic ideal Artin map on the concrete norm quotient is surjective.

Source context 7 commands

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

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

Lean source · statement

theorem arithmeticIdealNormQuotientArtinMap_surjective
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    Function.Surjective
      (arithmeticIdealNormQuotientArtinMap
        (K := K) (L := L) m hm)

theorem

arithmeticIdealNormQuotientArtinMap_eq_normResidue

L258 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealNormQuotientArtinMap_eq_normResidue

Documentation

The descended ideal Artin map is the arithmetic global norm-residue map after the vertical ideal/idèle quotient isomorphism. This is the commutative square in the ideal-theoretic Artin reciprocity theorem.

Source context 7 commands

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

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

Lean source · statement

theorem arithmeticIdealNormQuotientArtinMap_eq_normResidue
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (q :
      RayClass.primeToModulusIdeals m ⧸
        RayClass.idealNormSubgroup
          (K := K) (L := L) m) :
    arithmeticIdealNormQuotientArtinMap
        (K := K) (L := L) m hm q =
      Reciprocity.arithmeticGlobalNormResidueContinuousMulEquiv
        K L
        (idealNormQuotientEquivIdeleClassNormQuotient
          (K := K) (L := L) m hm q)

def

arithmeticIdealNormQuotientEquivGaloisGroup

L287 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealNormQuotientEquivGaloisGroup

Documentation

The canonical arithmetic ideal class-field isomorphism

J_K^m / (N_{L/K} J_L^m P_K^m) ≃ Gal(L/K).

Both the source subgroup and the target Galois group are the concrete objects occurring in the extension L / K.

Source context 7 commands

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

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

Lean source · statement

def arithmeticIdealNormQuotientEquivGaloisGroup
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    RayClass.primeToModulusIdeals m ⧸
        RayClass.idealNormSubgroup
          (K := K) (L := L) m ≃*
      (L ≃ₐ[K] L)

theorem

arithmeticIdealNormQuotientEquivGaloisGroup_mk

L305 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealNormQuotientEquivGaloisGroup_mk

Documentation

The arithmetic ideal norm-quotient equivalence sends a quotient representative to its arithmetic ideal Artin symbol.

Source context 7 commands

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

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

Lean source · statement

theorem arithmeticIdealNormQuotientEquivGaloisGroup_mk
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.primeToModulusIdeals m) :
    arithmeticIdealNormQuotientEquivGaloisGroup
        (K := K) (L := L) m hm
        (QuotientGroup.mk'
          (RayClass.idealNormSubgroup
            (K := K) (L := L) m) a) =
      arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm a

theorem

arithmeticIdealNormQuotientEquivGaloisGroup_eq_normResidue

L322 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealNormQuotientEquivGaloisGroup_eq_normResidue

Documentation

The canonical quotient equivalence makes the full arithmetic ideal/idèle reciprocity diagram commute.

Source context 7 commands

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

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

Lean source · statement

theorem arithmeticIdealNormQuotientEquivGaloisGroup_eq_normResidue
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (q :
      RayClass.primeToModulusIdeals m ⧸
        RayClass.idealNormSubgroup
          (K := K) (L := L) m) :
    arithmeticIdealNormQuotientEquivGaloisGroup
        (K := K) (L := L) m hm q =
      Reciprocity.arithmeticGlobalNormResidueContinuousMulEquiv
        K L
        (idealNormQuotientEquivIdeleClassNormQuotient
          (K := K) (L := L) m hm q)

theorem

orderOf_arithmeticIdealNormPrimeClass_eq_inertiaDegree_of_chosenUnramified

L342 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.orderOf_arithmeticIdealNormPrimeClass_eq_inertiaDegree_of_chosenUnramified

Documentation

For an unramified prime outside m, the order of its class modulo the norm-defined ideal group is the common residue degree upstairs.

Source context 7 commands

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

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

Lean source · statement

theorem
    orderOf_arithmeticIdealNormPrimeClass_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'
          (RayClass.idealNormSubgroup
            (K := K) (L := L) m)
          (RayClass.primeToModulusIdeal m v hv)) =
      Ideal.inertiaDegIn v.asIdeal (𝓞 L)

theorem

unramifiedPrime_pow_mem_idealNormSubgroup_iff_inertiaDegree_dvd

L367 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.unramifiedPrime_pow_mem_idealNormSubgroup_iff_inertiaDegree_dvd

Documentation

A power of an unramified prime lies in the norm-defined ideal group exactly when its common residue degree divides the exponent.

Source context 7 commands

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

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

Lean source · statement

theorem
    unramifiedPrime_pow_mem_idealNormSubgroup_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 ∈
        RayClass.idealNormSubgroup
          (K := K) (L := L) m ↔
      Ideal.inertiaDegIn v.asIdeal (𝓞 L) ∣ n

theorem

unramifiedPrime_idealNormDecompositionLaw

L391 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.unramifiedPrime_idealNormDecompositionLaw

Documentation

The full unramified decomposition law, with f defined as the order of the prime class modulo the genuine norm-defined ideal group.

Source context 7 commands

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

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

Lean source · full declaration

theorem unramifiedPrime_idealNormDecompositionLaw
    (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'
          (RayClass.idealNormSubgroup
            (K := K) (L := L) m)
          (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
  rw [← idealArtinKernel_eq_idealNormSubgroup
    (K := K) (L := L) m hm]
  exact
    unramifiedPrime_idealDecompositionLaw
      (K := K) (L := L) m hm v hv hunram

theorem

finitePlaceSplitsCompletely_iff_primeIdeal_mem_idealNormSubgroup

L422 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.finitePlaceSplitsCompletely_iff_primeIdeal_mem_idealNormSubgroup

Documentation

An unramified prime outside m splits completely exactly when its ideal class belongs to N_{L/K} J_L^m P_K^m.

Source context 7 commands

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

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

Lean source · statement

theorem
    finitePlaceSplitsCompletely_iff_primeIdeal_mem_idealNormSubgroup
    (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) :
    _root_.FinitePlaceSplitsCompletely
          (K := K) (L := L) v ↔
      RayClass.primeToModulusIdeal m v hv ∈
        RayClass.idealNormSubgroup
          (K := K) (L := L) m

theorem

arithmeticIdealArtin_ker_eq_norm_range_sup_ray_principal

L476 ↗

ClassFieldTheory.arithmeticIdealArtin_ker_eq_norm_range_sup_ray_principal

Documentation

The arithmetic ideal Artin kernel is the join of the genuine ideal-norm image with the ray-principal ideal subgroup.

Source context 5 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem arithmeticIdealArtin_ker_eq_norm_range_sup_ray_principal
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    (GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap
        (K := K) (L := L) m hm).ker =
      (RayClass.primeToModulusIdealNorm
        (K := K) (L := L) m).range ⊔
        RayClass.principalRayIdealSubgroup m

theorem

arithmeticIdealArtin_eq_one_iff_norm_range_sup_ray_principal

L492 ↗

ClassFieldTheory.arithmeticIdealArtin_eq_one_iff_norm_range_sup_ray_principal

Documentation

An ideal has trivial arithmetic Artin symbol precisely when it lies in the group generated by ideal norms and ray-principal ideals.

Source context 5 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem arithmeticIdealArtin_eq_one_iff_norm_range_sup_ray_principal
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.primeToModulusIdeals m) :
    GlobalClassFieldTheory.IdealClassFieldTheory.arithmeticIdealArtinGaloisMap
          (K := K) (L := L) m hm a = 1 ↔
      a ∈ (RayClass.primeToModulusIdealNorm
        (K := K) (L := L) m).range ⊔
          RayClass.principalRayIdealSubgroup m

Module documentation

Ideal norms and arithmetic Artin exactness

Declarations