Module

SmallHilbertClassFieldEmbedsInBig.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.SmallHilbertClassFieldEmbedsInBig

1 declaration indexed from sourceView source ↗

Module documentation

Inclusion of the small Hilbert class field in the big one

Everywhere-unramified extensions are unramified at finite places, so the maximality property of a big Hilbert class field supplies the embedding.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.All

theorem

smallHilbertClassField_embedsInBig

L23 ↗

ClassFieldTheory.smallHilbertClassField_embedsInBig

Documentation

Every small Hilbert class field embeds over the base into every big Hilbert class field.

Source context 2 commands

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

namespace ClassFieldTheory
universe u

Lean source · statement

theorem smallHilbertClassField_embedsInBig
    (K : Type u) [Field K] [NumberField K]
    (E : FiniteAbelianExtension K) (hE : IsSmallHilbertClassField E)
    (F : FiniteAbelianExtension K) (hF : IsBigHilbertClassField F) :
    Nonempty (E →ₐ[K] F)

Module documentation

Inclusion of the small Hilbert class field in the big one

Declarations

smallHilbertClassField_embedsInBig