Module

Series.lean

Nyll.ClassFieldTheory.LubinTate.FormalModule.Series

2 declarations indexed from sourceView source ↗

Module documentation

Lubin--Tate power series

A Lubin--Tate power series over a chosen valuation ring has zero constant coefficient, prescribed linear coefficient, and reduces to the residue-field Frobenius power series. The chosen element is not required to be a uniformizer in the structure itself, so the coefficient package can be reused independently.

Imports3

Mathlib.SetTheory.Cardinal.Finite
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.Basic
Mathlib.RingTheory.PowerSeries.Basic

Imported by4

structure

LubinTateSeries

L36 ↗

LubinTate.LubinTateSeries

Documentation

A Lubin--Tate series with prescribed linear coefficient π.

The first two fields specify the constant and linear terms. The final field specifies coefficientwise reduction to the residue-field Frobenius series.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · full declaration

structure LubinTateSeries
    (F : LocalField.{u, v} K) (π : F.valuationSubring) where
  /-- The underlying one-variable formal power series over `O_K`. -/
  toPowerSeries : PowerSeries F.valuationSubring
  /-- The constant coefficient of a Lubin--Tate series vanishes. -/
  constantCoeff_eq_zero :
    PowerSeries.constantCoeff toPowerSeries = 0
  /-- The linear coefficient is the chosen element `π`. -/
  coeff_one_eq_uniformizer :
    PowerSeries.coeff 1 toPowerSeries = π
  /-- Reduction to the residue field is the `q`-power Frobenius series. -/
  map_residue_eq_frobenius :
    PowerSeries.map F.residueMap toPowerSeries =
      (PowerSeries.X : PowerSeries F.residueField) ^
        Nat.card F.residueField

theorem

ext

L63 ↗

LubinTate.LubinTateSeries.ext

Documentation

Two Lubin--Tate series are equal when their underlying power series are equal.

Source context 8 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
attribute [simp] LubinTateSeries.constantCoeff_eq_zero
  LubinTateSeries.coeff_one_eq_uniformizer
  LubinTateSeries.map_residue_eq_frobenius
namespace LubinTateSeries
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}

Lean source · statement

theorem ext {e e' : LubinTateSeries F π}
    (h : e.toPowerSeries = e'.toPowerSeries) : e = e'

Module documentation

Lubin--Tate power series

Declarations

LubinTateSeries

ext