ClassFieldKernel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The even Artin kernel for totally real extensions

The ordinary finite congruence modulus needed by even Hecke characters is obtained from the actual class-field conductor, whose infinite part is empty in a totally real extension.

theorem OAI.DukePrimeDegree.exists_even_artin_modulus line 25

Source documentation

The norm subgroup of a totally real abelian extension has a defining modulus with no infinite places.

theorem exists_even_artin_modulus
    (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L]
    [Algebra K L] [IsAbelianGalois K L] [NumberField.IsTotallyReal L] :
    ∃ m : RayClass.Modulus K, m.infinitePart = ∅ ∧
      m.congruenceSubgroup ≤ (ideleClassNorm K L).range := by
…

theorem OAI.DukePrimeDegree.arithmetic_artin_eq_one_of_principal_ray line 43

Source documentation

Arithmetic normalization of the Artin map still annihilates every principal ray ideal.

theorem arithmetic_artin_eq_one_of_principal_ray
    {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L]
    [Algebra K L] [IsAbelianGalois K L]
    (m : RayClass.Modulus K)
    (hm : m.congruenceSubgroup ≤ (ideleClassNorm K L).range)
    (I : RayClass.primeToModulusIdeals m)
    (hI : I ∈ RayClass.principalRayIdealSubgroup m) :
    arithmeticIdealArtinGaloisMap (K := K) (L := L) m hm I = 1 := by
…