Module

RayClassOfFinitePrime.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassOfFinitePrime

4 declarations indexed from sourceView source ↗

Module documentation

Prime classes in ray class groups

Imports4

Imported by16

lemma

finitePrimeFractionalIdeal_mem_primeTo

L27 ↗

ClassFieldTheory.finitePrimeFractionalIdeal_mem_primeTo

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

lemma finitePrimeFractionalIdeal_mem_primeTo
    {K : Type u} [Field K] [NumberField K]
    (m : RayClassModulus K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    finitePrimeFractionalIdeal v ∈ rayClassPrimeToIdeals m

def

rayClassOfFinitePrime

L38 ↗

ClassFieldTheory.rayClassOfFinitePrime

Documentation

The class in the ray class group represented by a finite prime away from the modulus.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

def rayClassOfFinitePrime
    {K : Type u} [Field K] [NumberField K]
    (m : RayClassModulus K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) : RayClassGroup m

def

ordinaryRayClassOfFinitePrime

L47 ↗

ClassFieldTheory.ordinaryRayClassOfFinitePrime

Documentation

The ordinary ideal class represented by a finite 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
universe u

Lean source · statement

def ordinaryRayClassOfFinitePrime
    {K : Type u} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) :
    RayClassGroup (ordinaryRayClassModulus K)

def

narrowRayClassOfFinitePrime

L55 ↗

ClassFieldTheory.narrowRayClassOfFinitePrime

Documentation

The narrow ideal class represented by a finite 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
universe u

Lean source · statement

def narrowRayClassOfFinitePrime
    {K : Type u} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) :
    RayClassGroup (narrowRayClassModulus K)

Module documentation

Prime classes in ray class groups

Declarations

finitePrimeFractionalIdeal_mem_primeTo

rayClassOfFinitePrime

ordinaryRayClassOfFinitePrime

narrowRayClassOfFinitePrime