NYLL
Module

CompletedPrimitivePoint.lean

Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeEvaluation.CompletedPrimitivePoint
10 declarations indexed from sourceView source ↗

Module documentation

The completed multiplicative primitive point

This module evaluates the completed multiplicative comparison at the chosen completed standard primitive point. It proves the exact standard and changed-uniformizer torsion bounds and constructs the actual unit action on that point.

Imports2
Imported by2

Declarations

def

padicCompletedMultiplicativePrimitivePoint

L42 ↗
LubinTate.padicCompletedMultiplicativePrimitivePoint
Documentation

The completed multiplicative division point obtained by evaluating the coefficient-extended comparison at the chosen completed standard primitive point.

Source context 9 commands

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

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

padicCompletedMultiplicativePrimitivePoint_hasEval

L52 ↗
LubinTate.padicCompletedMultiplicativePrimitivePoint_hasEval
Documentation

The completed multiplicative primitive point is topologically nilpotent, so it is itself a valid power-series evaluation point.

Source context 9 commands

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

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

padicCompletedMultiplicativePrimitivePoint_uniformizer_pow_succ_eq_zero

L65 ↗
LubinTate.padicCompletedMultiplicativePrimitivePoint_uniformizer_pow_succ_eq_zero
Documentation

The actual completed multiplicative primitive point is killed by the scalar endomorphism for π ^ (n + 1).

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem
    padicCompletedMultiplicativePrimitivePoint_uniformizer_pow_succ_eq_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    padicCompletedMultiplicativeScalarEndomorphismValue p n
        (padicCompletedMultiplicativePrimitivePoint p n)
        (padicCompletedMultiplicativePrimitivePoint_hasEval p n)
        ((padicIntEquivValuationSubring p (p : ℤ_[p])) ^ (n + 1)) =
      0
theorem

padicCompletedMultiplicativePrimitivePoint_uniformizer_pow_ne_zero

L141 ↗
LubinTate.padicCompletedMultiplicativePrimitivePoint_uniformizer_pow_ne_zero
Documentation

The actual completed multiplicative primitive point is not killed by the scalar endomorphism for π ^ n.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem
    padicCompletedMultiplicativePrimitivePoint_uniformizer_pow_ne_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    padicCompletedMultiplicativeScalarEndomorphismValue p n
        (padicCompletedMultiplicativePrimitivePoint p n)
        (padicCompletedMultiplicativePrimitivePoint_hasEval p n)
        ((padicIntEquivValuationSubring p (p : ℤ_[p])) ^ n) ≠
      0
theorem

padicCompletedMultiplicativePrimitivePoint_changedUniformizer_pow_succ_eq_zero

L189 ↗
LubinTate.padicCompletedMultiplicativePrimitivePoint_changedUniformizer_pow_succ_eq_zero
Documentation

The completed multiplicative primitive point is killed by the n + 1-st power of the scalar u p defining the changed uniformizer.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem
    padicCompletedMultiplicativePrimitivePoint_changedUniformizer_pow_succ_eq_zero
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedMultiplicativeScalarEndomorphismValue p n
        (padicCompletedMultiplicativePrimitivePoint p n)
        (padicCompletedMultiplicativePrimitivePoint_hasEval p n)
        ((standardLubinTateChangedUniformizer
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) u) ^ (n + 1)) =
      0
theorem

padicCompletedMultiplicativePrimitivePoint_changedUniformizer_pow_ne_zero

L252 ↗
LubinTate.padicCompletedMultiplicativePrimitivePoint_changedUniformizer_pow_ne_zero
Documentation

The completed multiplicative primitive point is not killed one level early by the scalar u p.

Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
attribute [local instance 50]
  padicCompletedMultiplicativeWittUniformSpace
attribute [local instance]
  padicCompletedMultiplicativeTargetWithIdeal
  padicCompletedMultiplicativeTargetCompleteSpace
  padicCompletedMultiplicativeTargetT2Space
Lean source · statement
theorem
    padicCompletedMultiplicativePrimitivePoint_changedUniformizer_pow_ne_zero
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedMultiplicativeScalarEndomorphismValue p n
        (padicCompletedMultiplicativePrimitivePoint p n)
        (padicCompletedMultiplicativePrimitivePoint_hasEval p n)
        ((standardLubinTateChangedUniformizer
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) u) ^ n) ≠
      0
def

padicCompletedMultiplicativeUnitEndomorphism

L322 ↗
LubinTate.padicCompletedMultiplicativeUnitEndomorphism
Documentation

The multiplicative scalar endomorphism attached to a p-adic unit, with coefficients extended to the completed unramified Witt ring.

Source context 9 commands

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

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

padicCompletedMultiplicativeUnitEndomorphism_hasSubst

L331 ↗
LubinTate.padicCompletedMultiplicativeUnitEndomorphism_hasSubst
Documentation

The completed multiplicative unit endomorphism admits formal substitution.

Source context 9 commands

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

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

padicCompletedMultiplicativePrimitivePointUnitAction

L343 ↗
LubinTate.padicCompletedMultiplicativePrimitivePointUnitAction
Documentation

The action of a completed multiplicative unit endomorphism on the completed multiplicative primitive point.

Source context 9 commands

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

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

padicCompletedMultiplicativePrimitivePointUnitAction_hasEval

L354 ↗
LubinTate.padicCompletedMultiplicativePrimitivePointUnitAction_hasEval
Documentation

The unit translate of the completed multiplicative primitive point is again a convergent evaluation point.

Source context 9 commands

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

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

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