Module

StandardDominatingExtension.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.StandardDominatingExtension

2 declarations indexed from sourceView source ↗

Module documentation

Characteristic-independent dominating standard extensions

Every finite abelian local extension embeds into the fixed field represented by a compositum of a canonical unramified factor and a canonical standard Lubin--Tate factor. Reverse inclusion of norm subgroups supplies the embedding.

Imports3

Imported by2

theorem

exists_finiteAbelianDominatingStandardLubinTateCompositum

L34 ↗

LocalClassFieldTheory.exists_finiteAbelianDominatingStandardLubinTateCompositum

Documentation

Source-producing form retaining the unramified degree, positive principal-unit level, and the named characteristic-independent standard compositum.

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem exists_finiteAbelianDominatingStandardLubinTateCompositum
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    ∃ (d n : ℕ) (hd : 0 < d) (_hn : 0 < n),
      Nonempty
        (L →ₐ[K]
          abstractFixedField K (SeparableClosure K)
            (standardLubinTateFiniteAbelianCompositum K d n hd).field)

theorem

exists_finiteAbelianDominatingStandardFixedField

L72 ↗

LocalClassFieldTheory.exists_finiteAbelianDominatingStandardFixedField