Module

RayArtinModulusProjection.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayArtinModulusProjection

5 declarations indexed from sourceView source ↗

Module documentation

Naturality of ray Artin maps under reduction of the modulus

An embedding between two realizations of ray class fields intertwines the Artin action with the canonical projection of ray class groups. The statement uses only Mathlib and public Definitions vocabulary; the idelic implementation appears only in the proof.

Imports7

Imported by2

instance

rayClassGroupCommGroup

L31 ↗

ClassFieldTheory.rayClassGroupCommGroup

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

instance rayClassGroupCommGroup
    {K : Type} [Field K] [NumberField K]
    (m : RayClassModulus K) : CommGroup (RayClassGroup m)

theorem

rayArtin_prime_eq_arithmeticPrimeArtin

L36 ↗

ClassFieldTheory.rayArtin_prime_eq_arithmeticPrimeArtin

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
private local instance rayClassGroupCommGroup
    {K : Type} [Field K] [NumberField K]
    (m : RayClassModulus K) : CommGroup (RayClassGroup m) :=
  { (inferInstance : Group (RayClassGroup m)) with mul_comm := mul_comm' }

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

arithmeticPrimeArtin_restrict_tower

L59 ↗

ClassFieldTheory.arithmeticPrimeArtin_restrict_tower

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
private local instance rayClassGroupCommGroup
    {K : Type} [Field K] [NumberField K]
    (m : RayClassModulus K) : CommGroup (RayClassGroup m) :=
  { (inferInstance : Group (RayClassGroup m)) with mul_comm := mul_comm' }

Lean source · statement

theorem arithmeticPrimeArtin_restrict_tower
    {K E L : Type}
    [Field K] [NumberField K]
    [Field E] [NumberField E]
    [Field L] [NumberField L]
    [Algebra K E] [Algebra E L] [Algebra K L] [IsScalarTower K E L]
    [IsAbelianGalois K E] [IsAbelianGalois K L]
    (v : HeightOneSpectrum (𝓞 K)) :
    AlgEquiv.restrictNormalHom E
        (GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
          (K := K) (L := L) v) =
      GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := E) v

theorem

rayClassGroup_hom_ext_of_prime

L83 ↗

ClassFieldTheory.rayClassGroup_hom_ext_of_prime

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
private local instance rayClassGroupCommGroup
    {K : Type} [Field K] [NumberField K]
    (m : RayClassModulus K) : CommGroup (RayClassGroup m) :=
  { (inferInstance : Group (RayClassGroup m)) with mul_comm := mul_comm' }

Lean source · statement

theorem rayClassGroup_hom_ext_of_prime
    {K : Type} [Field K] [NumberField K]
    {G : Type} [CommGroup G]
    (n : RayClassModulus K)
    (f g : RayClassGroup n →* G)
    (hprime : ∀ (v : HeightOneSpectrum (𝓞 K))
      (hv : v ∉ n.finitePart.support),
        f (rayClassOfFinitePrime n v hv) =
          g (rayClassOfFinitePrime n v hv)) :
    f = g

theorem