Module

CompletedIterates.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.CompletedIterates

4 declarations indexed from sourceView source ↗

Module documentation

Valuations of standard Lubin--Tate iterates at a primitive point

At primitive level n + 1, the i-fold standard Lubin--Tate iterate has normalized additive valuation q ^ i for i ≤ n. The proof uses the two-term formula

f(y) = y ^ q + π y.

The first summand has valuation q ^ (i + 1). The second has strictly larger valuation because the image of the base uniformizer has valuation equal to the totally ramified level degree (q - 1) q ^ n.

Imports1

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.CompletedEvaluation

Imported by2

def

standardLubinTatePrimitivePointIterateInteger

L40 ↗

LubinTate.standardLubinTatePrimitivePointIterateInteger

Documentation

The i-fold standard polynomial iterate, evaluated at the primitive point in the complete level valuation ring.

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

Lean source · statement

def standardLubinTatePrimitivePointIterateInteger
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n i : ℕ) :
    (standardLubinTateLevelCompleteDVF hπ n).valuationSubring

theorem

standardLubinTatePrimitivePointIterateInteger_zero

L52 ↗

LubinTate.standardLubinTatePrimitivePointIterateInteger_zero

Documentation

The zeroth iterate is the primitive point itself.

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

Lean source · statement

theorem standardLubinTatePrimitivePointIterateInteger_zero
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    standardLubinTatePrimitivePointIterateInteger hπ n 0 =
      standardLubinTatePrimitivePointInteger hπ n

theorem

standardLubinTatePrimitivePointIterateInteger_succ

L61 ↗

LubinTate.standardLubinTatePrimitivePointIterateInteger_succ

Documentation

One more iterate is evaluation of y ↦ y ^ q + π y.

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

Lean source · statement

theorem standardLubinTatePrimitivePointIterateInteger_succ
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n i : ℕ) :
    standardLubinTatePrimitivePointIterateInteger hπ n (i + 1) =
      standardLubinTatePrimitivePointIterateInteger hπ n i ^
          Nat.card F.residueField +
        standardLubinTateLevelCoefficientHom hπ n π *
          standardLubinTatePrimitivePointIterateInteger hπ n i

theorem

standardLubinTatePrimitivePointIterateInteger_addVal

L81 ↗

LubinTate.standardLubinTatePrimitivePointIterateInteger_addVal

Documentation

Before the annihilating level, the evaluated iterates have exact normalized additive valuations 1, q, ..., q ^ n.

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

Lean source · statement

theorem standardLubinTatePrimitivePointIterateInteger_addVal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n i : ℕ) (hi : i ≤ n) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (standardLubinTatePrimitivePointIterateInteger hπ n i) =
      (Nat.card F.residueField ^ i : ℕ)

Module documentation

Valuations of standard Lubin--Tate iterates at a primitive point

Declarations

standardLubinTatePrimitivePointIterateInteger

standardLubinTatePrimitivePointIterateInteger_zero

standardLubinTatePrimitivePointIterateInteger_succ

standardLubinTatePrimitivePointIterateInteger_addVal