NYLL
Module

PrimitiveDisplacement.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.PrimitiveDisplacement
35 declarations indexed from sourceView source ↗

Module documentation

Displacements of primitive Lubin--Tate points

For the primitive point at level n + 1, a unit whose first nontrivial principal-unit layer is k displaces that point by an element of normalized additive valuation q ^ k.

The analytic input is proved here rather than assumed. A unit scalar endomorphism is X times an invertible power series. Likewise F(X, Y) - X for the standard formal group is Y times an invertible two-variable power series. Consequently neither operation changes the valuation of the topologically nilpotent input that it multiplies.

Imports5
Imported by4

Declarations

theorem

coeff_subst_X_zero

L47 ↗
LubinTate.coeff_subst_X_zero
Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section FormalFactors
Lean source · statement
theorem coeff_subst_X_zero
    {R : Type*} [CommRing R]
    (f : MvPowerSeries (Fin 2) R) (d : Fin 2 →₀ ℕ)
    (hd : d 1 = 0) :
    PowerSeries.coeff (d 0)
        (MvPowerSeries.subst
          ![(PowerSeries.X : PowerSeries R), 0] f) =
      MvPowerSeries.coeff d f
theorem

standardLubinTateFormalGroup_rightDisplacement_dvd

L73 ↗
LubinTate.standardLubinTateFormalGroup_rightDisplacement_dvd
Documentation

The standard formal-group difference F(X,Y) - X is divisible by Y.

Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section FormalFactors
Lean source · statement
theorem standardLubinTateFormalGroup_rightDisplacement_dvd
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    (MvPowerSeries.X (1 : Fin 2) :
        MvPowerSeries (Fin 2) F.valuationSubring) ∣
      SameUniformizer.standardFormalGroupPowerSeries hπ -
        MvPowerSeries.X (0 : Fin 2)
def

standardLubinTateFormalGroupRightDisplacementFactor

L117 ↗
LubinTate.standardLubinTateFormalGroupRightDisplacementFactor
Documentation

The quotient of F(X,Y) - X by Y.

Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section FormalFactors
Lean source · statement
def standardLubinTateFormalGroupRightDisplacementFactor
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    MvPowerSeries (Fin 2) F.valuationSubring
theorem

standardLubinTateFormalGroup_rightDisplacement_factor

L125 ↗
LubinTate.standardLubinTateFormalGroup_rightDisplacement_factor
Documentation

Factorization of the ordinary displacement in the standard formal group.

Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section FormalFactors
Lean source · statement
theorem standardLubinTateFormalGroup_rightDisplacement_factor
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    SameUniformizer.standardFormalGroupPowerSeries hπ -
        MvPowerSeries.X (0 : Fin 2) =
      MvPowerSeries.X (1 : Fin 2) *
        standardLubinTateFormalGroupRightDisplacementFactor hπ
theorem

standardLubinTateFormalGroupRightDisplacementFactor_constantCoeff

L135 ↗
LubinTate.standardLubinTateFormalGroupRightDisplacementFactor_constantCoeff
Documentation

The formal-group displacement factor has constant coefficient one.

Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section FormalFactors
Lean source · statement
theorem
    standardLubinTateFormalGroupRightDisplacementFactor_constantCoeff
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    MvPowerSeries.constantCoeff
        (standardLubinTateFormalGroupRightDisplacementFactor hπ) = 1
theorem

standardLubinTateFormalGroupRightDisplacementFactor_isUnit

L168 ↗
LubinTate.standardLubinTateFormalGroupRightDisplacementFactor_isUnit
Documentation

The formal-group displacement factor is invertible.

Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section FormalFactors
Lean source · statement
theorem standardLubinTateFormalGroupRightDisplacementFactor_isUnit
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    IsUnit (standardLubinTateFormalGroupRightDisplacementFactor hπ)
def

standardLubinTateEndomorphismLinearFactor

L177 ↗
LubinTate.standardLubinTateEndomorphismLinearFactor
Documentation

The factor left after removing X from the scalar endomorphism [a](X).

Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section FormalFactors
Lean source · statement
def standardLubinTateEndomorphismLinearFactor
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (a : F.valuationSubring) :
    PowerSeries F.valuationSubring
theorem

standardLubinTateEndomorphism_eq_X_mul_linearFactor

L186 ↗
LubinTate.standardLubinTateEndomorphism_eq_X_mul_linearFactor
Documentation

A standard scalar endomorphism is X times its linear factor.

Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section FormalFactors
Lean source · statement
theorem standardLubinTateEndomorphism_eq_X_mul_linearFactor
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (a : F.valuationSubring) :
    SameUniformizer.standardLubinTateEndomorphism hπ a =
      PowerSeries.X *
        standardLubinTateEndomorphismLinearFactor hπ a
theorem

standardLubinTateEndomorphismLinearFactor_constantCoeff

L212 ↗
LubinTate.standardLubinTateEndomorphismLinearFactor_constantCoeff
Documentation

The constant coefficient of the linear factor is the scalar.

Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section FormalFactors
Lean source · statement
theorem standardLubinTateEndomorphismLinearFactor_constantCoeff
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (a : F.valuationSubring) :
    PowerSeries.constantCoeff
        (standardLubinTateEndomorphismLinearFactor hπ a) = a
theorem

standardLubinTateEndomorphismLinearFactor_isUnit

L223 ↗
LubinTate.standardLubinTateEndomorphismLinearFactor_isUnit
Documentation

The linear factor of a unit scalar endomorphism is invertible.

Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section FormalFactors
Lean source · statement
theorem standardLubinTateEndomorphismLinearFactor_isUnit
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (a : F.valuationSubringˣ) :
    IsUnit
      (standardLubinTateEndomorphismLinearFactor hπ
        (a : F.valuationSubring))
instance

standardLubinTatePrimitiveDisplacementCoefficientUniformSpace

L237 ↗
LubinTate.standardLubinTatePrimitiveDisplacementCoefficientUniformSpace
Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
Lean source · statement
instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring
instance

standardLubinTatePrimitiveDisplacementTargetWithIdeal

L242 ↗
LubinTate.standardLubinTatePrimitiveDisplacementTargetWithIdeal
Source context 12 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
Lean source · full declaration
instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
instance

standardLubinTatePrimitiveDisplacementTargetCompleteSpace

L249 ↗
LubinTate.standardLubinTatePrimitiveDisplacementTargetCompleteSpace
Source context 13 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
Lean source · statement
instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
instance

standardLubinTatePrimitiveDisplacementTargetT2Space

L258 ↗
LubinTate.standardLubinTatePrimitiveDisplacementTargetT2Space
Source context 14 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
Lean source · statement
instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
instance

standardLubinTatePrimitiveDisplacementAlgebra

L267 ↗
LubinTate.standardLubinTatePrimitiveDisplacementAlgebra
Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
theorem

hasEval_fin_two

L274 ↗
LubinTate.hasEval_fin_two
Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem hasEval_fin_two
    {R : Type*} [CommRing R] [TopologicalSpace R]
    {x y : R} (hx : PowerSeries.HasEval x)
    (hy : PowerSeries.HasEval y) :
    MvPowerSeries.HasEval (![x, y] : Fin 2 → R)
theorem

standardLubinTateEndomorphismEvalAt_congr_point_forPrimitiveDisplacement

L286 ↗
LubinTate.standardLubinTateEndomorphismEvalAt_congr_point_forPrimitiveDisplacement
Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem
    standardLubinTateEndomorphismEvalAt_congr_point_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x y : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy : x = y) (a : F.valuationSubring) :
    standardLubinTateEndomorphismEvalAt hπ n x hx a =
      standardLubinTateEndomorphismEvalAt hπ n y hy a
theorem

standardLubinTateFormalAdd_sub_left_addVal

L299 ↗
LubinTate.standardLubinTateFormalAdd_sub_left_addVal
Documentation

Ordinary subtraction after standard formal-group addition has the same additive valuation as the added topologically nilpotent point.

Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateFormalAdd_sub_left_addVal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x z :
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) (hz : PowerSeries.HasEval z) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (standardLubinTateFormalAdd hπ n x z - x) =
      IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring z
theorem

standardLubinTateEndomorphismEvalAt_unit_addVal

L353 ↗
LubinTate.standardLubinTateEndomorphismEvalAt_unit_addVal
Documentation

A unit scalar endomorphism preserves normalized additive valuation on every topologically nilpotent point of a finite level.

Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateEndomorphismEvalAt_unit_addVal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) (a : F.valuationSubringˣ) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (standardLubinTateEndomorphismEvalAt hπ n x hx
          (a : F.valuationSubring)) =
      IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring x
theorem

standardLubinTateEndomorphismValue_uniformizer_pow

L383 ↗
LubinTate.standardLubinTateEndomorphismValue_uniformizer_pow
Documentation

The analytic value of [π^k] is the evaluated standard polynomial iterate.

Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateEndomorphismValue_uniformizer_pow
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) :
    standardLubinTateEndomorphismValue hπ n (π ^ k) =
      standardLubinTatePrimitivePointIterateInteger hπ n k
theorem

standardLubinTatePrimitivePointIterateInteger_hasEval

L395 ↗
LubinTate.standardLubinTatePrimitivePointIterateInteger_hasEval
Documentation

Every evaluated standard iterate before the annihilating level is topologically nilpotent.

Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTatePrimitivePointIterateInteger_hasEval
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) :
    PowerSeries.HasEval
      (standardLubinTatePrimitivePointIterateInteger hπ n k)
theorem

exists_unit_mul_uniformizer_pow_of_exactDepth

L405 ↗
LubinTate.exists_unit_mul_uniformizer_pow_of_exactDepth
Documentation

An element in the exact kth principal-unit layer is a unit times π^k.

Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem exists_unit_mul_uniformizer_pow_of_exactDepth
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (a : F.valuationSubringˣ) (k : ℕ)
    (ha :
      a ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF k)
    (hnot :
      a ∉ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (k + 1)) :
    ∃ c : F.valuationSubringˣ,
      (a : F.valuationSubring) - 1 =
        (c : F.valuationSubring) * π ^ k
theorem

standardLubinTateEndomorphismValue_sub_one_addVal_of_exactDepth

L450 ↗
LubinTate.standardLubinTateEndomorphismValue_sub_one_addVal_of_exactDepth
Documentation

Exact principal-unit depth controls the valuation of [a - 1] at the primitive point.

Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateEndomorphismValue_sub_one_addVal_of_exactDepth
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : F.valuationSubringˣ) (k : ℕ)
    (ha :
      a ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF k)
    (hnot :
      a ∉ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (k + 1))
    (hk : k ≤ n) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (standardLubinTateEndomorphismValue hπ n
          ((a : F.valuationSubring) - 1)) =
      (Nat.card F.residueField ^ k : ℕ)
theorem

standardLubinTatePrimitivePointIntegerAction_sub_self_addVal_of_exactDepth

L502 ↗
LubinTate.standardLubinTatePrimitivePointIntegerAction_sub_self_addVal_of_exactDepth
Documentation

If a unit first differs from 1 in principal-unit depth k, its ordinary displacement of the primitive point has valuation exactly q^k.

Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem
    standardLubinTatePrimitivePointIntegerAction_sub_self_addVal_of_exactDepth
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : F.valuationSubringˣ) (k : ℕ)
    (ha :
      a ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF k)
    (hnot :
      a ∉ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (k + 1))
    (hk : k ≤ n) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (standardLubinTatePrimitivePointIntegerAction hπ n a -
          standardLubinTatePrimitivePointInteger hπ n) =
      (Nat.card F.residueField ^ k : ℕ)
theorem

higherPrincipalUnitGroup_mem_of_le

L559 ↗
LubinTate.higherPrincipalUnitGroup_mem_of_le
Documentation

Principal-unit membership is antitone in the depth index.

Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem higherPrincipalUnitGroup_mem_of_le
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (a : F.valuationSubringˣ) {k r : ℕ} (hkr : k ≤ r)
    (ha :
      a ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF r) :
    a ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF k
theorem

mem_higherPrincipalUnitGroup_iff_le_of_sub_eq_unit_mul_uniformizer_pow

L574 ↗
LubinTate.mem_higherPrincipalUnitGroup_iff_le_of_sub_eq_unit_mul_uniformizer_pow
Documentation

If a - 1 is a unit times π^r, then membership in U^k is equivalent to k ≤ r.

Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem
    mem_higherPrincipalUnitGroup_iff_le_of_sub_eq_unit_mul_uniformizer_pow
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (a c : F.valuationSubringˣ) (r k : ℕ)
    (hsub :
      (a : F.valuationSubring) - 1 =
        (c : F.valuationSubring) * π ^ r) :
    a ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF k ↔
      k ≤ r
theorem

standardLubinTatePrimitivePointIntegerAction_sub_self_addVal_ge_iff_mem

L615 ↗
LubinTate.standardLubinTatePrimitivePointIntegerAction_sub_self_addVal_ge_iff_mem
Documentation

At a standard finite level, the valuation threshold q^k detects exactly the kth principal-unit subgroup. The statement includes the identity action, whose displacement has infinite additive valuation.

Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem
    standardLubinTatePrimitivePointIntegerAction_sub_self_addVal_ge_iff_mem
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : F.valuationSubringˣ) (k : ℕ)
    (hk : k ≤ n + 1) :
    ((Nat.card F.residueField ^ k : ℕ) : ℕ∞) ≤
        IsDiscreteValuationRing.addVal
          (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
          (standardLubinTatePrimitivePointIntegerAction hπ n a -
            standardLubinTatePrimitivePointInteger hπ n) ↔
      a ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF k
theorem

standardLubinTatePrimitivePointIntegerAction_sub_self_addVal_ge_iff_mem_of_pow_interval

L698 ↗
LubinTate.standardLubinTatePrimitivePointIntegerAction_sub_self_addVal_ge_iff_mem_of_pow_interval
Documentation

On the interval q^(k-1) - 1 ≤ r ≤ q^k - 1, the lower displacement bound r + 1 detects the kth principal-unit subgroup.

Source context 16 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem
    standardLubinTatePrimitivePointIntegerAction_sub_self_addVal_ge_iff_mem_of_pow_interval
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : F.valuationSubringˣ) (k r : ℕ)
    (hkpos : 1 ≤ k) (hk : k ≤ n + 1)
    (hlower : Nat.card F.residueField ^ (k - 1) ≤ r)
    (hupper : r < Nat.card F.residueField ^ k) :
    (((r + 1 : ℕ) : ℕ∞) ≤
        IsDiscreteValuationRing.addVal
          (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
          (standardLubinTatePrimitivePointIntegerAction hπ n a -
            standardLubinTatePrimitivePointInteger hπ n)) ↔
      a ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF k
instance

standardLubinTateLevelField_finiteDimensional_forPrimitiveDisplacement

L784 ↗
LubinTate.standardLubinTateLevelField_finiteDimensional_forPrimitiveDisplacement
Source context 17 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
section ParameterDisplacement
Lean source · statement
instance
    standardLubinTateLevelField_finiteDimensional_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n)
instance

standardLubinTateLevelField_isGalois_forPrimitiveDisplacement

L790 ↗
LubinTate.standardLubinTateLevelField_isGalois_forPrimitiveDisplacement
Source context 18 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
section ParameterDisplacement
private noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
Lean source · statement
instance
    standardLubinTateLevelField_isGalois_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n)
theorem

standardLubinTateUnitParameterToGal_apply_primitivePointInteger

L799 ↗
LubinTate.standardLubinTateUnitParameterToGal_apply_primitivePointInteger
Documentation

The valuation-ring action of the automorphism attached to a finite unit parameter agrees with the analytic action of its chosen representative on the primitive point.

Source context 19 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
section ParameterDisplacement
private noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
private noncomputable local instance
    standardLubinTateLevelField_isGalois_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n
Lean source · statement
theorem standardLubinTateUnitParameterToGal_apply_primitivePointInteger
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : standardLubinTateUnitParameter F n) :
    valuationSubringAutOfUniqueExtension
        (standardLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
          hπ n)
        (standardLubinTateUnitParameterToGal F hπ n a)
        (standardLubinTatePrimitivePointInteger hπ n) =
      standardLubinTatePrimitivePointIntegerAction hπ n
        (standardLubinTateUnitParameterChosenRepresentative F n a)
theorem

standardLubinTateUnitParameterToGal_displacement_addVal_of_chosenRepresentative_exactDepth

L824 ↗
LubinTate.standardLubinTateUnitParameterToGal_displacement_addVal_of_chosenRepresentative_exactDepth
Documentation

Exact depth of a chosen finite-parameter representative computes the displacement of the corresponding Galois automorphism.

Source context 19 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
section ParameterDisplacement
private noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
private noncomputable local instance
    standardLubinTateLevelField_isGalois_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n
Lean source · statement
theorem
    standardLubinTateUnitParameterToGal_displacement_addVal_of_chosenRepresentative_exactDepth
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : standardLubinTateUnitParameter F n) (k : ℕ)
    (ha :
      standardLubinTateUnitParameterChosenRepresentative F n a ∈
        CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF k)
    (hnot :
      standardLubinTateUnitParameterChosenRepresentative F n a ∉
        CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (k + 1))
    (hk : k ≤ n) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (valuationSubringAutOfUniqueExtension
            (standardLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
              hπ n)
            (standardLubinTateUnitParameterToGal F hπ n a)
            (standardLubinTatePrimitivePointInteger hπ n) -
          standardLubinTatePrimitivePointInteger hπ n) =
      (Nat.card F.residueField ^ k : ℕ)
theorem

standardLubinTateUnitParameterToGal_displacement_addVal_ge_iff_chosenRepresentative_mem

L854 ↗
LubinTate.standardLubinTateUnitParameterToGal_displacement_addVal_ge_iff_chosenRepresentative_mem
Documentation

The q^k displacement threshold for a finite-parameter automorphism is equivalent to its chosen representative belonging to U^k.

Source context 19 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
section ParameterDisplacement
private noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
private noncomputable local instance
    standardLubinTateLevelField_isGalois_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n
Lean source · statement
theorem
    standardLubinTateUnitParameterToGal_displacement_addVal_ge_iff_chosenRepresentative_mem
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : standardLubinTateUnitParameter F n) (k : ℕ)
    (hk : k ≤ n + 1) :
    ((Nat.card F.residueField ^ k : ℕ) : ℕ∞) ≤
        IsDiscreteValuationRing.addVal
          (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
          (valuationSubringAutOfUniqueExtension
              (standardLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
                hπ n)
              (standardLubinTateUnitParameterToGal F hπ n a)
              (standardLubinTatePrimitivePointInteger hπ n) -
            standardLubinTatePrimitivePointInteger hπ n) ↔
      standardLubinTateUnitParameterChosenRepresentative F n a ∈
        CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF k
theorem

standardLubinTateUnitParameterToGal_displacement_addVal_ge_iff_representative_mem_pow_interval

L879 ↗
LubinTate.standardLubinTateUnitParameterToGal_displacement_addVal_ge_iff_representative_mem_pow_interval
Documentation

The power-interval form of the finite-parameter displacement criterion, stated using its chosen representative.

Source context 19 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
section ParameterDisplacement
private noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
private noncomputable local instance
    standardLubinTateLevelField_isGalois_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n
Lean source · statement
theorem
    standardLubinTateUnitParameterToGal_displacement_addVal_ge_iff_representative_mem_pow_interval
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : standardLubinTateUnitParameter F n) (k r : ℕ)
    (hkpos : 1 ≤ k) (hk : k ≤ n + 1)
    (hlower : Nat.card F.residueField ^ (k - 1) ≤ r)
    (hupper : r < Nat.card F.residueField ^ k) :
    (((r + 1 : ℕ) : ℕ∞) ≤
        IsDiscreteValuationRing.addVal
          (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
          (valuationSubringAutOfUniqueExtension
              (standardLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
                hπ n)
              (standardLubinTateUnitParameterToGal F hπ n a)
              (standardLubinTatePrimitivePointInteger hπ n) -
            standardLubinTatePrimitivePointInteger hπ n)) ↔
      standardLubinTateUnitParameterChosenRepresentative F n a ∈
        CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF k
theorem

standardLubinTateGal_displacement_addVal_le_of_ne

L912 ↗
LubinTate.standardLubinTateGal_displacement_addVal_le_of_ne
Documentation

Every nontrivial displacement of the primitive point by a level Galois automorphism has additive valuation at most q ^ n.

Surjectivity of the finite unit-parameter action supplies a representative. If that representative fixed the point, it would lie in U^(n+1). Otherwise its first nontrivial depth is some k ≤ n, where the exact displacement formula is q^k.

Source context 19 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section AnalyticValuation
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveDisplacementAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
section ParameterDisplacement
private noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
private noncomputable local instance
    standardLubinTateLevelField_isGalois_forPrimitiveDisplacement
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n
Lean source · statement
theorem standardLubinTateGal_displacement_addVal_le_of_ne
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (σ : Gal(standardLubinTateLevelField hπ n/K))
    (hne :
      valuationSubringAutOfUniqueExtension
          (standardLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
            hπ n)
          σ (standardLubinTatePrimitivePointInteger hπ n) ≠
        standardLubinTatePrimitivePointInteger hπ n) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (valuationSubringAutOfUniqueExtension
            (standardLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
              hπ n)
            σ (standardLubinTatePrimitivePointInteger hπ n) -
          standardLubinTatePrimitivePointInteger hπ n) ≤
      ((Nat.card F.residueField ^ n : ℕ) : ℕ∞)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.