Module

SmallHilbertClassFieldUniqueUpToEquiv.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.SmallHilbertClassFieldUniqueUpToEquiv

1 declaration indexed from sourceView source ↗

Module documentation

Small Hilbert class fields are isomorphic

The intrinsic maximality condition determines a small Hilbert class field up to an isomorphism over the base. This asserts existence of an isomorphism, not a distinguished or unique choice of one.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.All

theorem

smallHilbertClassFields_equiv

L28 ↗

ClassFieldTheory.smallHilbertClassFields_equiv

Documentation

Any two small Hilbert class fields are isomorphic over the base field. The isomorphism itself need not be unique.

Source context 4 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem smallHilbertClassFields_equiv
    (K : Type u) [Field K] [NumberField K]
    (E F : FiniteAbelianExtension K)
    (hE : IsSmallHilbertClassField E)
    (hF : IsSmallHilbertClassField F) :
    Nonempty (E ≃ₐ[K] F)

Module documentation

Small Hilbert class fields are isomorphic

Declarations

smallHilbertClassFields_equiv