NYLL
Module

CompletedCoefficientEvaluation.lean

Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.CompletedCoefficientEvaluation
17 declarations indexed from sourceView source ↗

Module documentation

Coefficient maps and analytic evaluation on completed p-adic levels

This module equips completed Lubin--Tate levels with the direct p-adic coefficient maps used by polynomial and power-series evaluation. It also establishes the exact completed primitive-point torsion relations and the general injectivity criterion for evaluation with unit linear coefficient.

Imports2
Imported by3

Declarations

instance

padicCompletedMultiplicativeWittUniformSpace

L32 ↗
LubinTate.padicCompletedMultiplicativeWittUniformSpace
Documentation

The discrete Witt-vector coefficient uniformity used for completed evaluation.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
Lean source · statement
instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p)
instance

padicCompletedMultiplicativeTargetWithIdeal

L39 ↗
LubinTate.padicCompletedMultiplicativeTargetWithIdeal
Documentation

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

Source context 8 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
Lean source · full declaration
instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
instance

padicCompletedMultiplicativeTargetCompleteSpace

L47 ↗
LubinTate.padicCompletedMultiplicativeTargetCompleteSpace
Documentation

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

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
Lean source · statement
instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring
instance

padicCompletedMultiplicativeTargetT2Space

L57 ↗
LubinTate.padicCompletedMultiplicativeTargetT2Space
Documentation

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

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
Lean source · statement
instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring
instance

padicCompletedLevelField_padicAlgebra

L68 ↗
LubinTate.padicCompletedLevelField_padicAlgebra
Documentation

The completed Lubin--Tate level as an algebra over the original p-adic base field, through the completed unramified coefficient field.

Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
instance padicCompletedLevelField_padicAlgebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra ℚ_[p] (padicCompletedLevelField p n)
instance

padicCompletedLevelField_padicScalarTower

L75 ↗
LubinTate.padicCompletedLevelField_padicScalarTower
Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
instance padicCompletedLevelField_padicScalarTower
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    IsScalarTower ℚ_[p] (padicCompletedUnramifiedField p)
      (padicCompletedLevelField p n)
def

padicCompletedLevelPadicFieldCoefficientHom

L83 ↗
LubinTate.padicCompletedLevelPadicFieldCoefficientHom
Documentation

The canonical coefficient map from the p-adic valuation ring directly into the field underlying a completed Lubin--Tate level.

Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
def padicCompletedLevelPadicFieldCoefficientHom
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicLocalField p).valuationSubring →+*
      padicCompletedLevelField p n
def

padicCompletedLevelPadicIntegerCoefficientHom

L94 ↗
LubinTate.padicCompletedLevelPadicIntegerCoefficientHom
Documentation

The same p-adic coefficient map with codomain restricted to the valuation ring of the completed level.

Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
def padicCompletedLevelPadicIntegerCoefficientHom
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicLocalField p).valuationSubring →+*
      (padicCompletedLevelCompleteDVF p n).valuationSubring
theorem

padicCompletedLevelPadicIntegerCoefficientHom_coe

L104 ↗
LubinTate.padicCompletedLevelPadicIntegerCoefficientHom_coe
Documentation

Coercing the integral p-adic coefficient map to the completed-level field gives the canonical field-valued coefficient map.

Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedLevelPadicIntegerCoefficientHom_coe
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : (padicLocalField p).valuationSubring) :
    ((padicCompletedLevelPadicIntegerCoefficientHom p n a :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
      padicCompletedLevelField p n) =
        padicCompletedLevelPadicFieldCoefficientHom p n a
theorem

padicCompletedLevelPadicIntegerPolynomialEval_coe

L149 ↗
LubinTate.padicCompletedLevelPadicIntegerPolynomialEval_coe
Documentation

Polynomial evaluation through the integral coefficient map agrees, after coercion, with evaluation through the field coefficient map.

Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedLevelPadicIntegerPolynomialEval_coe
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (P : Polynomial (padicLocalField p).valuationSubring) :
    ((Polynomial.eval₂
        (padicCompletedLevelPadicIntegerCoefficientHom p n) x P :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
        padicCompletedLevelField p n) =
      Polynomial.eval₂
        (padicCompletedLevelPadicFieldCoefficientHom p n)
        (x : padicCompletedLevelField p n) P
theorem

padicCompletedPrimitiveRoot_standardPrimitivePolynomial

L176 ↗
LubinTate.padicCompletedPrimitiveRoot_standardPrimitivePolynomial
Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRoot_standardPrimitivePolynomial
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Polynomial.eval₂
        (padicCompletedLevelPadicFieldCoefficientHom p n)
        (padicCompletedPrimitiveRoot p n)
        (standardLubinTatePrimitivePolynomial
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) n) =
      0
theorem

padicCompletedPrimitiveRoot_iterate_succ_eq_zero

L193 ↗
LubinTate.padicCompletedPrimitiveRoot_iterate_succ_eq_zero
Documentation

The chosen primitive point in the completed level is killed by the n + 1-fold standard p-adic Lubin--Tate iterate.

Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRoot_iterate_succ_eq_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Polynomial.eval₂
        (padicCompletedLevelPadicFieldCoefficientHom p n)
        (padicCompletedPrimitiveRoot p n)
        (standardLubinTatePolynomialIterate
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) (n + 1)) =
      0
theorem

padicCompletedPrimitiveRoot_iterate_ne_zero

L216 ↗
LubinTate.padicCompletedPrimitiveRoot_iterate_ne_zero
Documentation

The chosen completed primitive point is not killed one level early.

Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRoot_iterate_ne_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Polynomial.eval₂
        (padicCompletedLevelPadicFieldCoefficientHom p n)
        (padicCompletedPrimitiveRoot p n)
        (standardLubinTatePolynomialIterate
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) n) ≠
      0
theorem

padicCompletedPrimitiveRootInteger_iterate_succ_eq_zero

L274 ↗
LubinTate.padicCompletedPrimitiveRootInteger_iterate_succ_eq_zero
Documentation

Integral form of the exact completed primitive-point torsion relation at level n + 1.

Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRootInteger_iterate_succ_eq_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Polynomial.eval₂
        (padicCompletedLevelPadicIntegerCoefficientHom p n)
        (padicCompletedPrimitiveRootInteger p n)
        (standardLubinTatePolynomialIterate
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) (n + 1)) =
      0
theorem

padicCompletedPrimitiveRootInteger_iterate_ne_zero

L299 ↗
LubinTate.padicCompletedPrimitiveRootInteger_iterate_ne_zero
Documentation

The integral completed primitive point is not killed by the level-n standard iterate.

Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRootInteger_iterate_ne_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Polynomial.eval₂
        (padicCompletedLevelPadicIntegerCoefficientHom p n)
        (padicCompletedPrimitiveRootInteger p n)
        (standardLubinTatePolynomialIterate
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) n) ≠
      0
theorem

padicCompletedLevelPowerSeriesEval_congr_point

L319 ↗
LubinTate.padicCompletedLevelPowerSeriesEval_congr_point
Documentation

Completed-level power-series evaluation is independent of the proof that its evaluation point is topologically nilpotent.

Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedLevelPowerSeriesEval_congr_point
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    {x y : (padicCompletedLevelCompleteDVF p n).valuationSubring}
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy : x = y)
    (f : PowerSeries (padicCompletedUnramifiedWittRing p)) :
    padicCompletedLevelPowerSeriesEval p n x hx f =
      padicCompletedLevelPowerSeriesEval p n y hy f
theorem

padicCompletedLevelPowerSeriesEval_injective_of_unitLinearCoefficient

L332 ↗
LubinTate.padicCompletedLevelPowerSeriesEval_injective_of_unitLinearCoefficient
Documentation

A completed-level power-series evaluation with zero constant coefficient and a unit linear coefficient is injective on convergent points.

Source context 11 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
/-- The discrete Witt-vector coefficient uniformity used for completed evaluation. -/
noncomputable local instance (priority := 50)
    padicCompletedMultiplicativeWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
/-- The maximal-ideal adic structure on a completed Lubin--Tate level. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
/-- Completeness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
/-- Separatedness of the completed-level valuation ring for its adic topology. -/
noncomputable local instance
    padicCompletedMultiplicativeTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem
    padicCompletedLevelPowerSeriesEval_injective_of_unitLinearCoefficient
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (f : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hconstant : PowerSeries.constantCoeff f = 0)
    (hlinear : IsUnit (PowerSeries.coeff 1 f))
    {x y : (padicCompletedLevelCompleteDVF p n).valuationSubring}
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy :
      padicCompletedLevelPowerSeriesEval p n x hx f =
        padicCompletedLevelPowerSeriesEval p n y hy f) :
    x = y

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