Module

FiniteAbelianReciprocityData.lean

Nyll.ClassFieldTheory.Definitions.GlobalClassFieldTheory.FiniteAbelianReciprocityData

1 declaration indexed from sourceView source ↗

Module documentation

Finite abelian global reciprocity data

The interface is ideal-theoretic: a ray-class Artin map is normalized by arithmetic Frobenius away from its modulus.

Imports3

Imported by11

structure

FiniteAbelianReciprocityData

L26 ↗

ClassFieldTheory.FiniteAbelianReciprocityData

Documentation

Finite abelian global-reciprocity data in ideal-theoretic form.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTheory
universe u v

Lean source · full declaration

structure FiniteAbelianReciprocityData
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L] where
  /-- A modulus through which the finite Artin map factors. -/
  modulus : RayClassModulus K
  /-- The extension is unramified away from the modulus. -/
  unramifiedOutsideModulus : IsUnramifiedOutsideModulus K L modulus
  /-- The finite Artin map on the ray class group. -/
  artin : RayClassGroup modulus →* (L ≃ₐ[K] L)
  /-- The finite Artin map is onto. -/
  artin_surjective : Function.Surjective artin
  /-- A prime class maps to arithmetic Frobenius. -/
  artin_frobenius :
    ∀ (v : HeightOneSpectrum (𝓞 K))
      (hv : v ∉ modulus.finitePart.support)
      (w : HeightOneSpectrum (𝓞 L)),
      w.asIdeal.LiesOver v.asIdeal →
        artin (rayClassOfFinitePrime modulus v hv) =
          arithmeticFrobeniusAt (K := K) w

Module documentation

Finite abelian global reciprocity data

Declarations

FiniteAbelianReciprocityData