Module

UpperRamification.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.UpperRamification

7 declarations indexed from sourceView source ↗

Module documentation

Herbrand functions and upper groups of standard Lubin--Tate levels

This file names the lower filtration, Herbrand function, inverse Herbrand function, and genuine real upper ramification groups attached to the chosen integral-closure valuation on a standard finite Lubin--Tate level.

Imports2

Imported by2

instance

standardLubinTateLevelField_finiteDimensional_forUpperRamification

L31 ↗

LubinTate.standardLubinTateLevelField_finiteDimensional_forUpperRamification

Source context 6 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]

Lean source · statement

instance
    standardLubinTateLevelField_finiteDimensional_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n)

instance

standardLubinTateLevelField_isGalois_forUpperRamification

L38 ↗

LubinTate.standardLubinTateLevelField_isGalois_forUpperRamification

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 RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n

Lean source · statement

instance
    standardLubinTateLevelField_isGalois_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n)

def

standardLubinTateLowerRamificationFiltration

L46 ↗

LubinTate.standardLubinTateLowerRamificationFiltration

Documentation

The lower ramification filtration packaged for the Herbrand API.

Source context 8 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

def standardLubinTateLowerRamificationFiltration
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
      Gal((standardLubinTateLevelField hπ n) / K)

def

standardLubinTateHerbrandFunction

L58 ↗

LubinTate.standardLubinTateHerbrandFunction

Documentation

The Herbrand function of a standard finite Lubin--Tate level.

Source context 8 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

def standardLubinTateHerbrandFunction
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (s : ℝ) : ℝ

def

standardLubinTateInverseHerbrandFunction

L69 ↗

LubinTate.standardLubinTateInverseHerbrandFunction

Documentation

The inverse Herbrand function of a standard finite Lubin--Tate level.

Source context 8 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

def standardLubinTateInverseHerbrandFunction
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (t : ℝ) : ℝ

def

standardLubinTateRealUpperRamificationGroup

L81 ↗

LubinTate.standardLubinTateRealUpperRamificationGroup

Documentation

The genuine real upper ramification group of a standard finite Lubin--Tate level.

Source context 8 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

def standardLubinTateRealUpperRamificationGroup
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (t : ℝ) :
    Subgroup Gal((standardLubinTateLevelField hπ n) / K)

theorem

standardLubinTateRealUpperRamificationGroup_herbrandFunction

L94 ↗

LubinTate.standardLubinTateRealUpperRamificationGroup_herbrandFunction

Documentation

Evaluating the upper filtration at a Herbrand value recovers the corresponding lower group.

Source context 8 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forUpperRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateRealUpperRamificationGroup_herbrandFunction
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (s : ℝ) :
    standardLubinTateRealUpperRamificationGroup hπ n
        (standardLubinTateHerbrandFunction hπ n s) =
      standardLubinTateRealLowerRamificationGroup hπ n s

Module documentation

Herbrand functions and upper groups of standard Lubin--Tate levels

Declarations

standardLubinTateLevelField_finiteDimensional_forUpperRamification

standardLubinTateLevelField_isGalois_forUpperRamification

standardLubinTateLowerRamificationFiltration

standardLubinTateHerbrandFunction

standardLubinTateInverseHerbrandFunction

standardLubinTateRealUpperRamificationGroup

standardLubinTateRealUpperRamificationGroup_herbrandFunction