NYLL
Module

DivisionPolynomial.lean

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

Module documentation

The uniformizer norm identity: equal-characteristic Lubin--Tate division polynomials

Let P(Y)=Y^q+TY. Its n-fold compositional iterate has degree q^n. The polynomial

Q_(n+1)(Y) = P^[n](Y)^(q-1) + T

cuts out the primitive level-n+1 division points. Here we construct these polynomials over κ((T)), prove the degree calculation, and choose an actual primitive root in the separable closure.

Imports3
Imported by5

Declarations

instance

equalCharacteristicDivisionBaseCharP

L39 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDivisionBaseCharP
Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
instance equalCharacteristicDivisionBaseCharP
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic] :
    CharP F.residueField⸨X⸩ F.residueCharacteristic
instance

equalCharacteristicDivisionClosureCharP

L47 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDivisionClosureCharP
Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
instance equalCharacteristicDivisionClosureCharP
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic] :
    CharP (SeparableClosure F.residueField⸨X⸩)
      F.residueCharacteristic
def

equalCharacteristicLubinTatePiPolynomial

L58 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiPolynomial
Documentation

The base Lubin--Tate polynomial Y^q + TY over κ((T)).

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTatePiPolynomial
    (F : LocalField.{u, v} K) :
    Polynomial F.residueField⸨X⸩
theorem

equalCharacteristicLaurentUniformizer_ne_zero

L65 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentUniformizer_ne_zero
Documentation

The Laurent-series parameter T is nonzero.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLaurentUniformizer_ne_zero
    (F : LocalField.{u, v} K) :
    equalCharacteristicLaurentUniformizer F ≠ 0
theorem

equalCharacteristicLubinTatePiPolynomial_natDegree

L77 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiPolynomial_natDegree
Documentation

The base Lubin--Tate polynomial has degree q.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiPolynomial_natDegree
    (F : LocalField.{u, v} K) :
    (equalCharacteristicLubinTatePiPolynomial F).natDegree =
      Nat.card F.residueField
def

equalCharacteristicLubinTatePiPolynomialIterate

L96 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiPolynomialIterate
Documentation

The n-fold compositional iterate of the base Lubin--Tate polynomial, starting from Y.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTatePiPolynomialIterate
    (F : LocalField.{u, v} K) (n : ℕ) :
    Polynomial F.residueField⸨X⸩
theorem

equalCharacteristicLubinTatePiPolynomialIterate_natDegree

L102 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiPolynomialIterate_natDegree
Documentation

The n-fold iterate has degree q^n.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiPolynomialIterate_natDegree
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTatePiPolynomialIterate F n).natDegree =
      Nat.card F.residueField ^ n
def

equalCharacteristicLubinTatePrimitivePolynomial

L113 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitivePolynomial
Documentation

The polynomial whose roots are exactly the primitive level-n+1 division points.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTatePrimitivePolynomial
    (F : LocalField.{u, v} K) (n : ℕ) :
    Polynomial F.residueField⸨X⸩
theorem

equalCharacteristicLubinTatePrimitivePolynomial_natDegree

L122 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitivePolynomial_natDegree
Documentation

The primitive level-n+1 polynomial has the expected positive degree (q-1)q^n.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePrimitivePolynomial_natDegree
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTatePrimitivePolynomial F n).natDegree =
      (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n
theorem

equalCharacteristicLubinTatePiPolynomial_eval₂

L144 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiPolynomial_eval₂
Documentation

Evaluation of the base polynomial in any ambient field is the ambient distinguished endomorphism.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiPolynomial_eval₂
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (φ : F.residueField⸨X⸩ →+* A) (x : A) :
    Polynomial.eval₂ φ x (equalCharacteristicLubinTatePiPolynomial F) =
      equalCharacteristicLubinTateAmbientPiEnd F
        (φ (equalCharacteristicLaurentUniformizer F)) x
theorem

equalCharacteristicLubinTateAmbientPiIterate_eq_function_iterate

L157 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientPiIterate_eq_function_iterate
Documentation

The additive-endomorphism iterate agrees with ordinary function iteration.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · full declaration
theorem equalCharacteristicLubinTateAmbientPiIterate_eq_function_iterate
    (F : LocalField.{u, v} K)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (t : A) (n : ℕ) (x : A) :
    equalCharacteristicLubinTateAmbientPiIterate F t n x =
      (fun y : A ↦ equalCharacteristicLubinTateAmbientPiEnd F t y)^[n] x := by
  induction n generalizing x with
  | zero => simp [equalCharacteristicLubinTateAmbientPiIterate_zero]
  | succ n ih =>
      rw [equalCharacteristicLubinTateAmbientPiIterate_succ,
        Function.iterate_succ_apply, ih]
theorem

equalCharacteristicLubinTatePiPolynomialIterate_eval₂

L171 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiPolynomialIterate_eval₂
Documentation

Evaluation of the compositional division polynomial is the actual ambient iterate of e.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiPolynomialIterate_eval₂
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (φ : F.residueField⸨X⸩ →+* A) (n : ℕ) (x : A) :
    Polynomial.eval₂ φ x
        (equalCharacteristicLubinTatePiPolynomialIterate F n) =
      equalCharacteristicLubinTateAmbientPiIterate F
        (φ (equalCharacteristicLaurentUniformizer F)) n x
theorem

residueField_natCard_cast_eq_zero

L204 ↗
LubinTate.EqualCharacteristic.residueField_natCard_cast_eq_zero
Documentation

The residue-field cardinality is zero in the Laurent-series base field.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem residueField_natCard_cast_eq_zero
    (F : LocalField.{u, v} K) :
    (Nat.card F.residueField : F.residueField⸨X⸩) = 0
theorem

equalCharacteristicLubinTatePiPolynomial_derivative

L215 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiPolynomial_derivative
Documentation

The derivative of Y^q+TY is the nonzero constant T.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiPolynomial_derivative
    (F : LocalField.{u, v} K) :
    (equalCharacteristicLubinTatePiPolynomial F).derivative =
      Polynomial.C (equalCharacteristicLaurentUniformizer F)
theorem

equalCharacteristicLubinTatePiPolynomialIterate_succ

L223 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiPolynomialIterate_succ
Documentation

Recursive description of the compositional iterates.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiPolynomialIterate_succ
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicLubinTatePiPolynomialIterate F (n + 1) =
      (equalCharacteristicLubinTatePiPolynomial F).comp
        (equalCharacteristicLubinTatePiPolynomialIterate F n)
theorem

equalCharacteristicLubinTatePiPolynomialIterate_derivative

L234 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiPolynomialIterate_derivative
Documentation

The derivative of the n-fold division polynomial is the nonzero constant T^n.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiPolynomialIterate_derivative
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTatePiPolynomialIterate F n).derivative =
      Polynomial.C (equalCharacteristicLaurentUniformizer F ^ n)
theorem

equalCharacteristicLubinTatePiPolynomialIterate_separable

L248 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiPolynomialIterate_separable
Documentation

Every iterated division polynomial is separable.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiPolynomialIterate_separable
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTatePiPolynomialIterate F n).Separable
theorem

equalCharacteristicLubinTatePiPolynomialIterate_succ_factor

L262 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiPolynomialIterate_succ_factor
Documentation

The next division polynomial factors as the preceding one times the primitive factor.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiPolynomialIterate_succ_factor
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicLubinTatePiPolynomialIterate F (n + 1) =
      equalCharacteristicLubinTatePiPolynomialIterate F n *
        equalCharacteristicLubinTatePrimitivePolynomial F n
theorem

equalCharacteristicLubinTatePrimitivePolynomial_separable

L280 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitivePolynomial_separable
Documentation

The primitive factor is separable because it divides the next separable division polynomial.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePrimitivePolynomial_separable
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTatePrimitivePolynomial F n).Separable
def

equalCharacteristicSeparableBaseHom

L290 ↗
LubinTate.EqualCharacteristic.equalCharacteristicSeparableBaseHom
Documentation

The canonical base embedding into the chosen separable closure.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · full declaration
def equalCharacteristicSeparableBaseHom
    (F : LocalField.{u, v} K) :
    F.residueField⸨X⸩ →+* SeparableClosure F.residueField⸨X⸩ where
  toFun x :=
    ⟨algebraMap F.residueField⸨X⸩
        (AlgebraicClosure F.residueField⸨X⸩) x,
      (separableClosure F.residueField⸨X⸩
        (AlgebraicClosure F.residueField⸨X⸩)).algebraMap_mem x⟩
  map_zero' := by
    apply Subtype.ext
    exact (algebraMap F.residueField⸨X⸩
      (AlgebraicClosure F.residueField⸨X⸩)).map_zero
  map_one' := by
    apply Subtype.ext
    exact (algebraMap F.residueField⸨X⸩
      (AlgebraicClosure F.residueField⸨X⸩)).map_one
  map_add' x y := by
    apply Subtype.ext
    exact (algebraMap F.residueField⸨X⸩
      (AlgebraicClosure F.residueField⸨X⸩)).map_add x y
  map_mul' x y := by
    apply Subtype.ext
    exact (algebraMap F.residueField⸨X⸩
      (AlgebraicClosure F.residueField⸨X⸩)).map_mul x y
def

equalCharacteristicSeparableCoefficientHom

L317 ↗
LubinTate.EqualCharacteristic.equalCharacteristicSeparableCoefficientHom
Documentation

The coefficient embedding of the residue field into the chosen separable closure of κ((T)).

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicSeparableCoefficientHom
    (F : LocalField.{u, v} K) :
    F.residueField →+* SeparableClosure F.residueField⸨X⸩
def

equalCharacteristicSeparableUniformizer

L324 ↗
LubinTate.EqualCharacteristic.equalCharacteristicSeparableUniformizer
Documentation

The image of T in the chosen separable closure.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicSeparableUniformizer
    (F : LocalField.{u, v} K) :
    SeparableClosure F.residueField⸨X⸩
theorem

exists_equalCharacteristicLubinTatePrimitivePolynomial_root

L333 ↗
LubinTate.EqualCharacteristic.exists_equalCharacteristicLubinTatePrimitivePolynomial_root
Documentation

A primitive level-n+1 division polynomial has a root in the separable closure. Separability of this polynomial is established below before the root is used to define the level field.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem exists_equalCharacteristicLubinTatePrimitivePolynomial_root
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    ∃ x : SeparableClosure F.residueField⸨X⸩,
      ((equalCharacteristicLubinTatePrimitivePolynomial F n).map
        (equalCharacteristicSeparableBaseHom F)).IsRoot x

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