Module

GlobalCompositumLocalizationEmbedding.lean

Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumLocalizationEmbedding

2 declarations indexed from sourceView source ↗

Module documentation

Embedding the localized global compositum in the common cyclotomic target

The synchronized global embedding is an isometry for the pulled-back place. It therefore extends to completions. Compatibility on the completed base identifies the restriction to the chosen localization as a genuine ℚ_p-algebra embedding into the same common cyclotomic target.

Imports2

Imported by3

def

kroneckerWeberGlobalCompositumLocalizationAlgHom

L31 ↗

KroneckerWeber.kroneckerWeberGlobalCompositumLocalizationAlgHom

Documentation

The actual embedding type, named one layer before taking Nonempty so later theorem declarations do not normalize the localization construction.

Source context 6 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]

Lean source · statement

def kroneckerWeberGlobalCompositumLocalizationAlgHom
    (p : Nat.Primes) [Fact p.1.Prime]
    (hp : p ∈ kroneckerWeberRamifiedPrimes (L := L)) : Type

theorem

kroneckerWeberGlobalCompositumLocalizationEmbedding

L42 ↗

KroneckerWeber.kroneckerWeberGlobalCompositumLocalizationEmbedding