Module

RecursiveCoefficient.lean

Nyll.ClassFieldTheory.LubinTate.FormalModule.RecursiveCoefficient

5 declarations indexed from sourceView source ↗

Module documentation

Recursive coefficients for Lubin--Tate intertwiners

This module connects the two coefficient-level inputs for the recursive construction of a same-uniformizer Lubin--Tate intertwiner. Reduction makes every coefficient of the current defect divisible by the uniformizer. In total degree m ≥ 2, the remaining scalar equation has factor 1 - π ^ (m - 1), which is a unit.

Imports1

Nyll.ClassFieldTheory.LubinTate.FormalModule.Reduction

Imported by3

def

normalizedDefectCoefficient

L36 ↗

LubinTate.SameUniformizer.normalizedDefectCoefficient

Documentation

The coefficient of an intertwining defect after removing one factor of the chosen uniformizer.

Source context 8 commands

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

noncomputable section
universe u v w
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type w} [Fintype σ]

Lean source · statement

def normalizedDefectCoefficient
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) :
    F.valuationSubring

theorem

uniformizer_mul_normalizedDefectCoefficient

L47 ↗

LubinTate.SameUniformizer.uniformizer_mul_normalizedDefectCoefficient

Documentation

Multiplying the normalized defect coefficient by the uniformizer recovers the original coefficient.

Source context 8 commands

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

noncomputable section
universe u v w
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type w} [Fintype σ]

Lean source · statement

theorem uniformizer_mul_normalizedDefectCoefficient
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) :
    π * normalizedDefectCoefficient hπ e ebar hH d =
      MvPowerSeries.coeff d (defect e ebar H)

def

correctionCoefficient

L65 ↗

LubinTate.SameUniformizer.correctionCoefficient

Documentation

The coefficient added in total degree d.degree by the recursive same-uniformizer intertwiner construction.

Its defining equation is the one which cancels the normalized defect in that degree. The hypothesis 2 ≤ d.degree ensures that the exponent d.degree - 1 is positive.

Source context 8 commands

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

noncomputable section
universe u v w
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type w} [Fintype σ]

Lean source · statement

def correctionCoefficient
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) (hd : 2 ≤ d.degree) :
    F.valuationSubring

theorem

correctionCoefficient_spec

L79 ↗

LubinTate.SameUniformizer.correctionCoefficient_spec

Documentation

The recursive correction coefficient satisfies its defining scalar equation.

Source context 8 commands

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

noncomputable section
universe u v w
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type w} [Fintype σ]

Lean source · statement

theorem correctionCoefficient_spec
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) (hd : 2 ≤ d.degree) :
    (1 - π ^ (d.degree - 1)) *
        correctionCoefficient hπ e ebar hH d hd =
      -normalizedDefectCoefficient hπ e ebar hH d

theorem

correctionCoefficient_unique

L96 ↗

LubinTate.SameUniformizer.correctionCoefficient_unique

Documentation

The defining scalar equation determines the recursive correction coefficient uniquely.

Source context 8 commands

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

noncomputable section
universe u v w
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
variable {σ : Type w} [Fintype σ]

Lean source · statement

theorem correctionCoefficient_unique
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) (hd : 2 ≤ d.degree)
    {c : F.valuationSubring}
    (hc :
      (1 - π ^ (d.degree - 1)) * c =
        -normalizedDefectCoefficient hπ e ebar hH d) :
    c = correctionCoefficient hπ e ebar hH d hd

Module documentation

Recursive coefficients for Lubin--Tate intertwiners

Declarations

normalizedDefectCoefficient

uniformizer_mul_normalizedDefectCoefficient

correctionCoefficient

correctionCoefficient_spec

correctionCoefficient_unique