Module

SmallHilbertClassFieldPrincipalization.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.SmallHilbertClassFieldPrincipalization

1 declaration indexed from sourceView source ↗

Module documentation

Principalization in the small Hilbert class field

The principal ideal theorem says that extension to the Hilbert class field makes every integral ideal of the base number field principal.

Imports3

Imported by1

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.All

theorem

ideals_becomePrincipalInSmallHilbertClassField

L25 ↗

ClassFieldTheory.ideals_becomePrincipalInSmallHilbertClassField

Documentation

Every integral ideal becomes principal in a small Hilbert class field.

Source context 3 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem ideals_becomePrincipalInSmallHilbertClassField
    (K : Type) [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) (hE : IsSmallHilbertClassField E) :
    ∀ I : Ideal (𝓞 K),
      (I.map (algebraMap (𝓞 K) (𝓞 E))).IsPrincipal

Module documentation

Principalization in the small Hilbert class field

Declarations

ideals_becomePrincipalInSmallHilbertClassField