Module

RayClassFieldRealization.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassFieldRealization

1 declaration indexed from sourceView source ↗

Module documentation

Ray class fields

Imports4

Imported by12

structure

RayClassFieldRealization

L27 ↗

ClassFieldTheory.RayClassFieldRealization

Documentation

A finite abelian extension realizing the ray class group through a Frobenius-normalized Artin isomorphism.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe u

Lean source · full declaration

structure RayClassFieldRealization
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) where
  /-- The ray class field. -/
  extension : FiniteAbelianExtension K
  /-- The extension is unramified away from the modulus. -/
  unramifiedOutsideModulus :
    IsUnramifiedOutsideModulus K extension m
  /-- The Artin isomorphism for the ray class field. -/
  artinEquiv : RayClassGroup m ≃* (extension ≃ₐ[K] extension)
  /-- A prime class maps to arithmetic Frobenius. -/
  artin_frobenius :
    ∀ (v : HeightOneSpectrum (𝓞 K))
      (hv : v ∉ m.finitePart.support)
      (w : HeightOneSpectrum (𝓞 extension)),
      w.asIdeal.LiesOver v.asIdeal →
        artinEquiv (rayClassOfFinitePrime m v hv) =
          arithmeticFrobeniusAt (K := K) w

Module documentation

Ray class fields

Declarations

RayClassFieldRealization