Module

BigHilbertClassFieldPrimeSplitting.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.BigHilbertClassFieldPrimeSplitting

1 declaration indexed from sourceView source ↗

Module documentation

Prime splitting in the big Hilbert class field

A finite prime splits completely in the big Hilbert class field precisely when its narrow ideal class is trivial. Real-place ramification does not affect this finite-prime criterion.

Imports5

Imported by2

theorem

finitePrime_splitsCompletelyInBigHilbertClassField_iff

L30 ↗

ClassFieldTheory.finitePrime_splitsCompletelyInBigHilbertClassField_iff

Documentation

A finite prime splits completely in the big Hilbert class field exactly when its narrow ray class is trivial.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem finitePrime_splitsCompletelyInBigHilbertClassField_iff
    (K : Type) [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) (hE : IsBigHilbertClassField E)
    (v : HeightOneSpectrum (𝓞 K)) :
    FinitePrimeSplitsCompletely K E v ↔
      narrowRayClassOfFinitePrime v = 1

Module documentation

Prime splitting in the big Hilbert class field

Declarations

finitePrime_splitsCompletelyInBigHilbertClassField_iff