NYLL
Module

IdealArtinQuotient.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.IdealArtinQuotient
7 declarations indexed from sourceView source ↗

Module documentation

The ideal Artin quotient

For a defining modulus m, the ideal-theoretic Artin map is surjective and has kernel H_m. The first isomorphism theorem therefore identifies J_K^m / H_m with the corresponding idelic norm quotient C_K / N.

Imports1
Imported by3

Declarations

instance

idealArtinKernelNormal

L35 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinKernelNormal
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
variable {K : Type} [Field K] [NumberField K]

-- Reuse the normality witness embedded in the imported ideal-Artin definitions.
-- Choosing a different generic witness here makes quotient equivalences compare
-- enormous, propositionally equal but non-definitional terms.
attribute [local instance] ideleClassSubgroupNormal
Lean source · statement
instance idealArtinKernelNormal
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    (idealArtinKernel m N hm).Normal
def

idealClassQuotientEquivNormQuotient

L45 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.idealClassQuotientEquivNormQuotient
Documentation

The ideal class-field isomorphism J_K^m / H_m ≃ C_K / N.

Source context 8 commands

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

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

-- Reuse the normality witness embedded in the imported ideal-Artin definitions.
-- Choosing a different generic witness here makes quotient equivalences compare
-- enormous, propositionally equal but non-definitional terms.
attribute [local instance] ideleClassSubgroupNormal
local instance idealArtinKernelNormal
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    (idealArtinKernel m N hm).Normal := by
  change (idealArtinMap m N hm).ker.Normal
  infer_instance
Lean source · statement
def idealClassQuotientEquivNormQuotient
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    RayClass.primeToModulusIdeals m ⧸
        idealArtinKernel m N hm ≃*
      IdeleClassGroup K ⧸ N
theorem

idealClassQuotientEquivNormQuotient_mk

L65 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.idealClassQuotientEquivNormQuotient_mk
Documentation

The ideal class-field equivalence sends a quotient representative to its ideal Artin image.

Source context 8 commands

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

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

-- Reuse the normality witness embedded in the imported ideal-Artin definitions.
-- Choosing a different generic witness here makes quotient equivalences compare
-- enormous, propositionally equal but non-definitional terms.
attribute [local instance] ideleClassSubgroupNormal
local instance idealArtinKernelNormal
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    (idealArtinKernel m N hm).Normal := by
  change (idealArtinMap m N hm).ker.Normal
  infer_instance
Lean source · statement
theorem idealClassQuotientEquivNormQuotient_mk
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N)
    (a : RayClass.primeToModulusIdeals m) :
    idealClassQuotientEquivNormQuotient m N hm
        (QuotientGroup.mk' (idealArtinKernel m N hm) a) =
      idealArtinMap m N hm a
theorem

idealClassQuotient_mk_eq_one_iff

L77 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.idealClassQuotient_mk_eq_one_iff
Documentation

The Artin kernel is exactly the equivalence relation defining the ideal class-field quotient.

Source context 8 commands

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

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

-- Reuse the normality witness embedded in the imported ideal-Artin definitions.
-- Choosing a different generic witness here makes quotient equivalences compare
-- enormous, propositionally equal but non-definitional terms.
attribute [local instance] ideleClassSubgroupNormal
local instance idealArtinKernelNormal
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    (idealArtinKernel m N hm).Normal := by
  change (idealArtinMap m N hm).ker.Normal
  infer_instance
Lean source · statement
theorem idealClassQuotient_mk_eq_one_iff
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N)
    (a : RayClass.primeToModulusIdeals m) :
    QuotientGroup.mk' (idealArtinKernel m N hm) a = 1 ↔
      idealArtinMap m N hm a = 1
def

idealClassQuotientEquivGaloisGroup

L99 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.idealClassQuotientEquivGaloisGroup
Documentation

The ideal class-field isomorphism with the actual Galois group: J_K^m / H_m ≃ Gal(L/K).

Its first factor is the ideal/idèle norm-quotient comparison, and its second factor is the genuine global norm-residue equivalence.

Source context 10 commands

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

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

-- Reuse the normality witness embedded in the imported ideal-Artin definitions.
-- Choosing a different generic witness here makes quotient equivalences compare
-- enormous, propositionally equal but non-definitional terms.
attribute [local instance] ideleClassSubgroupNormal
local instance idealArtinKernelNormal
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    (idealArtinKernel m N hm).Normal := by
  change (idealArtinMap m N hm).ker.Normal
  infer_instance
section ActualGaloisQuotient
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
def idealClassQuotientEquivGaloisGroup
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range) :
    RayClass.primeToModulusIdeals m ⧸
        idealArtinKernel m
          ((_root_.ideleClassNorm K L).range) hm ≃*
      (L ≃ₐ[K] L)
theorem

idealClassQuotientEquivGaloisGroup_mk

L116 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.idealClassQuotientEquivGaloisGroup_mk
Documentation

On a representative ideal, the actual ideal class-field isomorphism evaluates to the genuine Galois-valued ideal Artin map.

Source context 10 commands

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

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

-- Reuse the normality witness embedded in the imported ideal-Artin definitions.
-- Choosing a different generic witness here makes quotient equivalences compare
-- enormous, propositionally equal but non-definitional terms.
attribute [local instance] ideleClassSubgroupNormal
local instance idealArtinKernelNormal
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    (idealArtinKernel m N hm).Normal := by
  change (idealArtinMap m N hm).ker.Normal
  infer_instance
section ActualGaloisQuotient
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem idealClassQuotientEquivGaloisGroup_mk
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.primeToModulusIdeals m) :
    idealClassQuotientEquivGaloisGroup
        (K := K) (L := L) m hm
        (QuotientGroup.mk'
          (idealArtinKernel m
            ((_root_.ideleClassNorm K L).range) hm) a) =
      idealArtinGaloisMap (K := K) (L := L) m hm a
theorem

idealClassQuotient_mk_eq_one_iff_galoisArtin_eq_one

L132 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.idealClassQuotient_mk_eq_one_iff_galoisArtin_eq_one
Documentation

An ideal class is trivial in the class-field quotient exactly when its actual Galois-valued Artin symbol is trivial.

Source context 10 commands

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

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

-- Reuse the normality witness embedded in the imported ideal-Artin definitions.
-- Choosing a different generic witness here makes quotient equivalences compare
-- enormous, propositionally equal but non-definitional terms.
attribute [local instance] ideleClassSubgroupNormal
local instance idealArtinKernelNormal
    (m : RayClass.Modulus K)
    (N : Subgroup (IdeleClassGroup K))
    (hm : RayClass.Modulus.congruenceSubgroup m ≤ N) :
    (idealArtinKernel m N hm).Normal := by
  change (idealArtinMap m N hm).ker.Normal
  infer_instance
section ActualGaloisQuotient
variable
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem idealClassQuotient_mk_eq_one_iff_galoisArtin_eq_one
    (m : RayClass.Modulus K)
    (hm :
      RayClass.Modulus.congruenceSubgroup m ≤
        (_root_.ideleClassNorm K L).range)
    (a : RayClass.primeToModulusIdeals m) :
    QuotientGroup.mk'
          (idealArtinKernel m
            ((_root_.ideleClassNorm K L).range) hm) a =
        1 ↔
      idealArtinGaloisMap
          (K := K) (L := L) m hm a =
        1

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