NYLL
Module

CompletedEvaluation.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.CompletedEvaluation
25 declarations indexed from sourceView source ↗

Module documentation

Analytic evaluation in standard Lubin--Tate level fields

The scalar endomorphisms of a Lubin--Tate formal module are genuine infinite power series. This file evaluates them in the complete valuation ring of a standard finite level.

The coefficient map is the canonical map of valuation rings attached to the valued extension. The target carries its maximal-ideal adic topology. The chosen primitive division point is a uniformizer, hence is topologically nilpotent and is therefore a valid evaluation point.

Imports5
Imported by4

Declarations

instance

standardLubinTateLevelCoefficientUniformSpace

L45 ↗
LubinTate.standardLubinTateLevelCoefficientUniformSpace
Source context 11 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
Lean source · statement
instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring
instance

standardLubinTateLevelTargetWithIdeal

L51 ↗
LubinTate.standardLubinTateLevelTargetWithIdeal
Source context 12 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
Lean source · full declaration
instance
    standardLubinTateLevelTargetWithIdeal
    {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

standardLubinTateLevelTargetCompleteSpace

L59 ↗
LubinTate.standardLubinTateLevelTargetCompleteSpace
Source context 13 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
    standardLubinTateLevelTargetCompleteSpace
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
instance

standardLubinTateLevelTargetT2Space

L69 ↗
LubinTate.standardLubinTateLevelTargetT2Space
Source context 14 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
    standardLubinTateLevelTargetT2Space
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
def

standardLubinTateLevelCoefficientHom

L81 ↗
LubinTate.standardLubinTateLevelCoefficientHom
Documentation

The canonical coefficient map from the base valuation ring to the valuation ring of a standard Lubin--Tate level.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
def standardLubinTateLevelCoefficientHom
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    F.valuationSubring →+*
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
theorem

standardLubinTateLevelCoefficientHom_apply

L92 ↗
LubinTate.standardLubinTateLevelCoefficientHom_apply
Documentation

The level coefficient map is the ambient field algebra map after coercion from the two valuation rings.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateLevelCoefficientHom_apply
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : F.valuationSubring) :
    (standardLubinTateLevelCoefficientHom hπ n a).1 =
        algebraMap K (standardLubinTateLevelField hπ n) (a : K)
theorem

standardLubinTatePrimitivePointInteger_hasEval

L103 ↗
LubinTate.standardLubinTatePrimitivePointInteger_hasEval
Documentation

The primitive point is topologically nilpotent for the maximal-ideal adic topology of the level valuation ring.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTatePrimitivePointInteger_hasEval
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    PowerSeries.HasEval
      (standardLubinTatePrimitivePointInteger hπ n)
def

standardLubinTateLevelPowerSeriesEval

L115 ↗
LubinTate.standardLubinTateLevelPowerSeriesEval
Documentation

Analytic evaluation of power series at a topologically nilpotent integer of a standard Lubin--Tate level.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
def standardLubinTateLevelPowerSeriesEval
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    F.valuationSubring⟦X⟧ →+*
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
theorem

standardLubinTateLevelPowerSeriesEval_X

L128 ↗
LubinTate.standardLubinTateLevelPowerSeriesEval_X
Documentation

Evaluation sends the power-series variable to the chosen point.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateLevelPowerSeriesEval_X
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    standardLubinTateLevelPowerSeriesEval hπ n x hx PowerSeries.X = x
theorem

standardLubinTateLevelPowerSeriesEval_C

L140 ↗
LubinTate.standardLubinTateLevelPowerSeriesEval_C
Documentation

Evaluation sends a constant power series through the canonical coefficient map.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateLevelPowerSeriesEval_C
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) (a : F.valuationSubring) :
    standardLubinTateLevelPowerSeriesEval hπ n x hx
        (PowerSeries.C a) =
      standardLubinTateLevelCoefficientHom hπ n a
theorem

standardLubinTateLevelPowerSeriesEval_coe

L154 ↗
LubinTate.standardLubinTateLevelPowerSeriesEval_coe
Documentation

On polynomial power series, analytic evaluation agrees with ordinary polynomial evaluation.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateLevelPowerSeriesEval_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (P : Polynomial F.valuationSubring) :
    standardLubinTateLevelPowerSeriesEval hπ n x hx
        (P : PowerSeries F.valuationSubring) =
      Polynomial.eval₂
        (standardLubinTateLevelCoefficientHom hπ n) x P
theorem

standardLubinTateLevelPowerSeriesEval_continuous

L168 ↗
LubinTate.standardLubinTateLevelPowerSeriesEval_continuous
Documentation

Evaluation at a topologically nilpotent level integer is continuous.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateLevelPowerSeriesEval_continuous
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    Continuous
      (standardLubinTateLevelPowerSeriesEval hπ n x hx)
theorem

standardLubinTateLevelPowerSeriesEval_hasEval

L183 ↗
LubinTate.standardLubinTateLevelPowerSeriesEval_hasEval
Documentation

Evaluating a series with zero constant coefficient produces another topologically nilpotent level integer.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateLevelPowerSeriesEval_hasEval
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (f : PowerSeries F.valuationSubring)
    (hf : PowerSeries.HasSubst f) :
    PowerSeries.HasEval
      (standardLubinTateLevelPowerSeriesEval hπ n x hx f)
theorem

standardLubinTateLevelPowerSeriesEval_subst

L196 ↗
LubinTate.standardLubinTateLevelPowerSeriesEval_subst
Documentation

Analytic evaluation commutes with one-variable formal substitution.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateLevelPowerSeriesEval_subst
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a f : PowerSeries F.valuationSubring)
    (ha : PowerSeries.HasSubst a)
    (haEval : PowerSeries.HasEval
      (standardLubinTateLevelPowerSeriesEval hπ n x hx a)) :
    standardLubinTateLevelPowerSeriesEval hπ n x hx
        (PowerSeries.subst a f) =
      standardLubinTateLevelPowerSeriesEval hπ n
        (standardLubinTateLevelPowerSeriesEval hπ n x hx a)
        haEval f
def

standardLubinTatePrimitivePointEvaluation

L227 ↗
LubinTate.standardLubinTatePrimitivePointEvaluation
Documentation

The canonical evaluation homomorphism at the primitive point.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
def standardLubinTatePrimitivePointEvaluation
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    F.valuationSubring⟦X⟧ →+*
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
def

standardLubinTateEndomorphismEvalAt

L238 ↗
LubinTate.standardLubinTateEndomorphismEvalAt
Documentation

The value of the standard scalar endomorphism [a] at an arbitrary topologically nilpotent integer of a finite level.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
def standardLubinTateEndomorphismEvalAt
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) (a : F.valuationSubring) :
    (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
theorem

standardLubinTateEndomorphismEvalAt_hasEval

L248 ↗
LubinTate.standardLubinTateEndomorphismEvalAt_hasEval
Documentation

Every evaluated scalar endomorphism remains topologically nilpotent.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateEndomorphismEvalAt_hasEval
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) (a : F.valuationSubring) :
    PowerSeries.HasEval
      (standardLubinTateEndomorphismEvalAt hπ n x hx a)
def

standardLubinTateEndomorphismValue

L260 ↗
LubinTate.standardLubinTateEndomorphismValue
Documentation

The value [a](lambda_(n+1)) at the chosen primitive division point.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
def standardLubinTateEndomorphismValue
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : F.valuationSubring) :
    (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
theorem

standardLubinTateEndomorphismValue_hasEval

L271 ↗
LubinTate.standardLubinTateEndomorphismValue_hasEval
Documentation

Every scalar value at the primitive point is again topologically nilpotent.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateEndomorphismValue_hasEval
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : F.valuationSubring) :
    PowerSeries.HasEval
      (standardLubinTateEndomorphismValue hπ n a)
theorem

standardLubinTateEndomorphismEvalAt_one

L283 ↗
LubinTate.standardLubinTateEndomorphismEvalAt_one
Documentation

The value of [1] is the evaluation point.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateEndomorphismEvalAt_one
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    standardLubinTateEndomorphismEvalAt hπ n x hx 1 = x
theorem

standardLubinTateEndomorphismEvalAt_zero

L295 ↗
LubinTate.standardLubinTateEndomorphismEvalAt_zero
Documentation

The value of [0] is zero.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateEndomorphismEvalAt_zero
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    standardLubinTateEndomorphismEvalAt hπ n x hx 0 = 0
theorem

standardLubinTateEndomorphismEvalAt_mul

L306 ↗
LubinTate.standardLubinTateEndomorphismEvalAt_mul
Documentation

Multiplication of scalars becomes composition after analytic evaluation.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateEndomorphismEvalAt_mul
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) (a b : F.valuationSubring) :
    standardLubinTateEndomorphismEvalAt hπ n x hx (a * b) =
      standardLubinTateEndomorphismEvalAt hπ n
        (standardLubinTateEndomorphismEvalAt hπ n x hx b)
        (standardLubinTateEndomorphismEvalAt_hasEval hπ n x hx b) a
theorem

standardLubinTateEndomorphismValue_mul

L325 ↗
LubinTate.standardLubinTateEndomorphismValue_mul
Documentation

At the primitive point, multiplication of scalars is analytic composition of their values.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateEndomorphismValue_mul
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a b : F.valuationSubring) :
    standardLubinTateEndomorphismValue hπ n (a * b) =
      standardLubinTateEndomorphismEvalAt hπ n
        (standardLubinTateEndomorphismValue hπ n b)
        (standardLubinTateEndomorphismValue_hasEval hπ n b) a
theorem

standardLubinTateEndomorphismValue_one

L339 ↗
LubinTate.standardLubinTateEndomorphismValue_one
Documentation

The primitive-point value of [1] is the primitive point itself.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateEndomorphismValue_one
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    standardLubinTateEndomorphismValue hπ n 1 =
      standardLubinTatePrimitivePointInteger hπ n
theorem

standardLubinTateEndomorphismValue_zero

L350 ↗
LubinTate.standardLubinTateEndomorphismValue_zero
Documentation

The primitive-point value of [0] is zero.

Source context 15 commands

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

noncomputable section
open Filter
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open SameUniformizer
variable {K : Type u} [Field K]
private noncomputable local instance (priority := 50)
    standardLubinTateLevelCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTateLevelTargetWithIdeal
    {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
private noncomputable local instance
    standardLubinTateLevelTargetCompleteSpace
    {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
private noncomputable local instance
    standardLubinTateLevelTargetT2Space
    {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
Lean source · statement
theorem standardLubinTateEndomorphismValue_zero
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    standardLubinTateEndomorphismValue hπ n 0 = 0

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