NYLL
Module

FiniteLevelEvaluation.lean

Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.FiniteLevelEvaluation
13 declarations indexed from sourceView source ↗

Module documentation

Finite-level evaluation of the p-adic multiplicative comparison

This module evaluates the standard-to-multiplicative Lubin--Tate comparison on topologically nilpotent integers in a standard finite level. It proves the functional equation, compatibility with scalar endomorphisms, the inverse comparison identity, and injectivity of the evaluated comparison.

Imports3
Imported by3

Declarations

instance

padicMultiplicativeLevelCoefficientUniformSpace

L37 ↗
LubinTate.padicMultiplicativeLevelCoefficientUniformSpace
Documentation

The discrete coefficient uniformity used for finite-level analytic evaluation.

Source context 9 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
Lean source · statement
instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring
instance

padicMultiplicativeLevelTargetWithIdeal

L44 ↗
LubinTate.padicMultiplicativeLevelTargetWithIdeal
Documentation

The maximal-ideal adic structure on a standard finite Lubin--Tate level.

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
Lean source · full declaration
instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
instance

padicMultiplicativeLevelTargetCompleteSpace

L53 ↗
LubinTate.padicMultiplicativeLevelTargetCompleteSpace
Documentation

Completeness of the standard finite-level valuation ring for its adic topology.

Source context 11 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
/-- The maximal-ideal adic structure on a standard finite Lubin--Tate level. -/
noncomputable local instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
Lean source · statement
instance
    padicMultiplicativeLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
instance

padicMultiplicativeLevelTargetT2Space

L64 ↗
LubinTate.padicMultiplicativeLevelTargetT2Space
Documentation

Separatedness of the standard finite-level valuation ring for its adic topology.

Source context 12 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
/-- The maximal-ideal adic structure on a standard finite Lubin--Tate level. -/
noncomputable local instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
/-- Completeness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
Lean source · statement
instance
    padicMultiplicativeLevelTargetT2Space
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
instance

padicMultiplicativeLevelTargetTopologicalSpace

L77 ↗
LubinTate.padicMultiplicativeLevelTargetTopologicalSpace
Documentation

The specialized level uses the same maximal-ideal adic topology as the generic evaluator.

Source context 14 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
/-- The maximal-ideal adic structure on a standard finite Lubin--Tate level. -/
noncomputable local instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
/-- Completeness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetT2Space
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
section PadicLevelTopology
Lean source · statement
instance
    padicMultiplicativeLevelTargetTopologicalSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    TopologicalSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring
def

padicMultiplicativePrimitivePoint

L92 ↗
LubinTate.padicMultiplicativePrimitivePoint
Documentation

Evaluation of the standard-to-multiplicative comparison at the chosen standard primitive point of level n + 1.

Source context 15 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
/-- The maximal-ideal adic structure on a standard finite Lubin--Tate level. -/
noncomputable local instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
/-- Completeness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetT2Space
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
section PadicLevelTopology
/-- The specialized level uses the same maximal-ideal adic topology as the generic evaluator. -/
noncomputable local instance
    padicMultiplicativeLevelTargetTopologicalSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    TopologicalSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring :=
  @WithIdeal.instTopologicalSpace _ _
    (padicMultiplicativeLevelTargetWithIdeal
      (F := padicLocalField p)
      (π := show (padicLocalField p).valuationSubring from
        padicIntEquivValuationSubring p (p : ℤ_[p]))
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)
Lean source · statement
def padicMultiplicativePrimitivePoint
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring
theorem

padicMultiplicativePrimitivePoint_hasEval

L101 ↗
LubinTate.padicMultiplicativePrimitivePoint_hasEval
Documentation

The evaluated multiplicative point is topologically nilpotent.

Source context 15 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
/-- The maximal-ideal adic structure on a standard finite Lubin--Tate level. -/
noncomputable local instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
/-- Completeness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetT2Space
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
section PadicLevelTopology
/-- The specialized level uses the same maximal-ideal adic topology as the generic evaluator. -/
noncomputable local instance
    padicMultiplicativeLevelTargetTopologicalSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    TopologicalSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring :=
  @WithIdeal.instTopologicalSpace _ _
    (padicMultiplicativeLevelTargetWithIdeal
      (F := padicLocalField p)
      (π := show (padicLocalField p).valuationSubring from
        padicIntEquivValuationSubring p (p : ℤ_[p]))
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)
Lean source · statement
theorem padicMultiplicativePrimitivePoint_hasEval
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    PowerSeries.HasEval (padicMultiplicativePrimitivePoint p n)
theorem

padicMultiplicativeLubinTateSeries_eval

L116 ↗
LubinTate.padicMultiplicativeLubinTateSeries_eval
Documentation

At every standard level, analytic evaluation of the multiplicative Lubin--Tate series is the literal polynomial (1 + x)^p - 1.

Source context 15 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
/-- The maximal-ideal adic structure on a standard finite Lubin--Tate level. -/
noncomputable local instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
/-- Completeness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetT2Space
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
section PadicLevelTopology
/-- The specialized level uses the same maximal-ideal adic topology as the generic evaluator. -/
noncomputable local instance
    padicMultiplicativeLevelTargetTopologicalSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    TopologicalSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring :=
  @WithIdeal.instTopologicalSpace _ _
    (padicMultiplicativeLevelTargetWithIdeal
      (F := padicLocalField p)
      (π := show (padicLocalField p).valuationSubring from
        padicIntEquivValuationSubring p (p : ℤ_[p]))
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)
Lean source · statement
theorem padicMultiplicativeLubinTateSeries_eval
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x :
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    standardLubinTateLevelPowerSeriesEval
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx
        (padicMultiplicativeLubinTateSeries p).toPowerSeries =
      (1 + x) ^ p - 1
theorem

padicStandardToMultiplicativeIntertwiner_eval_functionalEquation

L139 ↗
LubinTate.padicStandardToMultiplicativeIntertwiner_eval_functionalEquation
Documentation

Analytic evaluation preserves the standard-to-multiplicative intertwining equation at every topologically nilpotent level integer.

Source context 15 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
/-- The maximal-ideal adic structure on a standard finite Lubin--Tate level. -/
noncomputable local instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
/-- Completeness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetT2Space
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
section PadicLevelTopology
/-- The specialized level uses the same maximal-ideal adic topology as the generic evaluator. -/
noncomputable local instance
    padicMultiplicativeLevelTargetTopologicalSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    TopologicalSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring :=
  @WithIdeal.instTopologicalSpace _ _
    (padicMultiplicativeLevelTargetWithIdeal
      (F := padicLocalField p)
      (π := show (padicLocalField p).valuationSubring from
        padicIntEquivValuationSubring p (p : ℤ_[p]))
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)
Lean source · statement
theorem padicStandardToMultiplicativeIntertwiner_eval_functionalEquation
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x :
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    standardLubinTateLevelPowerSeriesEval
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
        (standardLubinTateLevelPowerSeriesEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx
          (padicStandardToMultiplicativeIntertwiner p))
        (standardLubinTateLevelPowerSeriesEval_hasEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx
          (padicStandardToMultiplicativeIntertwiner p)
          (padicStandardToMultiplicativeIntertwiner_hasSubst p))
        (padicMultiplicativeLubinTateSeries p).toPowerSeries =
      standardLubinTateLevelPowerSeriesEval
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
        (standardLubinTateLevelPowerSeriesEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx
          (standardLubinTateSeries
            (padicMultiplicativeLubinTateSeries_isUniformizer p)).toPowerSeries)
        (standardLubinTateLevelPowerSeriesEval_hasEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx
          (standardLubinTateSeries
            (padicMultiplicativeLubinTateSeries_isUniformizer p)).toPowerSeries
          (PowerSeries.HasSubst.of_constantCoeff_zero
            (LubinTateSeries.constantCoeff_eq_zero
              (standardLubinTateSeries
                (padicMultiplicativeLubinTateSeries_isUniformizer p)))))
        (padicStandardToMultiplicativeIntertwiner p)
theorem

padicStandardToMultiplicativeIntertwiner_eval_endomorphism

L214 ↗
LubinTate.padicStandardToMultiplicativeIntertwiner_eval_endomorphism
Documentation

Finite-level evaluation of the comparison carries the standard scalar action with coefficient a to the unique multiplicative-series scalar action with the same coefficient.

Source context 15 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
/-- The maximal-ideal adic structure on a standard finite Lubin--Tate level. -/
noncomputable local instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
/-- Completeness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetT2Space
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
section PadicLevelTopology
/-- The specialized level uses the same maximal-ideal adic topology as the generic evaluator. -/
noncomputable local instance
    padicMultiplicativeLevelTargetTopologicalSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    TopologicalSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring :=
  @WithIdeal.instTopologicalSpace _ _
    (padicMultiplicativeLevelTargetWithIdeal
      (F := padicLocalField p)
      (π := show (padicLocalField p).valuationSubring from
        padicIntEquivValuationSubring p (p : ℤ_[p]))
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)
Lean source · full declaration
theorem padicStandardToMultiplicativeIntertwiner_eval_endomorphism
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x :
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a : (padicLocalField p).valuationSubring) :
    standardLubinTateLevelPowerSeriesEval
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
        (standardLubinTateEndomorphismEvalAt
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx a)
        (standardLubinTateEndomorphismEvalAt_hasEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx a)
        (padicStandardToMultiplicativeIntertwiner p) =
      standardLubinTateLevelPowerSeriesEval
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
        (standardLubinTateLevelPowerSeriesEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx
          (padicStandardToMultiplicativeIntertwiner p))
        (standardLubinTateLevelPowerSeriesEval_hasEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx
          (padicStandardToMultiplicativeIntertwiner p)
          (padicStandardToMultiplicativeIntertwiner_hasSubst p))
        (recursiveIntertwiner
          (padicMultiplicativeLubinTateSeries_isUniformizer p)
          (padicMultiplicativeLubinTateSeries p)
          (padicMultiplicativeLubinTateSeries p)
          (fun _ : Unit => a)) := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let H := padicStandardToMultiplicativeIntertwiner p
  let S := standardLubinTateEndomorphism hπ a
  let M :=
    recursiveIntertwiner hπ
      (padicMultiplicativeLubinTateSeries p)
      (padicMultiplicativeLubinTateSeries p)
      (fun _ : Unit => a)
  let xS := standardLubinTateEndomorphismEvalAt hπ n x hx a
  let xH := standardLubinTateLevelPowerSeriesEval hπ n x hx H
  let hSSubst : PowerSeries.HasSubst S :=
    (standardLubinTateEndomorphism_hasLinearTerm hπ a).hasSubst
  let hHSubst : PowerSeries.HasSubst H :=
    padicStandardToMultiplicativeIntertwiner_hasSubst p
  let hxS : PowerSeries.HasEval xS :=
    standardLubinTateEndomorphismEvalAt_hasEval hπ n x hx a
  let hxH : PowerSeries.HasEval xH :=
    standardLubinTateLevelPowerSeriesEval_hasEval
      hπ n x hx H hHSubst
  calc
    standardLubinTateLevelPowerSeriesEval hπ n xS hxS H =
        standardLubinTateLevelPowerSeriesEval hπ n x hx
          (PowerSeries.subst S H) :=
      (standardLubinTateLevelPowerSeriesEval_subst
        hπ n x hx S H hSSubst hxS).symm
    _ =
        standardLubinTateLevelPowerSeriesEval hπ n x hx
          (PowerSeries.subst H M) := by
      rw [padicStandardToMultiplicativeIntertwiner_endomorphism]
    _ =
        standardLubinTateLevelPowerSeriesEval hπ n xH hxH M :=
      standardLubinTateLevelPowerSeriesEval_subst
        hπ n x hx H M hHSubst hxH
theorem

padicMultiplicativeToStandardIntertwiner_eval_comp

L278 ↗
LubinTate.padicMultiplicativeToStandardIntertwiner_eval_comp
Documentation

Evaluating the reverse comparison after the forward comparison recovers every topologically nilpotent standard-level point.

Source context 15 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
/-- The maximal-ideal adic structure on a standard finite Lubin--Tate level. -/
noncomputable local instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
/-- Completeness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetT2Space
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
section PadicLevelTopology
/-- The specialized level uses the same maximal-ideal adic topology as the generic evaluator. -/
noncomputable local instance
    padicMultiplicativeLevelTargetTopologicalSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    TopologicalSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring :=
  @WithIdeal.instTopologicalSpace _ _
    (padicMultiplicativeLevelTargetWithIdeal
      (F := padicLocalField p)
      (π := show (padicLocalField p).valuationSubring from
        padicIntEquivValuationSubring p (p : ℤ_[p]))
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)
Lean source · statement
theorem padicMultiplicativeToStandardIntertwiner_eval_comp
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x :
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    standardLubinTateLevelPowerSeriesEval
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
        (standardLubinTateLevelPowerSeriesEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx
          (padicStandardToMultiplicativeIntertwiner p))
        (standardLubinTateLevelPowerSeriesEval_hasEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx
          (padicStandardToMultiplicativeIntertwiner p)
          (padicStandardToMultiplicativeIntertwiner_hasSubst p))
        (padicMultiplicativeToStandardIntertwiner p) =
      x
theorem

padicStandardToMultiplicativeIntertwiner_eval_zero

L323 ↗
LubinTate.padicStandardToMultiplicativeIntertwiner_eval_zero
Documentation

The forward comparison evaluates to zero at the zero point.

Source context 15 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
/-- The maximal-ideal adic structure on a standard finite Lubin--Tate level. -/
noncomputable local instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
/-- Completeness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetT2Space
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
section PadicLevelTopology
/-- The specialized level uses the same maximal-ideal adic topology as the generic evaluator. -/
noncomputable local instance
    padicMultiplicativeLevelTargetTopologicalSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    TopologicalSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring :=
  @WithIdeal.instTopologicalSpace _ _
    (padicMultiplicativeLevelTargetWithIdeal
      (F := padicLocalField p)
      (π := show (padicLocalField p).valuationSubring from
        padicIntEquivValuationSubring p (p : ℤ_[p]))
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)
Lean source · statement
theorem padicStandardToMultiplicativeIntertwiner_eval_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    standardLubinTateLevelPowerSeriesEval
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
        0 PowerSeries.HasEval.zero
        (padicStandardToMultiplicativeIntertwiner p) =
      0
theorem

padicStandardToMultiplicativeIntertwiner_eval_injective

L352 ↗
LubinTate.padicStandardToMultiplicativeIntertwiner_eval_injective
Documentation

Evaluation of the forward comparison is injective on topologically nilpotent points of every standard level.

Source context 15 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
variable {K : Type u} [Field K]
/-- The discrete coefficient uniformity used for finite-level analytic evaluation. -/
noncomputable local instance
    padicMultiplicativeLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
/-- The maximal-ideal adic structure on a standard finite Lubin--Tate level. -/
noncomputable local instance
    padicMultiplicativeLevelTargetWithIdeal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
/-- Completeness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the standard finite-level valuation ring for its adic topology. -/
noncomputable local instance
    padicMultiplicativeLevelTargetT2Space
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
section PadicLevelTopology
/-- The specialized level uses the same maximal-ideal adic topology as the generic evaluator. -/
noncomputable local instance
    padicMultiplicativeLevelTargetTopologicalSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    TopologicalSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring :=
  @WithIdeal.instTopologicalSpace _ _
    (padicMultiplicativeLevelTargetWithIdeal
      (F := padicLocalField p)
      (π := show (padicLocalField p).valuationSubring from
        padicIntEquivValuationSubring p (p : ℤ_[p]))
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n)
Lean source · statement
theorem padicStandardToMultiplicativeIntertwiner_eval_injective
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    {x y :
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring}
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy :
      standardLubinTateLevelPowerSeriesEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n x hx
          (padicStandardToMultiplicativeIntertwiner p) =
        standardLubinTateLevelPowerSeriesEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n y hy
          (padicStandardToMultiplicativeIntertwiner p)) :
    x = y

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