Module

CompletedSeries.lean

Nyll.ClassFieldTheory.LubinTate.Padic.ChangedUniformizerIntertwiner.CompletedSeries

12 declarations indexed from sourceView source ↗

Module documentation

Completed p-adic Lubin--Tate series

This module extends the multiplicative and changed-standard Lubin--Tate series to the completed unramified Witt ring and records their coefficients and residue reductions.

Imports4

Imported by4

def

padicCompletedMultiplicativeSeries

L31 ↗

LubinTate.padicCompletedMultiplicativeSeries

Documentation

The multiplicative Lubin--Tate series after extending its coefficients to the completed unramified Witt ring.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

def padicCompletedMultiplicativeSeries
    (p : ℕ) [Fact p.Prime] :
    PowerSeries (padicCompletedUnramifiedWittRing p)

def

padicCompletedChangedStandardSeries

L40 ↗

LubinTate.padicCompletedChangedStandardSeries

Documentation

The standard Lubin--Tate series for the changed uniformizer u p, after extending its coefficients to the completed unramified Witt ring.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

def padicCompletedChangedStandardSeries
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries (padicCompletedUnramifiedWittRing p)

theorem

padicCompletedMultiplicativeSeries_eq

L52 ↗

LubinTate.padicCompletedMultiplicativeSeries_eq

Documentation

The completed multiplicative Lubin--Tate series is the binomial series (1 + X) ^ p - 1.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicCompletedMultiplicativeSeries_eq
    (p : ℕ) [Fact p.Prime] :
    padicCompletedMultiplicativeSeries p =
      (1 + PowerSeries.X) ^ p - 1

theorem

padicCompletedChangedStandardSeries_eq

L63 ↗

LubinTate.padicCompletedChangedStandardSeries_eq

Documentation

The completed changed-standard series has linear coefficient u p and degree-p term X ^ p.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicCompletedChangedStandardSeries_eq
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    padicCompletedChangedStandardSeries p u =
      PowerSeries.C
          (((padicValuationUnitToCompletedUnramifiedWittUnit p u :
              (padicCompletedUnramifiedWittRing p)ˣ) : padicCompletedUnramifiedWittRing p) *
            (p : padicCompletedUnramifiedWittRing p)) *
          PowerSeries.X +
        PowerSeries.X ^ p

theorem

padicCompletedMultiplicativeSeries_constantCoeff

L104 ↗

LubinTate.padicCompletedMultiplicativeSeries_constantCoeff

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicCompletedMultiplicativeSeries_constantCoeff
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.constantCoeff
        (padicCompletedMultiplicativeSeries p) = 0

theorem

padicCompletedMultiplicativeSeries_coeff_one

L118 ↗

LubinTate.padicCompletedMultiplicativeSeries_coeff_one

Documentation

The linear coefficient of the completed multiplicative series is p.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicCompletedMultiplicativeSeries_coeff_one
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.coeff 1
        (padicCompletedMultiplicativeSeries p) =
      (p : padicCompletedUnramifiedWittRing p)

theorem

padicCompletedChangedStandardSeries_constantCoeff

L130 ↗

LubinTate.padicCompletedChangedStandardSeries_constantCoeff

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicCompletedChangedStandardSeries_constantCoeff
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.constantCoeff
        (padicCompletedChangedStandardSeries p u) = 0

theorem

padicCompletedMultiplicativeSeries_hasSubst

L144 ↗

LubinTate.padicCompletedMultiplicativeSeries_hasSubst

Documentation

The completed multiplicative Lubin--Tate series admits formal substitution.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicCompletedMultiplicativeSeries_hasSubst
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.HasSubst (padicCompletedMultiplicativeSeries p)

theorem

padicCompletedChangedStandardSeries_hasSubst

L152 ↗

LubinTate.padicCompletedChangedStandardSeries_hasSubst

Documentation

The completed changed standard Lubin--Tate series admits formal substitution.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicCompletedChangedStandardSeries_hasSubst
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.HasSubst (padicCompletedChangedStandardSeries p u)

theorem

padicCompletedMultiplicativeSeries_map_constantCoeff

L160 ↗

LubinTate.padicCompletedMultiplicativeSeries_map_constantCoeff

Documentation

Reduction of the completed multiplicative series modulo p is X ^ p.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicCompletedMultiplicativeSeries_map_constantCoeff
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.map WittVector.constantCoeff
        (padicCompletedMultiplicativeSeries p) =
      (PowerSeries.X :
        PowerSeries (AlgebraicClosure (ZMod p))) ^ p

theorem

padicCompletedChangedStandardSeries_map_constantCoeff

L175 ↗

LubinTate.padicCompletedChangedStandardSeries_map_constantCoeff

Documentation

Reduction of the completed changed-standard series modulo p is X ^ p.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicCompletedChangedStandardSeries_map_constantCoeff
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.map WittVector.constantCoeff
        (padicCompletedChangedStandardSeries p u) =
      (PowerSeries.X :
        PowerSeries (AlgebraicClosure (ZMod p))) ^ p

theorem

padicChangedUniformizerFrobenius_constantCoeff_eq_zero

L192 ↗

LubinTate.padicChangedUniformizerFrobenius_constantCoeff_eq_zero

Documentation

Coefficientwise Witt-vector Frobenius preserves a zero constant coefficient.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizerFrobenius_constantCoeff_eq_zero
    (p : ℕ) [Fact p.Prime]
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0) :
    PowerSeries.constantCoeff
        (PowerSeries.map WittVector.frobenius H) = 0

Module documentation

Completed p-adic Lubin--Tate series

Declarations