Module

StandardSeries.lean

Nyll.ClassFieldTheory.LubinTate.FormalModule.StandardSeries

3 declarations indexed from sourceView source ↗

Module documentation

The standard Lubin--Tate series

For a uniformizer π, the polynomial power series

π X + X ^ q,

where q is the cardinality of the residue field, is a Lubin--Tate series. This gives the general formal-module construction a canonical polynomial input without making an equal-characteristic assumption.

Imports1

Nyll.ClassFieldTheory.LubinTate.FormalModule.CoefficientEquation

Imported by4

def

standardLubinTatePowerSeries

L36 ↗

LubinTate.standardLubinTatePowerSeries

Documentation

The polynomial power series π X + X ^ q, where q is the residue field cardinality.

Source context 6 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]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}

Lean source · statement

def standardLubinTatePowerSeries
    (F : LocalField.{u, v} K) (π : F.valuationSubring) :
    PowerSeries F.valuationSubring

def

standardLubinTateSeries

L43 ↗

LubinTate.standardLubinTateSeries

Documentation

A uniformizer makes π X + X ^ q into a Lubin--Tate series.

Source context 6 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]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}

Lean source · full declaration

def standardLubinTateSeries
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    LubinTateSeries F π where
  toPowerSeries := standardLubinTatePowerSeries F π
  constantCoeff_eq_zero := by
    have hq0 : Nat.card F.residueField ≠ 0 :=
      Nat.ne_of_gt (lt_trans Nat.zero_lt_one
        (Finite.one_lt_card (α := F.residueField)))
    simp [standardLubinTatePowerSeries, hq0]
  coeff_one_eq_uniformizer := by
    have hq : 1 ≠ Nat.card F.residueField :=
      (Finite.one_lt_card (α := F.residueField)).ne
    simp [standardLubinTatePowerSeries, PowerSeries.coeff_X_pow, hq]
  map_residue_eq_frobenius := by
    simp [standardLubinTatePowerSeries,
      SameUniformizer.residueMap_uniformizer_eq_zero hπ]

theorem

standardLubinTateSeries_toPowerSeries

L65 ↗

LubinTate.LubinTateSeries.standardLubinTateSeries_toPowerSeries

Documentation

The underlying series of the standard Lubin--Tate input is literally π X + X ^ q.

Source context 7 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]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
namespace LubinTateSeries

Lean source · statement

theorem standardLubinTateSeries_toPowerSeries
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    (standardLubinTateSeries hπ).toPowerSeries =
      standardLubinTatePowerSeries F π

Module documentation

The standard Lubin--Tate series

Declarations

standardLubinTatePowerSeries

standardLubinTateSeries

standardLubinTateSeries_toPowerSeries