NYLL
Module

DivisionPolynomial.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.DivisionPolynomial
19 declarations indexed from sourceView source ↗

Module documentation

Standard Lubin--Tate division polynomials

For a local field F and an element π of its valuation ring, this file packages the polynomial

f(X) = X ^ q + π * X,

where q is the cardinality of the residue field. Its compositional iterates and the factors

Qₙ(X) = (f^[n](X)) ^ (q - 1) + π

are defined over the valuation ring itself. These constructions do not use an equal-characteristic model. In particular, they apply unchanged to the standard Lubin--Tate series over a mixed-characteristic local field.

The factorization

f^[n+1](X) = f^[n](X) * Qₙ(X)

is purely polynomial. No assertion about roots, irreducibility, or finite Lubin--Tate extensions is made here.

Imports2
Imported by3

Declarations

def

standardLubinTatePolynomial

L51 ↗
LubinTate.standardLubinTatePolynomial
Documentation

The polynomial X ^ q + π * X underlying the standard Lubin--Tate series.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
def standardLubinTatePolynomial
    (F : LocalField.{u, v} K) (π : F.valuationSubring) :
    Polynomial F.valuationSubring
theorem

standardLubinTatePolynomial_formula

L58 ↗
LubinTate.standardLubinTatePolynomial_formula
Documentation

The defining formula for the standard Lubin--Tate polynomial.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomial_formula
    (F : LocalField.{u, v} K) (π : F.valuationSubring) :
    standardLubinTatePolynomial F π =
      Polynomial.X ^ Nat.card F.residueField +
        Polynomial.C π * Polynomial.X
theorem

standardLubinTatePolynomial_eval

L68 ↗
LubinTate.standardLubinTatePolynomial_eval
Documentation

Evaluation of the standard polynomial has the expected two-term formula.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomial_eval
    (F : LocalField.{u, v} K) (π : F.valuationSubring)
    (x : F.valuationSubring) :
    (standardLubinTatePolynomial F π).eval x =
      x ^ Nat.card F.residueField + π * x
theorem

standardLubinTatePolynomial_toPowerSeries

L78 ↗
LubinTate.standardLubinTatePolynomial_toPowerSeries
Documentation

Coercing the standard polynomial to a power series gives the standard Lubin--Tate power series.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomial_toPowerSeries
    (F : LocalField.{u, v} K) (π : F.valuationSubring) :
    ((standardLubinTatePolynomial F π :
        Polynomial F.valuationSubring) :
      PowerSeries F.valuationSubring) =
        standardLubinTatePowerSeries F π
theorem

standardLubinTatePolynomial_toPowerSeries_eq_series

L90 ↗
LubinTate.standardLubinTatePolynomial_toPowerSeries_eq_series
Documentation

For a uniformizer, coercing the standard polynomial gives the underlying series of the bundled standard Lubin--Tate input.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomial_toPowerSeries_eq_series
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    ((standardLubinTatePolynomial F π :
        Polynomial F.valuationSubring) :
      PowerSeries F.valuationSubring) =
        (standardLubinTateSeries hπ).toPowerSeries
theorem

standardLubinTatePolynomial_natDegree

L101 ↗
LubinTate.standardLubinTatePolynomial_natDegree
Documentation

The standard Lubin--Tate polynomial has degree q.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomial_natDegree
    (F : LocalField.{u, v} K) (π : F.valuationSubring) :
    (standardLubinTatePolynomial F π).natDegree =
      Nat.card F.residueField
theorem

standardLubinTatePolynomial_monic

L117 ↗
LubinTate.standardLubinTatePolynomial_monic
Documentation

The standard Lubin--Tate polynomial is monic.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomial_monic
    (F : LocalField.{u, v} K) (π : F.valuationSubring) :
    (standardLubinTatePolynomial F π).Monic
def

standardLubinTatePolynomialIterate

L132 ↗
LubinTate.standardLubinTatePolynomialIterate
Documentation

The n-fold compositional iterate of the standard polynomial, starting from X.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
def standardLubinTatePolynomialIterate
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    Polynomial F.valuationSubring
theorem

standardLubinTatePolynomialIterate_zero

L139 ↗
LubinTate.standardLubinTatePolynomialIterate_zero
Documentation

The zeroth compositional iterate is X.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomialIterate_zero
    (F : LocalField.{u, v} K) (π : F.valuationSubring) :
    standardLubinTatePolynomialIterate F π 0 = Polynomial.X
theorem

standardLubinTatePolynomialIterate_succ

L146 ↗
LubinTate.standardLubinTatePolynomialIterate_succ
Documentation

A successor iterate is obtained by one further composition with the standard polynomial.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomialIterate_succ
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    standardLubinTatePolynomialIterate F π (n + 1) =
      (standardLubinTatePolynomial F π).comp
        (standardLubinTatePolynomialIterate F π n)
theorem

standardLubinTatePolynomialIterate_natDegree

L156 ↗
LubinTate.standardLubinTatePolynomialIterate_natDegree
Documentation

The n-fold standard compositional iterate has degree q ^ n.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomialIterate_natDegree
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    (standardLubinTatePolynomialIterate F π n).natDegree =
      Nat.card F.residueField ^ n
theorem

standardLubinTatePolynomialIterate_monic

L166 ↗
LubinTate.standardLubinTatePolynomialIterate_monic
Documentation

Every compositional iterate of the standard polynomial is monic.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomialIterate_monic
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    (standardLubinTatePolynomialIterate F π n).Monic
theorem

standardLubinTatePolynomialIterate_eval_zero

L184 ↗
LubinTate.standardLubinTatePolynomialIterate_eval_zero
Documentation

Every standard compositional iterate vanishes at zero.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomialIterate_eval_zero
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    (standardLubinTatePolynomialIterate F π n).eval 0 = 0
def

standardLubinTatePrimitivePolynomial

L199 ↗
LubinTate.standardLubinTatePrimitivePolynomial
Documentation

The primitive quotient polynomial at level n + 1.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
def standardLubinTatePrimitivePolynomial
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    Polynomial F.valuationSubring
theorem

standardLubinTatePrimitivePolynomial_formula

L207 ↗
LubinTate.standardLubinTatePrimitivePolynomial_formula
Documentation

The defining formula for the primitive quotient polynomial.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePrimitivePolynomial_formula
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    standardLubinTatePrimitivePolynomial F π n =
      standardLubinTatePolynomialIterate F π n ^
          (Nat.card F.residueField - 1) +
        Polynomial.C π
theorem

standardLubinTatePrimitivePolynomial_natDegree

L216 ↗
LubinTate.standardLubinTatePrimitivePolynomial_natDegree
Documentation

The primitive quotient polynomial has degree (q - 1) * q ^ n.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePrimitivePolynomial_natDegree
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    (standardLubinTatePrimitivePolynomial F π n).natDegree =
      (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n
theorem

standardLubinTatePrimitivePolynomial_monic

L238 ↗
LubinTate.standardLubinTatePrimitivePolynomial_monic
Documentation

The primitive quotient polynomial is monic.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePrimitivePolynomial_monic
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    (standardLubinTatePrimitivePolynomial F π n).Monic
theorem

standardLubinTatePrimitivePolynomial_coeff_zero

L263 ↗
LubinTate.standardLubinTatePrimitivePolynomial_coeff_zero
Documentation

The constant coefficient of the primitive quotient polynomial is π.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePrimitivePolynomial_coeff_zero
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    (standardLubinTatePrimitivePolynomial F π n).coeff 0 = π
theorem

standardLubinTatePolynomialIterate_succ_factor

L275 ↗
LubinTate.standardLubinTatePolynomialIterate_succ_factor
Documentation

The next compositional iterate is the current iterate times its primitive quotient polynomial.

Source context 6 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
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomialIterate_succ_factor
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    standardLubinTatePolynomialIterate F π (n + 1) =
      standardLubinTatePolynomialIterate F π n *
        standardLubinTatePrimitivePolynomial F π n

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