NYLL
Module

DisplacementValuation.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Ramification.DisplacementValuation
21 declarations indexed from sourceView source ↗

Module documentation

Valuation of primitive-point displacement

This module computes the normalized additive valuation of the displacement of the chosen primitive Lubin--Tate point from the first visible coefficient of the corresponding unit parameter.

Imports3
Imported by3

Declarations

def

equalCharacteristicLubinTateCoefficientInteger

L47 ↗
LubinTate.equalCharacteristicLubinTateCoefficientInteger
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
def equalCharacteristicLubinTateCoefficientInteger
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (c : F.residueField) :
    (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
theorem

equalCharacteristicLubinTateCoefficientInteger_zero

L59 ↗
LubinTate.equalCharacteristicLubinTateCoefficientInteger_zero
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTateCoefficientInteger_zero
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateCoefficientInteger F n 0 = 0
theorem

equalCharacteristicLubinTateCoefficientInteger_coe

L67 ↗
LubinTate.equalCharacteristicLubinTateCoefficientInteger_coe
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTateCoefficientInteger_coe
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (c : F.residueField) :
    (equalCharacteristicLubinTateCoefficientInteger F n c).val =
        algebraMap F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelField F n)
          (algebraMap F.residueField F.residueField⸨X⸩ c)
def

equalCharacteristicLubinTatePiEndInteger

L77 ↗
LubinTate.equalCharacteristicLubinTatePiEndInteger
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
def equalCharacteristicLubinTatePiEndInteger
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ)
    (x :
      (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring) :
    (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
theorem

equalCharacteristicLubinTatePiEndInteger_coe

L91 ↗
LubinTate.equalCharacteristicLubinTatePiEndInteger_coe
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTatePiEndInteger_coe
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ)
    (x :
      (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring) :
    (equalCharacteristicLubinTatePiEndInteger F n x).val =
      equalCharacteristicLubinTateAmbientPiEnd F
        (algebraMap F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelField F n)
          (equalCharacteristicLaurentUniformizer F))
        x.val
def

equalCharacteristicLubinTatePiIterateInteger

L108 ↗
LubinTate.equalCharacteristicLubinTatePiIterateInteger
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · full declaration
def equalCharacteristicLubinTatePiIterateInteger
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    ℕ →
      (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
  | 0 => equalCharacteristicLubinTatePrimitivePointInteger F n
  | i + 1 =>
      equalCharacteristicLubinTatePiEndInteger F n
        (equalCharacteristicLubinTatePiIterateInteger F n i)
theorem

equalCharacteristicLubinTateAmbientPiIterate_succ_left

L119 ↗
LubinTate.equalCharacteristicLubinTateAmbientPiIterate_succ_left
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTateAmbientPiIterate_succ_left
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n i : ℕ) (x : equalCharacteristicLubinTateLevelField F n) :
    equalCharacteristicLubinTateAmbientPiIterate F
        (algebraMap F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelField F n)
          (equalCharacteristicLaurentUniformizer F))
        (i + 1) x =
      equalCharacteristicLubinTateAmbientPiEnd F
          (algebraMap F.residueField⸨X⸩
            (equalCharacteristicLubinTateLevelField F n)
            (equalCharacteristicLaurentUniformizer F))
        (equalCharacteristicLubinTateAmbientPiIterate F
          (algebraMap F.residueField⸨X⸩
            (equalCharacteristicLubinTateLevelField F n)
            (equalCharacteristicLaurentUniformizer F))
          i x)
theorem

equalCharacteristicLubinTatePiIterateInteger_coe

L154 ↗
LubinTate.equalCharacteristicLubinTatePiIterateInteger_coe
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTatePiIterateInteger_coe
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n i : ℕ) :
    (equalCharacteristicLubinTatePiIterateInteger F n i).val =
      equalCharacteristicLubinTateAmbientPiIterate F
        (algebraMap F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelField F n)
          (equalCharacteristicLaurentUniformizer F))
        i (equalCharacteristicLubinTateLevelPowerBasis F n).gen
theorem

equalCharacteristicLubinTateCoefficientInteger_isUnit

L172 ↗
LubinTate.equalCharacteristicLubinTateCoefficientInteger_isUnit
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTateCoefficientInteger_isUnit
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) {c : F.residueField} (hc : c ≠ 0) :
    IsUnit (equalCharacteristicLubinTateCoefficientInteger F n c)
theorem

equalCharacteristicLubinTateCoefficientInteger_addVal

L186 ↗
LubinTate.equalCharacteristicLubinTateCoefficientInteger_addVal
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTateCoefficientInteger_addVal
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) {c : F.residueField} (hc : c ≠ 0) :
    IsDiscreteValuationRing.addVal
        (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
        (equalCharacteristicLubinTateCoefficientInteger F n c) = 0
theorem

equalCharacteristicLubinTatePiIterateInteger_addVal

L196 ↗
LubinTate.equalCharacteristicLubinTatePiIterateInteger_addVal
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTatePiIterateInteger_addVal
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n i : ℕ) (hi : i ≤ n) :
    IsDiscreteValuationRing.addVal
        (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
        (equalCharacteristicLubinTatePiIterateInteger F n i) =
      (Nat.card F.residueField ^ i : ℕ)
def

equalCharacteristicLubinTateBracketInteger

L276 ↗
LubinTate.equalCharacteristicLubinTateBracketInteger
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
def equalCharacteristicLubinTateBracketInteger
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (u : F.residueField⟦X⟧) :
    (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
theorem

equalCharacteristicLubinTateBracketInteger_coe

L287 ↗
LubinTate.equalCharacteristicLubinTateBracketInteger_coe
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTateBracketInteger_coe
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (u : F.residueField⟦X⟧) :
    (equalCharacteristicLubinTateBracketInteger F n u).val =
      equalCharacteristicLubinTateAmbientBracket F
        ((algebraMap F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelField F n)).comp
            (algebraMap F.residueField F.residueField⸨X⸩))
        (algebraMap F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelField F n)
          (equalCharacteristicLaurentUniformizer F))
        (n + 1) u (equalCharacteristicLubinTateLevelPowerBasis F n).gen
theorem

natCast_lt_addVal_finsetSum_of_forall_lt

L333 ↗
LubinTate.natCast_lt_addVal_finsetSum_of_forall_lt
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem natCast_lt_addVal_finsetSum_of_forall_lt
    {R I : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    (c : ℕ) (s : Finset I) (f : I → R)
    (h : ∀ i ∈ s,
      (c : ℕ∞) < IsDiscreteValuationRing.addVal R (f i)) :
    (c : ℕ∞) <
      IsDiscreteValuationRing.addVal R (∑ i ∈ s, f i)
theorem

equalCharacteristicLubinTateBracketInteger_addVal_eq_order

L354 ↗
LubinTate.equalCharacteristicLubinTateBracketInteger_addVal_eq_order
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTateBracketInteger_addVal_eq_order
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (u : F.residueField⟦X⟧)
    (hu : u ≠ 0) (hk : u.order.toNat ≤ n) :
    IsDiscreteValuationRing.addVal
        (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
        (equalCharacteristicLubinTateBracketInteger F n u) =
      (Nat.card F.residueField ^ u.order.toNat : ℕ)
theorem

equalCharacteristicLubinTateUnitParameterSeries_sub_one_order_toNat_le

L444 ↗
LubinTate.equalCharacteristicLubinTateUnitParameterSeries_sub_one_order_toNat_le
Documentation

The first nonzero coefficient of a nontrivial visible parameter occurs at an index at most n.

Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTateUnitParameterSeries_sub_one_order_toNat_le
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n)
    (hu : equalCharacteristicLubinTateUnitParameterSeries F n a - 1 ≠ 0) :
    (equalCharacteristicLubinTateUnitParameterSeries F n a - 1).order.toNat ≤
      n
theorem

equalCharacteristicLubinTateBracketInteger_coe_eq_aeval

L462 ↗
LubinTate.equalCharacteristicLubinTateBracketInteger_coe_eq_aeval
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem equalCharacteristicLubinTateBracketInteger_coe_eq_aeval
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (u : F.residueField⟦X⟧) :
    (equalCharacteristicLubinTateBracketInteger F n u).val =
      Polynomial.aeval (equalCharacteristicLubinTateLevelPowerBasis F n).gen
        (equalCharacteristicLubinTateBracketPolynomial F (n + 1) u)
theorem

equalCharacteristicLubinTatePrimitivePointInteger_displacement_eq_bracketInteger

L484 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePointInteger_displacement_eq_bracketInteger
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem
    equalCharacteristicLubinTatePrimitivePointInteger_displacement_eq_bracketInteger
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ)
    (sigma : Gal((equalCharacteristicLubinTateLevelField F n)/F.residueField⸨X⸩))
    (a : equalCharacteristicLubinTateUnitParameter F n)
    (ha :
      sigma (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
        equalCharacteristicLubinTateLevelBracket F n (n + 1)
          (equalCharacteristicLubinTateUnitParameterSeries F n a)
          (equalCharacteristicLubinTateLevelPowerBasis F n).gen) :
    valuationSubringAutOfUniqueExtension
          (equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
            F n)
          sigma (equalCharacteristicLubinTatePrimitivePointInteger F n) -
        equalCharacteristicLubinTatePrimitivePointInteger F n =
      equalCharacteristicLubinTateBracketInteger F n
        (equalCharacteristicLubinTateUnitParameterSeries F n a - 1)
theorem

equalCharacteristicLubinTatePrimitivePointInteger_displacement_addVal

L509 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePointInteger_displacement_addVal
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem
    equalCharacteristicLubinTatePrimitivePointInteger_displacement_addVal
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ)
    (sigma : Gal((equalCharacteristicLubinTateLevelField F n)/F.residueField⸨X⸩))
    (a : equalCharacteristicLubinTateUnitParameter F n)
    (ha :
      sigma (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
        equalCharacteristicLubinTateLevelBracket F n (n + 1)
          (equalCharacteristicLubinTateUnitParameterSeries F n a)
          (equalCharacteristicLubinTateLevelPowerBasis F n).gen)
    (hu : equalCharacteristicLubinTateUnitParameterSeries F n a - 1 ≠ 0) :
    IsDiscreteValuationRing.addVal
        (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
        (valuationSubringAutOfUniqueExtension
            (equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
              F n)
            sigma (equalCharacteristicLubinTatePrimitivePointInteger F n) -
          equalCharacteristicLubinTatePrimitivePointInteger F n) =
      (Nat.card F.residueField ^
        (equalCharacteristicLubinTateUnitParameterSeries F n a - 1).order.toNat :
          ℕ)
theorem

equalCharacteristicLubinTateUnitParameterSeries_sub_one_ne_zero_of_sigma_ne_one

L543 ↗
LubinTate.equalCharacteristicLubinTateUnitParameterSeries_sub_one_ne_zero_of_sigma_ne_one
Documentation

A nonidentity automorphism has a genuinely nonzero visible coefficient difference from the identity parameter.

Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem
    equalCharacteristicLubinTateUnitParameterSeries_sub_one_ne_zero_of_sigma_ne_one
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ)
    (sigma : Gal((equalCharacteristicLubinTateLevelField F n)/F.residueField⸨X⸩))
    (a : equalCharacteristicLubinTateUnitParameter F n)
    (ha :
      sigma (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
        equalCharacteristicLubinTateLevelBracket F n (n + 1)
          (equalCharacteristicLubinTateUnitParameterSeries F n a)
          (equalCharacteristicLubinTateLevelPowerBasis F n).gen)
    (hsigma : sigma ≠ 1) :
    equalCharacteristicLubinTateUnitParameterSeries F n a - 1 ≠ 0
theorem

equalCharacteristicLubinTatePrimitivePointInteger_displacement_addVal_of_ne_one

L597 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePointInteger_displacement_addVal_of_ne_one
Documentation

If k is the first visible coefficient where a nonidentity Galois parameter differs from 1, then its displacement of the primitive uniformizer has normalized additive valuation exactly q^k.

Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
  equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Lean source · statement
theorem
    equalCharacteristicLubinTatePrimitivePointInteger_displacement_addVal_of_ne_one
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ)
    (sigma : Gal((equalCharacteristicLubinTateLevelField F n)/F.residueField⸨X⸩))
    (a : equalCharacteristicLubinTateUnitParameter F n)
    (ha :
      sigma (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
        equalCharacteristicLubinTateLevelBracket F n (n + 1)
          (equalCharacteristicLubinTateUnitParameterSeries F n a)
          (equalCharacteristicLubinTateLevelPowerBasis F n).gen)
    (hsigma : sigma ≠ 1) :
    IsDiscreteValuationRing.addVal
        (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
        (valuationSubringAutOfUniqueExtension
            (equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
              F n)
            sigma (equalCharacteristicLubinTatePrimitivePointInteger F n) -
          equalCharacteristicLubinTatePrimitivePointInteger F n) =
      (Nat.card F.residueField ^
        (equalCharacteristicLubinTateUnitParameterSeries F n a - 1).order.toNat :
          ℕ)

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