NYLL
Module

CompletedScalarEndomorphism.lean

Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.CompletedScalarEndomorphism
29 declarations indexed from sourceView source ↗

Module documentation

Completed standard and multiplicative scalar endomorphisms

This module extends the standard-to-multiplicative comparison and scalar endomorphisms to the completed unramified Witt ring. It proves the genuine composition, torsion, and injectivity identities for their analytic actions.

Imports7
Imported by3

Declarations

def

padicCompletedStandardToMultiplicativeIntertwiner

L45 ↗
LubinTate.padicCompletedStandardToMultiplicativeIntertwiner
Documentation

The standard-to-multiplicative intertwiner after extending its ℚ_p-integral coefficients to the completed unramified Witt ring.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
def padicCompletedStandardToMultiplicativeIntertwiner
    (p : ℕ) [Fact p.Prime] :
    PowerSeries (padicCompletedUnramifiedWittRing p)
theorem

padicCompletedStandardToMultiplicativeIntertwiner_frobenius

L55 ↗
LubinTate.padicCompletedStandardToMultiplicativeIntertwiner_frobenius
Documentation

Witt Frobenius fixes the completed standard-to-multiplicative intertwiner because all of its coefficients descend from the p-adic valuation ring.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardToMultiplicativeIntertwiner_frobenius
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.map WittVector.frobenius
        (padicCompletedStandardToMultiplicativeIntertwiner p) =
      padicCompletedStandardToMultiplicativeIntertwiner p
theorem

padicCompletedStandardToMultiplicativeIntertwiner_constantCoeff

L68 ↗
LubinTate.padicCompletedStandardToMultiplicativeIntertwiner_constantCoeff
Documentation

The completed standard-to-multiplicative intertwiner has zero constant coefficient.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardToMultiplicativeIntertwiner_constantCoeff
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.constantCoeff
        (padicCompletedStandardToMultiplicativeIntertwiner p) = 0
theorem

padicCompletedStandardToMultiplicativeIntertwiner_hasSubst

L82 ↗
LubinTate.padicCompletedStandardToMultiplicativeIntertwiner_hasSubst
Documentation

The completed standard-to-multiplicative intertwiner admits formal substitution and convergent evaluation at topologically nilpotent points.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardToMultiplicativeIntertwiner_hasSubst
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.HasSubst
      (padicCompletedStandardToMultiplicativeIntertwiner p)
theorem

padicCompletedStandardToMultiplicativeIntertwiner_eval_injective

L91 ↗
LubinTate.padicCompletedStandardToMultiplicativeIntertwiner_eval_injective
Documentation

Evaluation of the completed standard-to-multiplicative comparison is injective on topologically nilpotent completed-level integers.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardToMultiplicativeIntertwiner_eval_injective
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    {x y : (padicCompletedLevelCompleteDVF p n).valuationSubring}
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy :
      padicCompletedLevelPowerSeriesEval p n x hx
          (padicCompletedStandardToMultiplicativeIntertwiner p) =
        padicCompletedLevelPowerSeriesEval p n y hy
          (padicCompletedStandardToMultiplicativeIntertwiner p)) :
    x = y
def

padicCompletedStandardScalarEndomorphism

L114 ↗
LubinTate.padicCompletedStandardScalarEndomorphism
Documentation

A standard p-adic Lubin--Tate scalar endomorphism after extending its coefficients to the completed unramified Witt ring.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
def padicCompletedStandardScalarEndomorphism
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries (padicCompletedUnramifiedWittRing p)
theorem

padicCompletedStandardScalarEndomorphism_constantCoeff

L125 ↗
LubinTate.padicCompletedStandardScalarEndomorphism_constantCoeff
Documentation

Completed standard scalar endomorphisms have zero constant coefficient.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardScalarEndomorphism_constantCoeff
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.constantCoeff
        (padicCompletedStandardScalarEndomorphism p a) =
      0
theorem

padicCompletedStandardScalarEndomorphism_hasSubst

L144 ↗
LubinTate.padicCompletedStandardScalarEndomorphism_hasSubst
Documentation

Completed standard scalar endomorphisms support formal substitution.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardScalarEndomorphism_hasSubst
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.HasSubst
      (padicCompletedStandardScalarEndomorphism p a)
theorem

padicCompletedStandardScalarEndomorphism_mul

L154 ↗
LubinTate.padicCompletedStandardScalarEndomorphism_mul
Documentation

Multiplication of standard p-adic scalars is composition after completed coefficient extension.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardScalarEndomorphism_mul
    (p : ℕ) [Fact p.Prime]
    (a b : (padicLocalField p).valuationSubring) :
    padicCompletedStandardScalarEndomorphism p (a * b) =
      PowerSeries.subst
        (padicCompletedStandardScalarEndomorphism p b)
        (padicCompletedStandardScalarEndomorphism p a)
theorem

padicCompletedStandardToMultiplicativeIntertwiner_endomorphism

L190 ↗
LubinTate.padicCompletedStandardToMultiplicativeIntertwiner_endomorphism
Documentation

The completed standard-to-multiplicative comparison intertwines the actual completed scalar endomorphisms.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem
    padicCompletedStandardToMultiplicativeIntertwiner_endomorphism
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.subst
        (padicCompletedStandardScalarEndomorphism p a)
        (padicCompletedStandardToMultiplicativeIntertwiner p) =
      PowerSeries.subst
        (padicCompletedStandardToMultiplicativeIntertwiner p)
        (padicCompletedMultiplicativeScalarEndomorphism p a)
def

padicCompletedStandardScalarEndomorphismValue

L244 ↗
LubinTate.padicCompletedStandardScalarEndomorphismValue
Documentation

Analytic action of a completed standard scalar endomorphism on a topologically nilpotent point.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
def padicCompletedStandardScalarEndomorphismValue
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a : (padicLocalField p).valuationSubring) :
    (padicCompletedLevelCompleteDVF p n).valuationSubring
theorem

padicCompletedStandardScalarEndomorphismValue_hasEval

L255 ↗
LubinTate.padicCompletedStandardScalarEndomorphismValue_hasEval
Documentation

A completed standard scalar value remains a convergent evaluation point.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardScalarEndomorphismValue_hasEval
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.HasEval
      (padicCompletedStandardScalarEndomorphismValue p n x hx a)
theorem

padicCompletedStandardScalarEndomorphismValue_mul

L268 ↗
LubinTate.padicCompletedStandardScalarEndomorphismValue_mul
Documentation

Multiplication of standard scalars is composition of their completed analytic actions.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardScalarEndomorphismValue_mul
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a b : (padicLocalField p).valuationSubring) :
    padicCompletedStandardScalarEndomorphismValue p n x hx (a * b) =
      padicCompletedStandardScalarEndomorphismValue p n
        (padicCompletedStandardScalarEndomorphismValue p n x hx b)
        (padicCompletedStandardScalarEndomorphismValue_hasEval
          p n x hx b) a
theorem

padicCompletedStandardScalarEndomorphism_one

L291 ↗
LubinTate.padicCompletedStandardScalarEndomorphism_one
Documentation

The scalar 1 acts by the identity series after completed coefficient extension.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardScalarEndomorphism_one
    (p : ℕ) [Fact p.Prime] :
    padicCompletedStandardScalarEndomorphism p 1 =
      PowerSeries.X
theorem

padicCompletedStandardScalarEndomorphism_uniformizer

L303 ↗
LubinTate.padicCompletedStandardScalarEndomorphism_uniformizer
Documentation

The standard uniformizer acts by the defining standard Lubin--Tate series after completed coefficient extension.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardScalarEndomorphism_uniformizer
    (p : ℕ) [Fact p.Prime] :
    padicCompletedStandardScalarEndomorphism p
        (padicIntEquivValuationSubring p (p : ℤ_[p])) =
      PowerSeries.map
        (padicValuationSubringToCompletedUnramifiedWittRing p)
        (standardLubinTateSeries
          (padicMultiplicativeLubinTateSeries_isUniformizer p)
          ).toPowerSeries
theorem

padicCompletedStandardScalarEndomorphismValue_one

L319 ↗
LubinTate.padicCompletedStandardScalarEndomorphismValue_one
Documentation

The completed analytic action of scalar 1 fixes its input.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardScalarEndomorphismValue_one
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    padicCompletedStandardScalarEndomorphismValue p n x hx 1 =
      x
theorem

padicCompletedStandardScalarEndomorphismValue_zero

L330 ↗
LubinTate.padicCompletedStandardScalarEndomorphismValue_zero
Documentation

Every completed standard scalar endomorphism fixes the zero point.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardScalarEndomorphismValue_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : (padicLocalField p).valuationSubring) :
    padicCompletedStandardScalarEndomorphismValue p n
        0 PowerSeries.HasEval.zero a =
      0
theorem

padicCompletedLevelPowerSeriesEval_map_polynomial

L347 ↗
LubinTate.padicCompletedLevelPowerSeriesEval_map_polynomial
Documentation

Evaluating a coefficient-extended polynomial as a completed power series agrees with integral polynomial evaluation.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedLevelPowerSeriesEval_map_polynomial
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (P : Polynomial (padicLocalField p).valuationSubring) :
    padicCompletedLevelPowerSeriesEval p n x hx
        (PowerSeries.map
          (padicValuationSubringToCompletedUnramifiedWittRing p)
          (P : PowerSeries (padicLocalField p).valuationSubring)) =
      Polynomial.eval₂
        (padicCompletedLevelPadicIntegerCoefficientHom p n) x P
theorem

padicCompletedStandardScalarEndomorphismValue_uniformizer_pow

L365 ↗
LubinTate.padicCompletedStandardScalarEndomorphismValue_uniformizer_pow
Documentation

Evaluating the scalar π ^ r on any completed-level nilpotent point is evaluation of the r-fold standard division-polynomial iterate.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardScalarEndomorphismValue_uniformizer_pow
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) (r : ℕ) :
    padicCompletedStandardScalarEndomorphismValue p n x hx
        ((padicIntEquivValuationSubring p (p : ℤ_[p])) ^ r) =
      Polynomial.eval₂
        (padicCompletedLevelPadicIntegerCoefficientHom p n) x
        (standardLubinTatePolynomialIterate
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) r)
def

padicCompletedMultiplicativeScalarEndomorphismValue

L403 ↗
LubinTate.padicCompletedMultiplicativeScalarEndomorphismValue
Documentation

Analytic action of a completed multiplicative scalar endomorphism.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
def padicCompletedMultiplicativeScalarEndomorphismValue
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a : (padicLocalField p).valuationSubring) :
    (padicCompletedLevelCompleteDVF p n).valuationSubring
theorem

padicCompletedMultiplicativeScalarEndomorphismValue_hasEval

L414 ↗
LubinTate.padicCompletedMultiplicativeScalarEndomorphismValue_hasEval
Documentation

A completed multiplicative scalar value remains a convergent evaluation point.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedMultiplicativeScalarEndomorphismValue_hasEval
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.HasEval
      (padicCompletedMultiplicativeScalarEndomorphismValue
        p n x hx a)
theorem

padicCompletedMultiplicativeScalarEndomorphismValue_mul

L428 ↗
LubinTate.padicCompletedMultiplicativeScalarEndomorphismValue_mul
Documentation

Multiplication of multiplicative scalars is composition of their completed analytic actions.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedMultiplicativeScalarEndomorphismValue_mul
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a b : (padicLocalField p).valuationSubring) :
    padicCompletedMultiplicativeScalarEndomorphismValue
        p n x hx (a * b) =
      padicCompletedMultiplicativeScalarEndomorphismValue p n
        (padicCompletedMultiplicativeScalarEndomorphismValue
          p n x hx b)
        (padicCompletedMultiplicativeScalarEndomorphismValue_hasEval
          p n x hx b) a
theorem

padicCompletedMultiplicativeScalarEndomorphismValue_zero

L452 ↗
LubinTate.padicCompletedMultiplicativeScalarEndomorphismValue_zero
Documentation

Every completed multiplicative scalar endomorphism fixes the zero point.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedMultiplicativeScalarEndomorphismValue_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : (padicLocalField p).valuationSubring) :
    padicCompletedMultiplicativeScalarEndomorphismValue p n
        0 PowerSeries.HasEval.zero a =
      0
theorem

padicCompletedMultiplicativeScalarEndomorphismValue_unit_injective

L470 ↗
LubinTate.padicCompletedMultiplicativeScalarEndomorphismValue_unit_injective
Documentation

A p-adic unit scalar acts injectively on all topologically nilpotent completed-level integers.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem
    padicCompletedMultiplicativeScalarEndomorphismValue_unit_injective
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    {x y : (padicCompletedLevelCompleteDVF p n).valuationSubring}
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy :
      padicCompletedMultiplicativeScalarEndomorphismValue p n x hx
          (u : (padicLocalField p).valuationSubring) =
        padicCompletedMultiplicativeScalarEndomorphismValue p n y hy
          (u : (padicLocalField p).valuationSubring)) :
    x = y
theorem

padicCompletedMultiplicativeScalarEndomorphismValue_one

L500 ↗
LubinTate.padicCompletedMultiplicativeScalarEndomorphismValue_one
Documentation

The scalar-one completed multiplicative endomorphism fixes every topologically nilpotent completed-level integer.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedMultiplicativeScalarEndomorphismValue_one
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    padicCompletedMultiplicativeScalarEndomorphismValue p n x hx 1 =
      x
theorem

padicCompletedMultiplicativeScalarEndomorphismValue_unit_after_inverse

L519 ↗
LubinTate.padicCompletedMultiplicativeScalarEndomorphismValue_unit_after_inverse
Documentation

Acting first by the inverse of a p-adic unit and then by the unit itself recovers every topologically nilpotent completed-level integer.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem
    padicCompletedMultiplicativeScalarEndomorphismValue_unit_after_inverse
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (u : (padicLocalField p).valuationSubringˣ) :
    padicCompletedMultiplicativeScalarEndomorphismValue p n
        (padicCompletedMultiplicativeScalarEndomorphismValue p n x hx
          ((u⁻¹ : (padicLocalField p).valuationSubringˣ) :
            (padicLocalField p).valuationSubring))
        (padicCompletedMultiplicativeScalarEndomorphismValue_hasEval
          p n x hx
          ((u⁻¹ : (padicLocalField p).valuationSubringˣ) :
            (padicLocalField p).valuationSubring))
        (u : (padicLocalField p).valuationSubring) =
      x
theorem

padicCompletedStandardToMultiplicativeIntertwiner_eval_endomorphism

L557 ↗
LubinTate.padicCompletedStandardToMultiplicativeIntertwiner_eval_endomorphism
Documentation

Completed analytic evaluation of the standard-to-multiplicative comparison carries every standard scalar action to the actual multiplicative scalar action.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem
    padicCompletedStandardToMultiplicativeIntertwiner_eval_endomorphism
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a : (padicLocalField p).valuationSubring) :
    padicCompletedLevelPowerSeriesEval p n
        (padicCompletedStandardScalarEndomorphismValue p n x hx a)
        (padicCompletedStandardScalarEndomorphismValue_hasEval
          p n x hx a)
        (padicCompletedStandardToMultiplicativeIntertwiner p) =
      padicCompletedMultiplicativeScalarEndomorphismValue p n
        (padicCompletedLevelPowerSeriesEval p n x hx
          (padicCompletedStandardToMultiplicativeIntertwiner p))
        (padicCompletedLevelPowerSeriesEval_hasEval p n x hx
          (padicCompletedStandardToMultiplicativeIntertwiner p)
          (padicCompletedStandardToMultiplicativeIntertwiner_hasSubst p))
        a
theorem

padicCompletedStandardScalarEndomorphismValue_unit_injective

L609 ↗
LubinTate.padicCompletedStandardScalarEndomorphismValue_unit_injective
Documentation

A p-adic unit scalar acts injectively through the completed standard Lubin--Tate endomorphism on all topologically nilpotent completed-level integers.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem
    padicCompletedStandardScalarEndomorphismValue_unit_injective
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    {x y : (padicCompletedLevelCompleteDVF p n).valuationSubring}
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy :
      padicCompletedStandardScalarEndomorphismValue p n x hx
          (u : (padicLocalField p).valuationSubring) =
        padicCompletedStandardScalarEndomorphismValue p n y hy
          (u : (padicLocalField p).valuationSubring)) :
    x = y
theorem

padicCompletedStandardToMultiplicativeIntertwiner_eval_zero

L676 ↗
LubinTate.padicCompletedStandardToMultiplicativeIntertwiner_eval_zero
Documentation

The completed standard-to-multiplicative comparison evaluates to zero at the zero point.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem padicCompletedStandardToMultiplicativeIntertwiner_eval_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    padicCompletedLevelPowerSeriesEval p n
        0 PowerSeries.HasEval.zero
        (padicCompletedStandardToMultiplicativeIntertwiner p) =
      0

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