Module

IdealArtinMap.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.IdealArtinMap

33 declarations indexed from sourceView source ↗

Module documentation

The ideal-theoretic Artin map

Let N ≤ C_K be a class-field norm subgroup and let m be a defining modulus, so C_K^m ≤ N. The idelic quotient map then factors through the ideal ray class group. Composing with the projection from ideals prime to m gives the ideal-theoretic Artin map. This file proves its surjectivity, identifies its kernel, and records the exact sequence.

The target is kept as the concrete reciprocity quotient C_K / N; global reciprocity identifies this quotient with the corresponding abelian Galois group.

Imports3

Imported by4

instance

idealArtinMap_ideleClassGroupIsMulCommutative

L38 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinMap_ideleClassGroupIsMulCommutative

Source context 6 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)

instance

ideleClassSubgroupNormal

L43 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.ideleClassSubgroupNormal

Source context 7 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal

def

rayClassToNormQuotient

L49 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rayClassToNormQuotient

Documentation

The quotient map from the ray class group modulo a defining modulus to the class-field reciprocity quotient.

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def rayClassToNormQuotient
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    RayClass.RayClassGroup m →*
      IdeleClassGroup K ⧸ N

theorem

rayClassToNormQuotient_mk

L62 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rayClassToNormQuotient_mk

Documentation

The ray-class quotient map sends the class of an idele class to its class modulo the norm subgroup.

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem rayClassToNormQuotient_mk
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N)
    (c : IdeleClassGroup K) :
    rayClassToNormQuotient m N hm
        (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup m) c) =
      QuotientGroup.mk' N c

theorem

rayClassToNormQuotient_surjective

L74 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rayClassToNormQuotient_surjective

Documentation

The quotient map attached to a defining modulus is surjective.

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem rayClassToNormQuotient_surjective
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    Function.Surjective
      (rayClassToNormQuotient m N hm)

def

idealRayClassArtinMap

L89 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealRayClassArtinMap

Documentation

The Artin map on the ideal ray class group, obtained from the idele-theoretic reciprocity quotient.

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def idealRayClassArtinMap
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    RayClass.IdealRayClassGroup m →*
      IdeleClassGroup K ⧸ N

theorem

idealRayClassArtinMap_surjective

L99 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealRayClassArtinMap_surjective

Documentation

The ideal-ray-class Artin map is surjective.

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem idealRayClassArtinMap_surjective
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    Function.Surjective
      (idealRayClassArtinMap m N hm)

def

idealArtinMap

L110 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinMap

Documentation

The Artin map on fractional ideals prime to m.

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def idealArtinMap
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    RayClass.primeToModulusIdeals m →*
      IdeleClassGroup K ⧸ N

theorem

quotientRaySubgroupEquivIdealRayClassGroup_mk

L120 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.quotientRaySubgroupEquivIdealRayClassGroup_mk

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem
    quotientRaySubgroupEquivIdealRayClassGroup_mk
    (m : RayClass.Modulus K)
    (a : RayClass.idelePrimeToModulusSubgroup m) :
    RayClass.quotientRaySubgroupEquivIdealRayClassGroup m
        (QuotientGroup.mk'
          (RayClass.raySubgroupInPrimeTo m) a) =
      RayClass.idealRayProjection m a

theorem

quotientRaySubgroupEquivIdeleRayQuotient_mk

L130 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.quotientRaySubgroupEquivIdeleRayQuotient_mk

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem
    quotientRaySubgroupEquivIdeleRayQuotient_mk
    (m : RayClass.Modulus K)
    (a : RayClass.idelePrimeToModulusSubgroup m) :
    RayClass.quotientRaySubgroupEquivIdeleRayQuotient m
        (QuotientGroup.mk'
          (RayClass.raySubgroupInPrimeTo m) a) =
      RayClass.primeToRayClassProjection m a

theorem

rayClassGroupEquivIdeleQuotient_mk_mk

L140 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rayClassGroupEquivIdeleQuotient_mk_mk

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

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

L158 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rayClassGroupEquivIdealRayClassGroup_mk_primeTo

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

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

L192 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinMap_primeToIdealMap

Documentation

The ideal Artin map of the fractional ideal attached to a prime-to-modulus idèle is its class in the idèle-class quotient.

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

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

def

idealArtinKernel

L229 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinKernel

Documentation

The ideal group H_m attached to N: precisely the ideals whose Artin class is trivial.

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

def idealArtinKernel
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    Subgroup (RayClass.primeToModulusIdeals m)

theorem

principalRayIdealSubgroup_le_idealArtinKernel

L237 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.principalRayIdealSubgroup_le_idealArtinKernel

Documentation

Principal ray ideals lie in the Artin kernel.

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem principalRayIdealSubgroup_le_idealArtinKernel
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    RayClass.principalRayIdealSubgroup m ≤
      idealArtinKernel m N hm

def

normIdeleLiftedModulus

L266 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.normIdeleLiftedModulus

Documentation

For choosing idèle representatives of ideal norms, retain the finite part of the ideal-norm lifted modulus and impose positivity at every real place upstairs. Its prime-to ideal group is definitionally the same as the one for idealNormLiftedModulus, while positivity makes its idèle norm prime to the selected infinite part downstairs.

Source context 11 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section NormDefinedFiniteKernel
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [FiniteDimensional K L] in

Lean source · statement

def normIdeleLiftedModulus
    (m : RayClass.Modulus K) : RayClass.Modulus L

theorem

ideleNorm_mem_finitePrimeToModulusSubgroup_aux

L272 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.ideleNorm_mem_finitePrimeToModulusSubgroup_aux

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section NormDefinedFiniteKernel
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem ideleNorm_mem_finitePrimeToModulusSubgroup_aux
    (m : RayClass.Modulus K)
    (a : RayClass.idelePrimeToModulusSubgroup
      (normIdeleLiftedModulus (K := K) (L := L) m)) :
    (IdeleGroup.norm K L (a : IdeleGroup L)).2 ∈
      RayClass.finitePrimeToModulusSubgroup m

theorem

ideleNorm_mem_idelePrimeToModulusSubgroup

L302 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.ideleNorm_mem_idelePrimeToModulusSubgroup

Documentation

The idèle norm carries idèles prime to the lifted modulus to idèles prime to the base modulus. At real places this uses positivity of both real-real and complex-real local norms.

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section NormDefinedFiniteKernel
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem ideleNorm_mem_idelePrimeToModulusSubgroup
    (m : RayClass.Modulus K)
    (a : RayClass.idelePrimeToModulusSubgroup
      (normIdeleLiftedModulus
        (K := K) (L := L) m)) :
    IdeleGroup.norm K L (a : IdeleGroup L) ∈
      RayClass.idelePrimeToModulusSubgroup m

def

primeToModulusIdeleNorm

L391 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.primeToModulusIdeleNorm

Documentation

The ordinary idèle norm restricted to the prime-to-modulus subgroups selected by the lifted modulus.

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section NormDefinedFiniteKernel
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · full declaration

def primeToModulusIdeleNorm
    (m : RayClass.Modulus K) :
    RayClass.idelePrimeToModulusSubgroup
        (normIdeleLiftedModulus
          (K := K) (L := L) m) →*
      RayClass.idelePrimeToModulusSubgroup m where
  toFun a :=
    ⟨IdeleGroup.norm K L (a : IdeleGroup L),
      ideleNorm_mem_idelePrimeToModulusSubgroup
        (K := K) (L := L) m a⟩
  map_one' := by
    apply Subtype.ext
    exact map_one (IdeleGroup.norm K L)
  map_mul' a b := by
    apply Subtype.ext
    exact
      (IdeleGroup.norm K L).map_mul
        (a : IdeleGroup L) (b : IdeleGroup L)

theorem

primeToIdealMap_primeToModulusIdeleNorm

L413 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.primeToIdealMap_primeToModulusIdeleNorm

Documentation

The restricted idèle norm and the genuine ideal norm commute with the prime-to-modulus fractional-ideal maps.

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section NormDefinedFiniteKernel
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem primeToIdealMap_primeToModulusIdeleNorm
    (m : RayClass.Modulus K)
    (a : RayClass.idelePrimeToModulusSubgroup
      (normIdeleLiftedModulus
        (K := K) (L := L) m)) :
    RayClass.primeToIdealMap m
        (primeToModulusIdeleNorm
          (K := K) (L := L) m a) =
      RayClass.primeToModulusIdealNorm
        (K := K) (L := L) m
        (RayClass.primeToIdealMap
          (normIdeleLiftedModulus
            (K := K) (L := L) m) a)

theorem

exists_primeToModulusIdele_norm_class_eq_of_mem_idealArtinKernel

L432 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.exists_primeToModulusIdele_norm_class_eq_of_mem_idealArtinKernel

Source context 11 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section NormDefinedFiniteKernel
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem
    exists_primeToModulusIdele_norm_class_eq_of_mem_idealArtinKernel
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    {I : RayClass.primeToModulusIdeals m}
    (hI : I ∈ idealArtinKernel m
      (_root_.ideleClassNorm K L).range hm) :
    ∃ a : RayClass.idelePrimeToModulusSubgroup m,
      RayClass.primeToIdealMap m a = I ∧
        ∃ b : RayClass.idelePrimeToModulusSubgroup
            (normIdeleLiftedModulus
              (K := K) (L := L) m),
          QuotientGroup.mk'
              (IdeleGroup.principalSubgroup K)
              (IdeleGroup.norm K L (b : IdeleGroup L)) =
            QuotientGroup.mk'
              (IdeleGroup.principalSubgroup K)
              (a : IdeleGroup K)

theorem

primeToIdealMap_mem_idealNormSubgroup_of_norm_class_eq

L522 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.primeToIdealMap_mem_idealNormSubgroup_of_norm_class_eq

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section NormDefinedFiniteKernel
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem
    primeToIdealMap_mem_idealNormSubgroup_of_norm_class_eq
    (m : RayClass.Modulus K)
    (a : RayClass.idelePrimeToModulusSubgroup m)
    (b : RayClass.idelePrimeToModulusSubgroup
      (normIdeleLiftedModulus
        (K := K) (L := L) m))
    (hNormClass :
      QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K)
          (IdeleGroup.norm K L (b : IdeleGroup L)) =
        QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K)
          (a : IdeleGroup K)) :
    RayClass.primeToIdealMap m a ∈
      RayClass.idealNormSubgroup
        (K := K) (L := L) m

theorem

idealArtinKernel_le_idealNormSubgroup

L596 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinKernel_le_idealNormSubgroup

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section NormDefinedFiniteKernel
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem idealArtinKernel_le_idealNormSubgroup
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    idealArtinKernel m
        (_root_.ideleClassNorm K L).range hm ≤
      RayClass.idealNormSubgroup
        (K := K) (L := L) m

theorem

idealNormSubgroup_le_idealArtinKernel

L614 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealNormSubgroup_le_idealArtinKernel

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section NormDefinedFiniteKernel
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem idealNormSubgroup_le_idealArtinKernel
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    RayClass.idealNormSubgroup
        (K := K) (L := L) m ≤
      idealArtinKernel m
        (_root_.ideleClassNorm K L).range hm

theorem

idealArtinKernel_eq_idealNormSubgroup_of_finiteExtension

L653 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinKernel_eq_idealNormSubgroup_of_finiteExtension

Documentation

For a finite extension and a defining modulus, the kernel of the ideal Artin map is exactly the genuine norm-defined ideal group N_{L/K} J_L^m P_K^m.

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section NormDefinedFiniteKernel
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem idealArtinKernel_eq_idealNormSubgroup_of_finiteExtension
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    idealArtinKernel m
        (_root_.ideleClassNorm K L).range hm =
      RayClass.idealNormSubgroup
        (K := K) (L := L) m

theorem

idealArtinKernel_eq_idealNormSubgroup

L681 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinKernel_eq_idealNormSubgroup

Documentation

For a defining modulus, the kernel of the ideal Artin map is exactly the genuine norm-defined ideal group N_{L/K} J_L^m P_K^m for a finite Galois extension. This preserves the original Galois-facing API while delegating to the finite-extension theorem.

Source context 11 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section NormDefinedKernel
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem idealArtinKernel_eq_idealNormSubgroup
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    idealArtinKernel m
        (_root_.ideleClassNorm K L).range hm =
      RayClass.idealNormSubgroup
        (K := K) (L := L) m

theorem

idealArtinMap_surjective

L696 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinMap_surjective

Documentation

The Artin map on ideals is surjective.

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem idealArtinMap_surjective
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    Function.Surjective (idealArtinMap m N hm)

theorem

idealArtin_exact

L708 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtin_exact

Documentation

Exactness of 1 → H_m → J_K^m → C_K/N → 1.

Source context 8 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

theorem idealArtin_exact
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    (∀ a : RayClass.primeToModulusIdeals m,
      idealArtinMap m N hm a = 1 ↔
        a ∈ idealArtinKernel m N hm) ∧
      Function.Surjective (idealArtinMap m N hm)

def

idealArtinGaloisMap

L730 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinGaloisMap

Documentation

The ideal-theoretic Artin map with its actual Galois-group target.

For a defining modulus of the genuine norm subgroup N_{L/K} C_L, this is the quotient-valued ideal Artin map followed by the global norm-residue equivalence C_K / N_{L/K} C_L ≃ Gal(L/K).

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section ActualGaloisArtin
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

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

theorem

idealArtinGaloisMap_apply

L746 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinGaloisMap_apply

Documentation

Evaluation of the actual ideal Artin map is the global norm-residue equivalence applied to the quotient-valued ideal Artin class.

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section ActualGaloisArtin
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem idealArtinGaloisMap_apply
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.primeToModulusIdeals m) :
    idealArtinGaloisMap (K := K) (L := L) m hm a =
      Additive.toMul
        (Reciprocity.globalNormResidueEquiv K L
          (Additive.ofMul
            (idealArtinMap m
              ((_root_.ideleClassNorm K L).range) hm a)))

theorem

idealArtinGaloisMap_surjective

L761 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinGaloisMap_surjective

Documentation

The actual Galois-valued ideal Artin map is surjective.

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section ActualGaloisArtin
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

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

theorem

idealArtinGaloisMap_ker

L777 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinGaloisMap_ker

Documentation

Passing from the genuine norm quotient to the actual Galois group does not change the ideal Artin kernel.

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section ActualGaloisArtin
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem idealArtinGaloisMap_ker
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    (idealArtinGaloisMap
        (K := K) (L := L) m hm).ker =
      idealArtinKernel m
        ((_root_.ideleClassNorm K L).range) hm

theorem

idealArtinGalois_exact

L802 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinGalois_exact

Documentation

Exactness of the actual ideal Artin sequence 1 → H_m → J_K^m → Gal(L/K) → 1.

Source context 10 commands

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

open scoped NumberField BigOperators NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open NumberField
variable {K : Type} [Field K] [NumberField K]
local instance
    idealArtinMap_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance ideleClassSubgroupNormal
    (N : Subgroup (IdeleClassGroup K)) : N.Normal :=
  N.normal_of_isMulCommutative
section ActualGaloisArtin
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]

Lean source · statement

theorem idealArtinGalois_exact
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    (∀ a : RayClass.primeToModulusIdeals m,
      idealArtinGaloisMap (K := K) (L := L) m hm a = 1 ↔
        a ∈ idealArtinKernel m
          ((_root_.ideleClassNorm K L).range) hm) ∧
      Function.Surjective
        (idealArtinGaloisMap (K := K) (L := L) m hm)

Module documentation

The ideal-theoretic Artin map

Declarations