Module

RayClassSubgroupPrimeSplitting.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassSubgroupPrimeSplitting

1 declaration indexed from sourceView source ↗

Module documentation

Prime splitting in a ray-class subgroup class field

At a prime away from the modulus, complete splitting is equivalent to membership of the prime's ray class in the defining subgroup.

Imports3

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

finitePrime_splitsCompletelyInRayClassSubgroupField_iff

L30 ↗

ClassFieldTheory.finitePrime_splitsCompletelyInRayClassSubgroupField_iff

Documentation

A prime away from the modulus splits completely in the class field of H exactly when its ray class belongs to H.

Source context 5 commands

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

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

Lean source · statement

theorem finitePrime_splitsCompletelyInRayClassSubgroupField_iff
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) (H : Subgroup (RayClassGroup m))
    (R : RayClassSubgroupRealization K m H)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    FinitePrimeSplitsCompletely K R.extension v ↔
      rayClassOfFinitePrime m v hv ∈ H

Module documentation

Prime splitting in a ray-class subgroup class field

Declarations

finitePrime_splitsCompletelyInRayClassSubgroupField_iff