NYLL
Module

ChangedPolynomialEvaluation.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.ChangedPolynomialEvaluation
4 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: evaluation of changed Lubin--Tate polynomials

This small interface identifies the changed polynomials over k((T)) with their ambient Lubin--Tate endomorphisms. Keeping the evaluation layer separate avoids rebuilding the larger algebraic changed-uniformizer construction when it is used at completed points.

Imports2
Imported by4

Declarations

theorem

equalCharacteristicChangedPiPolynomial_eval₂

L36 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomial_eval₂
Documentation

Evaluation of the changed Lubin--Tate polynomial in any compatible ambient field is the corresponding distinguished endomorphism.

Source context 7 commands

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

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

equalCharacteristicChangedPiPolynomialIterate_eval₂

L50 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomialIterate_eval₂
Documentation

Evaluation commutes with every compositional iterate of the changed Lubin--Tate polynomial.

Source context 7 commands

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

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

equalCharacteristicChangedPrimitivePolynomial_eval₂

L84 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedPrimitivePolynomial_eval₂
Documentation

The changed primitive polynomial evaluates to the defining primitive Lubin--Tate equation in every compatible ambient field.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicChangedPrimitivePolynomial_eval₂
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (φ : F.residueField⸨X⸩ →+* A) (n : ℕ) (x : A) :
    Polynomial.eval₂ φ x
        (equalCharacteristicChangedPrimitivePolynomial F a n) =
      equalCharacteristicLubinTateAmbientPiIterate F
          (φ (equalCharacteristicChangedLaurentUniformizer F a)) n x ^
          (Nat.card F.residueField - 1) +
        φ (equalCharacteristicChangedLaurentUniformizer F a)
theorem

equalCharacteristicChangedPrimitivePolynomial_isRoot_of_primitive

L103 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedPrimitivePolynomial_isRoot_of_primitive
Documentation

A point killed exactly at division level n + 1 is a root of the changed primitive polynomial indexed by n.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicChangedPrimitivePolynomial_isRoot_of_primitive
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (φ : F.residueField⸨X⸩ →+* A) (n : ℕ) (x : A)
    (htors : IsEqualCharacteristicLubinTateAmbientTorsion F
      (φ (equalCharacteristicChangedLaurentUniformizer F a)) (n + 1) x)
    (hprimitive : ¬ IsEqualCharacteristicLubinTateAmbientTorsion F
      (φ (equalCharacteristicChangedLaurentUniformizer F a)) n x) :
    ((equalCharacteristicChangedPrimitivePolynomial F a n).map φ).IsRoot x

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