Module

BigHilbertClassFieldNarrowRayRealization.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.BigHilbertClassFieldNarrowRayRealization

1 declaration indexed from sourceView source ↗

Module documentation

The big Hilbert class field as a narrow ray class field

Its narrow-class Artin isomorphism and unramifiedness at finite primes give a ray-class-field realization whose extension is the original field.

Imports4

Imported by2

theorem

bigHilbertClassField_hasNarrowRayRealization

L29 ↗

ClassFieldTheory.bigHilbertClassField_hasNarrowRayRealization

Documentation

A big Hilbert class field realizes the narrow 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 bigHilbertClassField_hasNarrowRayRealization
    (K : Type) [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) (hE : IsBigHilbertClassField E) :
    ∃ R : RayClassFieldRealization K (narrowRayClassModulus K),
      R.extension = E

Module documentation

The big Hilbert class field as a narrow ray class field

Declarations

bigHilbertClassField_hasNarrowRayRealization