Module

SmallHilbertClassFieldArtinEquiv.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.SmallHilbertClassFieldArtinEquiv

1 declaration indexed from sourceView source ↗

Module documentation

Artin isomorphism for the small Hilbert class field

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

Imports7

Imported by2

theorem

smallHilbertClassField_artinEquiv

L33 ↗

ClassFieldTheory.smallHilbertClassField_artinEquiv

Documentation

The ordinary class group acts through the Frobenius-normalized Artin isomorphism on a small 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 smallHilbertClassField_artinEquiv
    (K : Type) [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) (hE : IsSmallHilbertClassField E) :
    ∃ artin : RayClassGroup (ordinaryRayClassModulus K) ≃*
        (E ≃ₐ[K] E),
      ∀ (v : HeightOneSpectrum (𝓞 K))
        (w : HeightOneSpectrum (𝓞 E)),
        w.asIdeal.LiesOver v.asIdeal →
          artin (ordinaryRayClassOfFinitePrime v) =
            arithmeticFrobeniusAt (K := K) w

Module documentation

Artin isomorphism for the small Hilbert class field

Declarations

smallHilbertClassField_artinEquiv