Module

LevelValuation.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.LevelValuation

2 declarations indexed from sourceView source ↗

Module documentation

Uniqueness of the valuation on standard Lubin--Tate levels

The standard level field is finite and Galois over the local base field. Consequently the complete discrete valuation selected from its integral closure is the unique extension of the base valuation. This is the bridge needed by the genuine lower- and upper-numbering ramification groups.

Imports3

Imported by4

theorem

standardLubinTateLevelCompleteDVF_hasUniqueValuationExtension

L38 ↗

LubinTate.standardLubinTateLevelCompleteDVF_hasUniqueValuationExtension

Documentation

The chosen complete valuation on a standard Lubin--Tate level is the unique extension of the base valuation.

Source context 7 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
open _root_.ValuationTheory.DiscreteValuationField.ValuedExtension (
  HasUniqueValuationExtension
) in

Lean source · statement

theorem standardLubinTateLevelCompleteDVF_hasUniqueValuationExtension
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    HasUniqueValuationExtension.{u, v, u, 0, 0}
      (base := F.toCompleteDVF)
      (target := standardLubinTateLevelCompleteDVF hπ n)

theorem

standardLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension

L55 ↗

LubinTate.standardLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension