Module

LowerRamification.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.LowerRamification

5 declarations indexed from sourceView source ↗

Module documentation

Lower ramification groups of standard Lubin--Tate levels

This file places the genuine real lower ramification filtration on a standard Lubin--Tate level. Since the integral closure is generated by the primitive Lubin--Tate uniformizer, membership at a natural index is detected by the displacement of that one element.

Imports4

Imported by3

def

standardLubinTateRealLowerRamificationGroup

L37 ↗

LubinTate.standardLubinTateRealLowerRamificationGroup

Documentation

The actual real lower ramification group of a standard Lubin--Tate level, formed using its integral-closure 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 RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

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

instance

standardLubinTateLevelField_finiteDimensional_forLowerRamification

L48 ↗

LubinTate.standardLubinTateLevelField_finiteDimensional_forLowerRamification

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
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

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

instance

standardLubinTateLevelField_isGalois_forLowerRamification

L55 ↗

LubinTate.standardLubinTateLevelField_isGalois_forLowerRamification

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
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forLowerRamification
    {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_forLowerRamification
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n)

theorem

mem_standardLubinTateRealLowerRamificationGroup_nat_iff_primitivePoint

L65 ↗

LubinTate.mem_standardLubinTateRealLowerRamificationGroup_nat_iff_primitivePoint

Documentation

At a natural lower index, an automorphism belongs to the lower ramification group exactly when its displacement of the primitive Lubin--Tate uniformizer has additive valuation at least i + 1.

Source context 9 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
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forLowerRamification
    {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_forLowerRamification
    {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 mem_standardLubinTateRealLowerRamificationGroup_nat_iff_primitivePoint
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n i : ℕ)
    (σ : Gal((standardLubinTateLevelField hπ n)/K)) :
    σ ∈ standardLubinTateRealLowerRamificationGroup hπ n (i : ℝ) ↔
      ((i + 1 : ℕ) : ℕ∞) ≤
        IsDiscreteValuationRing.addVal
          (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
          (valuationSubringAutOfUniqueExtension
              (standardLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
                hπ n)
              σ (standardLubinTatePrimitivePointInteger hπ n) -
            standardLubinTatePrimitivePointInteger hπ n)

theorem

standardLubinTateRealLowerRamificationGroup_eq_natCeil

L127 ↗

LubinTate.standardLubinTateRealLowerRamificationGroup_eq_natCeil

Documentation

At a nonnegative real lower index, the standard lower group is already the group at the natural-number ceiling of that index.

Source context 9 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
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forLowerRamification
    {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_forLowerRamification
    {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 standardLubinTateRealLowerRamificationGroup_eq_natCeil
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (s : ℝ) (hs : 0 ≤ s) :
    standardLubinTateRealLowerRamificationGroup hπ n s =
      standardLubinTateRealLowerRamificationGroup
        hπ n (⌈s⌉₊ : ℝ)

Module documentation

Lower ramification groups of standard Lubin--Tate levels

Declarations

standardLubinTateRealLowerRamificationGroup

standardLubinTateLevelField_finiteDimensional_forLowerRamification

standardLubinTateLevelField_isGalois_forLowerRamification

mem_standardLubinTateRealLowerRamificationGroup_nat_iff_primitivePoint

standardLubinTateRealLowerRamificationGroup_eq_natCeil