Module

SmallHilbertClassFieldPrimeSplitting.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.SmallHilbertClassFieldPrimeSplitting

1 declaration indexed from sourceView source ↗

Module documentation

Prime splitting in the small Hilbert class field

A finite prime splits completely in the Hilbert class field precisely when its fractional ideal class is trivial. Both sides use Mathlib's native ideal-theoretic objects.

Imports5

Imported by1

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.All

theorem

finitePrime_splitsCompletelyInSmallHilbertClassField_iff_principal

L31 ↗

ClassFieldTheory.finitePrime_splitsCompletelyInSmallHilbertClassField_iff_principal

Documentation

A finite prime splits completely in a small Hilbert class field exactly when its fractional ideal is principal.

Source context 4 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain

Lean source · statement

theorem finitePrime_splitsCompletelyInSmallHilbertClassField_iff_principal
    (K : Type) [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) (hE : IsSmallHilbertClassField E)
    (v : HeightOneSpectrum (𝓞 K)) :
    FinitePrimeSplitsCompletely K E v ↔
      finitePrimeFractionalIdeal v ∈
        (toPrincipalIdeal (𝓞 K) K).range

Module documentation

Prime splitting in the small Hilbert class field

Declarations

finitePrime_splitsCompletelyInSmallHilbertClassField_iff_principal