Module

ExistsRayArtinModulusProjection.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.ExistsRayArtinModulusProjection

3 declarations indexed from sourceView source ↗

Module documentation

Existence of a modulus-compatible ray class field embedding

Reducing the modulus yields an embedding of ray class field realizations that intertwines their Artin maps.

Imports8

Imported by4

theorem

rayArtin_prime_eq_arithmeticPrimeArtin

L30 ↗

ClassFieldTheory.rayArtin_prime_eq_arithmeticPrimeArtin

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem rayArtin_prime_eq_arithmeticPrimeArtin
    {K : Type} [Field K] [NumberField K]
    {m : RayClassModulus K} (R : RayClassFieldRealization K m)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    R.rayArtin (rayClassOfFinitePrime m v hv) =
      GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := R.extension) v

theorem

rayClassFieldRealization_norm_range

L53 ↗

ClassFieldTheory.rayClassFieldRealization_norm_range

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem rayClassFieldRealization_norm_range
    {K : Type} [Field K] [NumberField K]
    {m : RayClassModulus K} (R : RayClassFieldRealization K m) :
    (_root_.ideleClassNorm K R.extension).range =
      (GlobalClassFieldComparison.rayClassModulusToOriginal K m).congruenceSubgroup

theorem