Module

RayClassFieldPrimeSplitting.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassFieldPrimeSplitting

1 declaration indexed from sourceView source ↗

Module documentation

Prime splitting in a ray class field

For a prime away from the modulus, the Frobenius-normalized Artin isomorphism identifies complete splitting with triviality of the corresponding ray class.

Imports4

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

finitePrime_splitsCompletelyInRayClassField_iff

L32 ↗

ClassFieldTheory.finitePrime_splitsCompletelyInRayClassField_iff

Documentation

A prime away from the modulus splits completely in its ray class field exactly when its ray class is trivial.

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_splitsCompletelyInRayClassField_iff
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K)
    (R : RayClassFieldRealization K m)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ m.finitePart.support) :
    FinitePrimeSplitsCompletely K R.extension v ↔
      rayClassOfFinitePrime m v hv = 1

Module documentation

Prime splitting in a ray class field

Declarations

finitePrime_splitsCompletelyInRayClassField_iff