Module

ChangedUniformizer.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.ChangedUniformizer

55 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: changing the equal-characteristic uniformizer

If u is a unit of κ[[T]], then uT is again a uniformizer. This file repeats the mechanical part of the Lubin--Tate construction with

P_{uT}(Y) = Y^q + uT Y.

The primitive level polynomial is monic and Eisenstein at (T), hence irreducible over κ((T)); its simple root extension has degree (q - 1)q^n, and the norm of the negative generator is exactly uT. This is the changed-uniformizer algebra used in the proof of the completed theta-intertwining theorem.

Imports3

Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.NormUniformizer
Mathlib.FieldTheory.IsSepClosed

Imported by6

def

equalCharacteristicChangedIntegralUniformizer

L43 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralUniformizer

Documentation

The changed integral uniformizer uT, for u ∈ κ[[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 equalCharacteristicChangedIntegralUniformizer
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    F.residueField⟦X⟧

def

equalCharacteristicChangedLaurentUniformizer

L49 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizer

Documentation

The changed uniformizer uT in κ((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 equalCharacteristicChangedLaurentUniformizer
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    F.residueField⸨X⸩

def

equalCharacteristicChangedLaurentUnit

L56 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUnit

Documentation

The Laurent-series unit corresponding to the integral unit a.

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 equalCharacteristicChangedLaurentUnit
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    F.residueField⸨X⸩ˣ

theorem

equalCharacteristicChangedLaurentUniformizer_eq_unit_mul

L62 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizer_eq_unit_mul

Documentation

The changed parameter really is the changed parameter uT.

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 equalCharacteristicChangedLaurentUniformizer_eq_unit_mul
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicChangedLaurentUniformizer F a =
      (equalCharacteristicChangedLaurentUnit F a : F.residueField⸨X⸩) *
        equalCharacteristicLaurentUniformizer F

theorem

equalCharacteristicChangedLaurentUniformizer_one

L74 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizer_one

Documentation

Changing the Laurent uniformizer by the unit one leaves it unchanged.

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 equalCharacteristicChangedLaurentUniformizer_one
    (F : LocalField.{u, v} K) :
    equalCharacteristicChangedLaurentUniformizer F 1 =
      equalCharacteristicLaurentUniformizer F

theorem

equalCharacteristicChangedIntegralUniformizer_ne_zero

L82 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralUniformizer_ne_zero

Documentation

A unit multiple of the integral uniformizer 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 equalCharacteristicChangedIntegralUniformizer_ne_zero
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicChangedIntegralUniformizer F a ≠ 0

theorem

equalCharacteristicChangedLaurentUniformizer_ne_zero

L88 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizer_ne_zero

Documentation

The changed Laurent uniformizer 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 equalCharacteristicChangedLaurentUniformizer_ne_zero
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicChangedLaurentUniformizer F a ≠ 0

def

equalCharacteristicChangedIntegralPiPolynomial

L101 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPiPolynomial

Documentation

The integral Lubin--Tate polynomial attached to uT.

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 equalCharacteristicChangedIntegralPiPolynomial
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    Polynomial F.residueField⟦X⟧

theorem

equalCharacteristicChangedIntegralPiPolynomial_monic

L109 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPiPolynomial_monic

Documentation

The changed integral π-polynomial is monic.

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 equalCharacteristicChangedIntegralPiPolynomial_monic
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    (equalCharacteristicChangedIntegralPiPolynomial F a).Monic

theorem

equalCharacteristicChangedIntegralPiPolynomial_natDegree

L120 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPiPolynomial_natDegree

Documentation

The changed integral π-polynomial has degree equal to the residue-field cardinality.

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 equalCharacteristicChangedIntegralPiPolynomial_natDegree
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    (equalCharacteristicChangedIntegralPiPolynomial F a).natDegree =
      Nat.card F.residueField

def

equalCharacteristicChangedIntegralPiPolynomialIterate

L133 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPiPolynomialIterate

Documentation

The compositional iterate of P_{uT} 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 equalCharacteristicChangedIntegralPiPolynomialIterate
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Polynomial F.residueField⟦X⟧

theorem

equalCharacteristicChangedIntegralPiPolynomialIterate_natDegree

L139 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPiPolynomialIterate_natDegree

Documentation

The n-fold changed integral π-polynomial 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 equalCharacteristicChangedIntegralPiPolynomialIterate_natDegree
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedIntegralPiPolynomialIterate F a n).natDegree =
      Nat.card F.residueField ^ n

theorem

equalCharacteristicChangedIntegralPiPolynomialIterate_succ

L149 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPiPolynomialIterate_succ

Documentation

The successor iterate is obtained by one more composition with the changed π-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 equalCharacteristicChangedIntegralPiPolynomialIterate_succ
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedIntegralPiPolynomialIterate F a (n + 1) =
      (equalCharacteristicChangedIntegralPiPolynomial F a).comp
        (equalCharacteristicChangedIntegralPiPolynomialIterate F a n)

theorem

equalCharacteristicChangedIntegralPiPolynomialIterate_monic

L159 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPiPolynomialIterate_monic

Documentation

Every iterate of the changed integral π-polynomial is monic.

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 equalCharacteristicChangedIntegralPiPolynomialIterate_monic
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedIntegralPiPolynomialIterate F a n).Monic

theorem

equalCharacteristicChangedIntegralPiPolynomial_map_constantCoeff

L174 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPiPolynomial_map_constantCoeff

Documentation

Reducing coefficients sends the changed integral π-polynomial to X ^ 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 equalCharacteristicChangedIntegralPiPolynomial_map_constantCoeff
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    (equalCharacteristicChangedIntegralPiPolynomial F a).map
        (PowerSeries.constantCoeff (R := F.residueField)) =
      Polynomial.X ^ Nat.card F.residueField

theorem

equalCharacteristicChangedIntegralPiPolynomialIterate_map_constantCoeff

L183 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPiPolynomialIterate_map_constantCoeff

Documentation

Reducing coefficients sends the n-fold changed π-iterate to X ^ (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 equalCharacteristicChangedIntegralPiPolynomialIterate_map_constantCoeff
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedIntegralPiPolynomialIterate F a n).map
        (PowerSeries.constantCoeff (R := F.residueField)) =
      Polynomial.X ^ (Nat.card F.residueField ^ n)

theorem

equalCharacteristicChangedIntegralPiPolynomialIterate_eval_zero

L199 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPiPolynomialIterate_eval_zero

Documentation

Every changed integral π-iterate vanishes at zero.

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 equalCharacteristicChangedIntegralPiPolynomialIterate_eval_zero
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedIntegralPiPolynomialIterate F a n).eval 0 = 0

def

equalCharacteristicChangedIntegralPrimitivePolynomial

L213 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPrimitivePolynomial

Documentation

The integral primitive level-n+1 polynomial for uT.

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 equalCharacteristicChangedIntegralPrimitivePolynomial
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Polynomial F.residueField⟦X⟧

theorem

equalCharacteristicChangedIntegralPrimitivePolynomial_natDegree

L221 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPrimitivePolynomial_natDegree

Documentation

The changed integral primitive polynomial has 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 equalCharacteristicChangedIntegralPrimitivePolynomial_natDegree
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedIntegralPrimitivePolynomial F a n).natDegree =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n

theorem

equalCharacteristicChangedIntegralPrimitivePolynomial_monic

L241 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPrimitivePolynomial_monic

Documentation

The changed integral primitive polynomial is monic.

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 equalCharacteristicChangedIntegralPrimitivePolynomial_monic
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedIntegralPrimitivePolynomial F a n).Monic

theorem

equalCharacteristicChangedIntegralPrimitivePolynomial_map_constantCoeff

L261 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPrimitivePolynomial_map_constantCoeff

Documentation

Reducing the changed integral primitive polynomial yields the expected monomial.

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 equalCharacteristicChangedIntegralPrimitivePolynomial_map_constantCoeff
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedIntegralPrimitivePolynomial F a n).map
        (PowerSeries.constantCoeff (R := F.residueField)) =
      Polynomial.X ^
        ((Nat.card F.residueField - 1) * Nat.card F.residueField ^ n)

theorem

equalCharacteristicChangedIntegralPrimitivePolynomial_coeff_zero

L273 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPrimitivePolynomial_coeff_zero

Documentation

The constant coefficient of the changed integral primitive polynomial is the changed uniformizer.

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 equalCharacteristicChangedIntegralPrimitivePolynomial_coeff_zero
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedIntegralPrimitivePolynomial F a n).coeff 0 =
      equalCharacteristicChangedIntegralUniformizer F a

theorem

equalCharacteristicChangedIntegralUniformizer_notMem_span_X_sq

L284 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralUniformizer_notMem_span_X_sq

Documentation

The changed integral uniformizer does not lie in the square of the X-adic ideal.

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 equalCharacteristicChangedIntegralUniformizer_notMem_span_X_sq
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicChangedIntegralUniformizer F a ∉
      (Ideal.span ({PowerSeries.X} : Set F.residueField⟦X⟧)) ^ 2

theorem

equalCharacteristicChangedIntegralPrimitivePolynomial_isEisensteinAt

L296 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPrimitivePolynomial_isEisensteinAt

Documentation

The changed primitive polynomial is Eisenstein at (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 equalCharacteristicChangedIntegralPrimitivePolynomial_isEisensteinAt
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedIntegralPrimitivePolynomial F a n).IsEisensteinAt
      (Ideal.span ({PowerSeries.X} : Set F.residueField⟦X⟧))

theorem

equalCharacteristicChangedIntegralPrimitivePolynomial_irreducible

L324 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPrimitivePolynomial_irreducible

Documentation

The changed integral primitive polynomial is irreducible by Eisenstein's criterion.

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 equalCharacteristicChangedIntegralPrimitivePolynomial_irreducible
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Irreducible (equalCharacteristicChangedIntegralPrimitivePolynomial F a n)

def

equalCharacteristicChangedPiPolynomial

L338 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomial

Documentation

The Laurent-series Lubin--Tate polynomial for the changed uniformizer.

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 equalCharacteristicChangedPiPolynomial
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    Polynomial F.residueField⸨X⸩

theorem

equalCharacteristicChangedPiPolynomial_eq

L345 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomial_eq

Documentation

Expands the changed Laurent π-polynomial as X ^ q + π * X.

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 equalCharacteristicChangedPiPolynomial_eq
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicChangedPiPolynomial F a =
      Polynomial.X ^ Nat.card F.residueField +
        Polynomial.C (equalCharacteristicChangedLaurentUniformizer F a) *
          Polynomial.X

theorem

equalCharacteristicChangedPiPolynomial_natDegree

L356 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomial_natDegree

Documentation

The changed Laurent π-polynomial has degree equal to the residue-field cardinality.

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 equalCharacteristicChangedPiPolynomial_natDegree
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    (equalCharacteristicChangedPiPolynomial F a).natDegree =
      Nat.card F.residueField

def

equalCharacteristicChangedPiPolynomialIterate

L365 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomialIterate

Documentation

The compositional iterate of P_{uT} 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 equalCharacteristicChangedPiPolynomialIterate
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Polynomial F.residueField⸨X⸩

theorem

equalCharacteristicChangedPiPolynomialIterate_natDegree

L371 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomialIterate_natDegree

Documentation

The n-fold changed Laurent π-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 equalCharacteristicChangedPiPolynomialIterate_natDegree
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedPiPolynomialIterate F a n).natDegree =
      Nat.card F.residueField ^ n

theorem

equalCharacteristicChangedPiPolynomialIterate_succ

L381 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomialIterate_succ

Documentation

A successor Laurent π-iterate is one further composition.

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 equalCharacteristicChangedPiPolynomialIterate_succ
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedPiPolynomialIterate F a (n + 1) =
      (equalCharacteristicChangedPiPolynomial F a).comp
        (equalCharacteristicChangedPiPolynomialIterate F a n)

theorem

equalCharacteristicChangedIntegralPiPolynomialIterate_map

L391 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedIntegralPiPolynomialIterate_map

Documentation

Base change carries the integral π-iterate to the Laurent π-iterate.

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 equalCharacteristicChangedIntegralPiPolynomialIterate_map
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedIntegralPiPolynomialIterate F a n).map
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩) =
      equalCharacteristicChangedPiPolynomialIterate F a n

def

equalCharacteristicChangedPrimitivePolynomial

L406 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPrimitivePolynomial

Documentation

The Laurent-series primitive polynomial for the changed uniformizer.

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 equalCharacteristicChangedPrimitivePolynomial
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Polynomial F.residueField⸨X⸩

theorem

equalCharacteristicChangedPrimitivePolynomial_eq

L413 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPrimitivePolynomial_eq

Documentation

Expands the changed primitive polynomial using the changed π-iterate.

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 equalCharacteristicChangedPrimitivePolynomial_eq
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedPrimitivePolynomial F a n =
      equalCharacteristicChangedPiPolynomialIterate F a n ^
          (Nat.card F.residueField - 1) +
        Polynomial.C (equalCharacteristicChangedLaurentUniformizer F a)

theorem

equalCharacteristicChangedPrimitivePolynomial_natDegree

L425 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPrimitivePolynomial_natDegree

Documentation

The changed primitive polynomial has 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 equalCharacteristicChangedPrimitivePolynomial_natDegree
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedPrimitivePolynomial F a n).natDegree =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n

theorem

equalCharacteristicChangedPrimitivePolynomial_monic

L434 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPrimitivePolynomial_monic

Documentation

The changed primitive polynomial over the Laurent field is monic.

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 equalCharacteristicChangedPrimitivePolynomial_monic
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedPrimitivePolynomial F a n).Monic

theorem

equalCharacteristicChangedPrimitivePolynomial_irreducible

L440 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPrimitivePolynomial_irreducible

Documentation

The changed primitive polynomial over the Laurent field is irreducible.

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 equalCharacteristicChangedPrimitivePolynomial_irreducible
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Irreducible (equalCharacteristicChangedPrimitivePolynomial F a n)

theorem

equalCharacteristicChangedPrimitivePolynomial_coeff_zero

L449 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPrimitivePolynomial_coeff_zero

Documentation

The changed Laurent uniformizer is the primitive polynomial's constant coefficient.

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 equalCharacteristicChangedPrimitivePolynomial_coeff_zero
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedPrimitivePolynomial F a n).coeff 0 =
      equalCharacteristicChangedLaurentUniformizer F a

theorem

equalCharacteristicChangedPiPolynomial_derivative

L458 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomial_derivative

Documentation

The derivative of the changed π-polynomial is the constant changed uniformizer.

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 equalCharacteristicChangedPiPolynomial_derivative
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    (equalCharacteristicChangedPiPolynomial F a).derivative =
      Polynomial.C (equalCharacteristicChangedLaurentUniformizer F a)

theorem

equalCharacteristicChangedPiPolynomialIterate_derivative

L466 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomialIterate_derivative

Documentation

The derivative of the n-fold changed π-iterate is the nth uniformizer power.

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 equalCharacteristicChangedPiPolynomialIterate_derivative
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedPiPolynomialIterate F a n).derivative =
      Polynomial.C (equalCharacteristicChangedLaurentUniformizer F a ^ n)

theorem

equalCharacteristicChangedPiPolynomialIterate_separable

L479 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomialIterate_separable

Documentation

Every iterate of the changed Laurent π-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 equalCharacteristicChangedPiPolynomialIterate_separable
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedPiPolynomialIterate F a n).Separable

theorem

equalCharacteristicChangedPiPolynomialIterate_succ_factor

L492 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomialIterate_succ_factor

Documentation

The successor π-iterate factors through the current iterate and 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 equalCharacteristicChangedPiPolynomialIterate_succ_factor
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedPiPolynomialIterate F a (n + 1) =
      equalCharacteristicChangedPiPolynomialIterate F a n *
        equalCharacteristicChangedPrimitivePolynomial F a n

theorem

equalCharacteristicChangedPrimitivePolynomial_separable

L509 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPrimitivePolynomial_separable

Documentation

The changed primitive 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 equalCharacteristicChangedPrimitivePolynomial_separable
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedPrimitivePolynomial F a n).Separable

theorem

exists_equalCharacteristicChangedPrimitivePolynomial_root

L519 ↗

LubinTate.EqualCharacteristic.exists_equalCharacteristicChangedPrimitivePolynomial_root

Documentation

The changed primitive polynomial has a root in the 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

theorem exists_equalCharacteristicChangedPrimitivePolynomial_root
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    ∃ x : SeparableClosure F.residueField⸨X⸩,
      ((equalCharacteristicChangedPrimitivePolynomial F a n).map
        (equalCharacteristicSeparableBaseHom F)).IsRoot x

def

chosenEqualCharacteristicChangedPrimitiveRoot

L541 ↗

LubinTate.EqualCharacteristic.chosenEqualCharacteristicChangedPrimitiveRoot

Documentation

A chosen changed-uniformizer primitive level root.

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 chosenEqualCharacteristicChangedPrimitiveRoot
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    SeparableClosure F.residueField⸨X⸩

theorem

chosenEqualCharacteristicChangedPrimitiveRoot_isRoot

L548 ↗

LubinTate.EqualCharacteristic.chosenEqualCharacteristicChangedPrimitiveRoot_isRoot

Documentation

The chosen changed primitive element is a root of the base-changed 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 chosenEqualCharacteristicChangedPrimitiveRoot_isRoot
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    ((equalCharacteristicChangedPrimitivePolynomial F a n).map
      (equalCharacteristicSeparableBaseHom F)).IsRoot
        (chosenEqualCharacteristicChangedPrimitiveRoot F a n)

theorem

chosenEqualCharacteristicChangedPrimitiveRoot_isIntegral

L558 ↗

LubinTate.EqualCharacteristic.chosenEqualCharacteristicChangedPrimitiveRoot_isIntegral

Documentation

The chosen changed primitive root is integral over the Laurent 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 chosenEqualCharacteristicChangedPrimitiveRoot_isIntegral
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    IsIntegral F.residueField⸨X⸩
      (chosenEqualCharacteristicChangedPrimitiveRoot F a n)

theorem

equalCharacteristicChangedPrimitivePolynomial_eq_minpoly

L570 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPrimitivePolynomial_eq_minpoly

Documentation

The changed primitive polynomial is the minimal polynomial of the chosen root.

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 equalCharacteristicChangedPrimitivePolynomial_eq_minpoly
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    equalCharacteristicChangedPrimitivePolynomial F a n =
      minpoly F.residueField⸨X⸩
        (chosenEqualCharacteristicChangedPrimitiveRoot F a n)

def

equalCharacteristicChangedLevelField

L585 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedLevelField

Documentation

The simple level field for the changed uniformizer.

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 equalCharacteristicChangedLevelField
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    IntermediateField F.residueField⸨X⸩
      (SeparableClosure F.residueField⸨X⸩)

theorem

equalCharacteristicChangedLevelField_finiteDimensional

L594 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedLevelField_finiteDimensional

Documentation

The changed Lubin–Tate level field is finite-dimensional over the Laurent 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 equalCharacteristicChangedLevelField_finiteDimensional
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicChangedLevelField F a n)

theorem

equalCharacteristicChangedLevelField_finrank

L603 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedLevelField_finrank

Documentation

The changed level field has 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 equalCharacteristicChangedLevelField_finrank
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    Module.finrank F.residueField⸨X⸩
      (equalCharacteristicChangedLevelField F a n) =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n

def

equalCharacteristicChangedLevelGenerator

L623 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedLevelGenerator

Documentation

The chosen root as a generator of its changed-uniformizer 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

def equalCharacteristicChangedLevelGenerator
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    equalCharacteristicChangedLevelField F a n

theorem

equalCharacteristicChangedLevelGenerator_eq_powerBasis_gen

L631 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedLevelGenerator_eq_powerBasis_gen

Documentation

The chosen changed level generator agrees with the generator of its power basis.

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 equalCharacteristicChangedLevelGenerator_eq_powerBasis_gen
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    equalCharacteristicChangedLevelGenerator F a n =
      (IntermediateField.adjoin.powerBasis
        (chosenEqualCharacteristicChangedPrimitiveRoot_isIntegral F a n)).gen

theorem

changedAlgebraNorm_neg

L644 ↗

LubinTate.EqualCharacteristic.changedAlgebraNorm_neg

Documentation

The norm of a negative element, separated from the changed level field's large concrete type.

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 changedAlgebraNorm_neg
    {R S : Type*} [Field R] [Field S] [Algebra R S] (x : S) :
    Algebra.norm R (-x) = (-1) ^ Module.finrank R S * Algebra.norm R x

theorem

equalCharacteristicChanged_norm_neg_levelGenerator

L652 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChanged_norm_neg_levelGenerator

Documentation

The completed theta-intertwining theorem, changed-uniformizer norm identity: N(-λ_{uT,n+1}) = uT.

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 equalCharacteristicChanged_norm_neg_levelGenerator
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    Algebra.norm F.residueField⸨X⸩
        (-equalCharacteristicChangedLevelGenerator F a n) =
      equalCharacteristicChangedLaurentUniformizer F a

Module documentation

The completed theta-intertwining theorem: changing the equal-characteristic uniformizer

Declarations