Module

SmallHilbertClassFieldOrdinaryRayRealization.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.SmallHilbertClassFieldOrdinaryRayRealization

1 declaration indexed from sourceView source ↗

Module documentation

The small Hilbert class field as an ordinary ray class field

Its ordinary-class Artin isomorphism and everywhere-unramifiedness give a ray-class-field realization whose extension is the original field.

Imports4

Imported by2

theorem

smallHilbertClassField_hasOrdinaryRayRealization

L29 ↗

ClassFieldTheory.smallHilbertClassField_hasOrdinaryRayRealization

Documentation

A small Hilbert class field realizes the ordinary ray class group, with the same extension and arithmetic Frobenius normalization.

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 smallHilbertClassField_hasOrdinaryRayRealization
    (K : Type) [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) (hE : IsSmallHilbertClassField E) :
    ∃ R : RayClassFieldRealization K (ordinaryRayClassModulus K),
      R.extension = E

Module documentation

The small Hilbert class field as an ordinary ray class field

Declarations

smallHilbertClassField_hasOrdinaryRayRealization