Module

ChangedPrimitiveEvaluation.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.ChangedPrimitiveEvaluation

4 declarations indexed from sourceView source ↗

Module documentation

Evaluating a changed primitive polynomial at the original primitive point

Let π be a uniformizer, let u be a unit with u - 1 ∈ m^(n+1), and put π' = uπ. The parameter difference π' - π then lies in m^(n+2). At the standard primitive level n + 1, whose ramification index is

d = (q - 1) q^n,

this difference maps into the d(n+2)-th power of the target maximal ideal. The parameter-congruence theorem consequently shows that the changed primitive polynomial evaluated at the original primitive point has additive valuation at least d(n+2).

This is the quantitative algebraic input for the characteristic-independent Krasner comparison of the original and changed finite levels.

Imports8

Imported by2

theorem

standardLubinTateChangedUniformizer_sub_mem_maximalIdeal_pow

L54 ↗

LubinTate.standardLubinTateChangedUniformizer_sub_mem_maximalIdeal_pow

Documentation

A depth-n+1 unit changes a uniformizer only in depth n+2.

Source context 10 commands

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

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

Lean source · statement

theorem standardLubinTateChangedUniformizer_sub_mem_maximalIdeal_pow
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (n + 1)) :
    standardLubinTateChangedUniformizer F π u - π ∈
      F.maximalIdeal ^ (n + 2)

theorem

standardLubinTateChangedUniformizer_map_sub_mem_levelMaximalIdeal_pow

L83 ↗

LubinTate.standardLubinTateChangedUniformizer_map_sub_mem_levelMaximalIdeal_pow

Documentation

In the original standard level, the changed and original parameters remain congruent through target depth d(n+2).

Source context 10 commands

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

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

Lean source · statement

theorem
    standardLubinTateChangedUniformizer_map_sub_mem_levelMaximalIdeal_pow
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (n + 1)) :
    standardLubinTateLevelCoefficientHom hπ n
          (standardLubinTateChangedUniformizer F π u) -
        standardLubinTateLevelCoefficientHom hπ n π ∈
      (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal ^
        (((Nat.card F.residueField - 1) *
          Nat.card F.residueField ^ n) * (n + 2))

theorem

standardLubinTateChangedPrimitivePolynomial_eval_mem_maximalIdeal_pow

L122 ↗

LubinTate.standardLubinTateChangedPrimitivePolynomial_eval_mem_maximalIdeal_pow

Documentation

The changed primitive polynomial, evaluated at the original primitive point, lies in target depth d(n+2).

Source context 10 commands

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

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

Lean source · statement

theorem standardLubinTateChangedPrimitivePolynomial_eval_mem_maximalIdeal_pow
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (n + 1)) :
    Polynomial.eval₂
        (standardLubinTateLevelCoefficientHom hπ n)
        (standardLubinTatePrimitivePointInteger hπ n)
        (standardLubinTatePrimitivePolynomial F
          (standardLubinTateChangedUniformizer F π u) n) ∈
      (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal ^
        (((Nat.card F.residueField - 1) *
          Nat.card F.residueField ^ n) * (n + 2))

theorem

standardLubinTateChangedPrimitivePolynomial_eval_addVal_ge

L163 ↗

LubinTate.standardLubinTateChangedPrimitivePolynomial_eval_addVal_ge

Documentation

Quantitative form of the changed-polynomial evaluation estimate.

Source context 10 commands

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

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

Lean source · statement

theorem standardLubinTateChangedPrimitivePolynomial_eval_addVal_ge
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (n + 1)) :
    ((((Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n) * (n + 2) : ℕ) : ℕ∞) ≤
      IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (Polynomial.eval₂
          (standardLubinTateLevelCoefficientHom hπ n)
          (standardLubinTatePrimitivePointInteger hπ n)
          (standardLubinTatePrimitivePolynomial F
            (standardLubinTateChangedUniformizer F π u) n))

Module documentation

Evaluating a changed primitive polynomial at the original primitive point

Declarations

standardLubinTateChangedUniformizer_sub_mem_maximalIdeal_pow

standardLubinTateChangedUniformizer_map_sub_mem_levelMaximalIdeal_pow

standardLubinTateChangedPrimitivePolynomial_eval_mem_maximalIdeal_pow

standardLubinTateChangedPrimitivePolynomial_eval_addVal_ge