Module

EqualCharacteristicDominatingExtension.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.EqualCharacteristicDominatingExtension

2 declarations indexed from sourceView source ↗

Module documentation

Equal-characteristic dominating extensions

Every finite abelian extension of a positive-characteristic local field embeds into the fixed field represented by a finite abelian compositum of an unramified factor and a transported Lubin--Tate factor. This is the source-producing field extension used for descent of filtered reciprocity.

Imports3

Imported by2

theorem

exists_equalCharacteristicFiniteAbelianDominatingStandardCompositum

L34 ↗

LocalClassFieldTheory.exists_equalCharacteristicFiniteAbelianDominatingStandardCompositum

Documentation

Source-producing form retaining the uniformizer, the unramified degree, the Lubin--Tate level, and the named standard compositum.

Source context 8 commands

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

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

Lean source · statement

theorem exists_equalCharacteristicFiniteAbelianDominatingStandardCompositum
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (p : ℕ) [Fact p.Prime] [CharP K p] :
    ∃ (ϖ : Kˣ) (d n : ℕ)
        (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
        (hd : 0 < d) (_hn : 0 < n),
      Nonempty
        (L →ₐ[K]
          abstractFixedField K (SeparableClosure K)
            (equalCharacteristicStandardFiniteAbelianCompositum
              K p ϖ hϖ d n hd).field)

theorem

exists_equalCharacteristicFiniteAbelianDominatingFixedField

L81 ↗

LocalClassFieldTheory.exists_equalCharacteristicFiniteAbelianDominatingFixedField