Module

BigHilbertClassFieldArtinEquiv.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.BigHilbertClassFieldArtinEquiv

1 declaration indexed from sourceView source ↗

Module documentation

Artin isomorphism for the big Hilbert class field

The narrow ideal class group is isomorphic to the Galois group of the big Hilbert class field. The displayed compatibility with arithmetic Frobenius fixes the Artin normalization of the isomorphism.

Imports7

Imported by3

theorem

bigHilbertClassField_artinEquiv

L33 ↗

ClassFieldTheory.bigHilbertClassField_artinEquiv

Documentation

The narrow class group acts through the Frobenius-normalized Artin isomorphism on a big Hilbert class field.

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_artinEquiv
    (K : Type) [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) (hE : IsBigHilbertClassField E) :
    ∃ artin : RayClassGroup (narrowRayClassModulus K) ≃*
        (E ≃ₐ[K] E),
      ∀ (v : HeightOneSpectrum (𝓞 K))
        (w : HeightOneSpectrum (𝓞 E)),
        w.asIdeal.LiesOver v.asIdeal →
          artin (narrowRayClassOfFinitePrime v) =
            arithmeticFrobeniusAt (K := K) w

Module documentation

Artin isomorphism for the big Hilbert class field

Declarations

bigHilbertClassField_artinEquiv