Module

RecursiveIntertwiner.lean

Nyll.ClassFieldTheory.LubinTate.FormalModule.RecursiveIntertwiner

46 declarations indexed from sourceView source ↗

Module documentation

Finite-degree approximations to Lubin--Tate intertwiners

For a fixed total degree there are only finitely many monomials. This file orders those monomials, applies the coefficient correction from RecursiveCorrection one at a time, and then iterates the resulting degreewise correction.

The construction is genuinely recursive: stage n + 1 corrects every monomial of total degree n + 2. Corrections in that degree leave all lower coefficients unchanged. The stabilized coefficient series and its intertwining equation are established below after the finite-degree construction.

Imports2

Imported by3

theorem

linearForm_hasLinearTerm

L41 ↗

LubinTate.SameUniformizer.linearForm_hasLinearTerm

Documentation

The prescribed linear form itself has the prescribed linear term.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem linearForm_hasLinearTerm
    (L : sigma → F.valuationSubring) :
    HasLinearTerm (linearForm L) L

abbrev

Approximation

L46 ↗

LubinTate.SameUniformizer.Approximation

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

abbrev Approximation
    (L : sigma → F.valuationSubring)

def

degreeIndexList

L51 ↗

LubinTate.SameUniformizer.degreeIndexList

Documentation

The finite list of all monomials of a fixed total degree.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

def degreeIndexList (m : ℕ) :
    List {d : sigma →₀ ℕ // d.degree = m}

theorem

degreeIndexList_nodup

L57 ↗

LubinTate.SameUniformizer.degreeIndexList_nodup

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem degreeIndexList_nodup (m : ℕ) :
    (degreeIndexList (sigma := sigma) m).Nodup

theorem

mem_degreeIndexList

L62 ↗

LubinTate.SameUniformizer.mem_degreeIndexList

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem mem_degreeIndexList
    (m : ℕ) (d : {d : sigma →₀ ℕ // d.degree = m}) :
    d ∈ degreeIndexList (sigma := sigma) m

def

correctionStep

L70 ↗

LubinTate.SameUniformizer.correctionStep

Documentation

One step in a fixed-degree correction list, bundled with preservation of the prescribed linear term.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

def correctionStep
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (H : Approximation (F := F) L)
    (d : {d : sigma →₀ ℕ // d.degree = m}) :
    Approximation (F := F) L

def

correctList

L85 ↗

LubinTate.SameUniformizer.correctList

Documentation

Apply a list of fixed-degree monomial corrections from left to right.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

def correctList
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (ds : List {d : sigma →₀ ℕ // d.degree = m})
    (H : Approximation (F := F) L) :
    Approximation (F := F) L

theorem

coeff_correctionStep_eq_of_degree_lt

L95 ↗

LubinTate.SameUniformizer.coeff_correctionStep_eq_of_degree_lt

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_correctionStep_eq_of_degree_lt
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (H : Approximation (F := F) L)
    (d : {d : sigma →₀ ℕ // d.degree = m})
    (q : sigma →₀ ℕ) (hq : q.degree < m) :
    MvPowerSeries.coeff q (correctionStep hpi e ebar hm H d).1 =
      MvPowerSeries.coeff q H.1

theorem

coeff_correctList_eq_of_degree_lt

L115 ↗

LubinTate.SameUniformizer.coeff_correctList_eq_of_degree_lt

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_correctList_eq_of_degree_lt
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (ds : List {d : sigma →₀ ℕ // d.degree = m})
    (H : Approximation (F := F) L)
    (q : sigma →₀ ℕ) (hq : q.degree < m) :
    MvPowerSeries.coeff q (correctList hpi e ebar hm ds H).1 =
      MvPowerSeries.coeff q H.1

theorem

coeff_defect_correctionStep_eq_of_ne

L142 ↗

LubinTate.SameUniformizer.coeff_defect_correctionStep_eq_of_ne

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_defect_correctionStep_eq_of_ne
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (H : Approximation (F := F) L)
    (q d : {d : sigma →₀ ℕ // d.degree = m})
    (hqd : q ≠ d) :
    MvPowerSeries.coeff q.1
        (defect e ebar (correctionStep hpi e ebar hm H d).1) =
      MvPowerSeries.coeff q.1 (defect e ebar H.1)

theorem

coeff_defect_correctList_eq_of_not_mem

L165 ↗

LubinTate.SameUniformizer.coeff_defect_correctList_eq_of_not_mem

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_defect_correctList_eq_of_not_mem
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (ds : List {d : sigma →₀ ℕ // d.degree = m})
    (H : Approximation (F := F) L)
    (q : {d : sigma →₀ ℕ // d.degree = m})
    (hq : q ∉ ds) :
    MvPowerSeries.coeff q.1
        (defect e ebar (correctList hpi e ebar hm ds H).1) =
      MvPowerSeries.coeff q.1 (defect e ebar H.1)

theorem

coeff_defect_correctList_eq_zero_of_mem

L204 ↗

LubinTate.SameUniformizer.coeff_defect_correctList_eq_zero_of_mem

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_defect_correctList_eq_zero_of_mem
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (ds : List {d : sigma →₀ ℕ // d.degree = m})
    (H : Approximation (F := F) L)
    (hds : ds.Nodup)
    (q : {d : sigma →₀ ℕ // d.degree = m})
    (hq : q ∈ ds) :
    MvPowerSeries.coeff q.1
        (defect e ebar (correctList hpi e ebar hm ds H).1) = 0

def

correctDegree

L257 ↗

LubinTate.SameUniformizer.correctDegree

Documentation

Correct every monomial in one fixed total degree.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

def correctDegree
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    (H : Approximation (F := F) L)
    (m : ℕ) (hm : 2 ≤ m) :
    Approximation (F := F) L

theorem

coeff_correctDegree_eq_of_degree_lt

L266 ↗

LubinTate.SameUniformizer.coeff_correctDegree_eq_of_degree_lt

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_correctDegree_eq_of_degree_lt
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    (H : Approximation (F := F) L)
    (m : ℕ) (hm : 2 ≤ m)
    (q : sigma →₀ ℕ) (hq : q.degree < m) :
    MvPowerSeries.coeff q (correctDegree hpi e ebar H m hm).1 =
      MvPowerSeries.coeff q H.1

theorem

coeff_defect_correctDegree_eq_zero

L278 ↗

LubinTate.SameUniformizer.coeff_defect_correctDegree_eq_zero

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_defect_correctDegree_eq_zero
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    (H : Approximation (F := F) L)
    (m : ℕ) (hm : 2 ≤ m)
    (q : sigma →₀ ℕ) (hq : q.degree = m) :
    MvPowerSeries.coeff q
        (defect e ebar (correctDegree hpi e ebar H m hm).1) = 0

def

approximation

L301 ↗

LubinTate.SameUniformizer.approximation

Documentation

The bundled finite-degree approximations. Stage zero is the prescribed linear form, and stage n + 1 corrects total degree n + 2.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · full declaration

def approximation
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring) :
    ℕ → Approximation (F := F) L
  | 0 => ⟨linearForm L, linearForm_hasLinearTerm L⟩
  | n + 1 =>
      correctDegree hpi e ebar
        (approximation hpi e ebar L n) (n + 2) (by omega)

def

intertwinerApproximation

L313 ↗

LubinTate.SameUniformizer.intertwinerApproximation

Documentation

The stage-n finite-degree approximation to the intertwiner with linear term L.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

def intertwinerApproximation
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring) (n : ℕ) :
    MvPowerSeries sigma F.valuationSubring

theorem

intertwinerApproximation_hasLinearTerm

L321 ↗

LubinTate.SameUniformizer.intertwinerApproximation_hasLinearTerm

Documentation

Every finite-degree approximation retains the prescribed linear term.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem intertwinerApproximation_hasLinearTerm
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring) (n : ℕ) :
    HasLinearTerm (intertwinerApproximation hpi e ebar L n) L

theorem

intertwinerApproximation_zero

L330 ↗

LubinTate.SameUniformizer.intertwinerApproximation_zero

Documentation

Stage zero is exactly the prescribed linear form.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem intertwinerApproximation_zero
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring) :
    intertwinerApproximation hpi e ebar L 0 = linearForm L

theorem

coeff_intertwinerApproximation_succ_eq_of_degree_lt

L339 ↗

LubinTate.SameUniformizer.coeff_intertwinerApproximation_succ_eq_of_degree_lt

Documentation

Passing from stage n to stage n + 1 leaves every coefficient below total degree n + 2 unchanged.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_intertwinerApproximation_succ_eq_of_degree_lt
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring)
    (n : ℕ) (q : sigma →₀ ℕ) (hq : q.degree < n + 2) :
    MvPowerSeries.coeff q
        (intertwinerApproximation hpi e ebar L (n + 1)) =
      MvPowerSeries.coeff q
        (intertwinerApproximation hpi e ebar L n)

theorem

coeff_defect_intertwinerApproximation_succ_eq_zero

L355 ↗

LubinTate.SameUniformizer.coeff_defect_intertwinerApproximation_succ_eq_zero

Documentation

Stage n + 1 has zero defect in every coordinate of total degree n + 2.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_defect_intertwinerApproximation_succ_eq_zero
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring)
    (n : ℕ) (q : sigma →₀ ℕ) (hq : q.degree = n + 2) :
    MvPowerSeries.coeff q
        (defect e ebar
          (intertwinerApproximation hpi e ebar L (n + 1))) = 0

theorem

coeff_intertwinerApproximation_eq_of_le

L370 ↗

LubinTate.SameUniformizer.coeff_intertwinerApproximation_eq_of_le

Documentation

Once a coefficient lies below the next correction degree, it remains unchanged at every later finite stage.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_intertwinerApproximation_eq_of_le
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring)
    (q : sigma →₀ ℕ) {m n : ℕ} (hmn : m ≤ n)
    (hq : q.degree < m + 2) :
    MvPowerSeries.coeff q
        (intertwinerApproximation hpi e ebar L n) =
      MvPowerSeries.coeff q
        (intertwinerApproximation hpi e ebar L m)

def

recursiveIntertwiner

L390 ↗

LubinTate.SameUniformizer.recursiveIntertwiner

Documentation

The full recursive series takes the coefficient of a monomial of degree m from the first stage which has already corrected degree m.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

def recursiveIntertwiner
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring) :
    MvPowerSeries sigma F.valuationSubring

theorem

coeff_recursiveIntertwiner

L401 ↗

LubinTate.SameUniformizer.coeff_recursiveIntertwiner

Documentation

The defining stabilized-coefficient formula.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_recursiveIntertwiner
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring) (d : sigma →₀ ℕ) :
    MvPowerSeries.coeff d (recursiveIntertwiner hpi e ebar L) =
      MvPowerSeries.coeff d
        (intertwinerApproximation hpi e ebar L (d.degree - 1))

theorem

coeff_recursiveIntertwiner_eq_intertwinerApproximation

L412 ↗

LubinTate.SameUniformizer.coeff_recursiveIntertwiner_eq_intertwinerApproximation

Documentation

Through degree n + 1, the stabilized series agrees with the stage-n finite approximation.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_recursiveIntertwiner_eq_intertwinerApproximation
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring)
    (n : ℕ) (d : sigma →₀ ℕ) (hd : d.degree ≤ n + 1) :
    MvPowerSeries.coeff d (recursiveIntertwiner hpi e ebar L) =
      MvPowerSeries.coeff d
        (intertwinerApproximation hpi e ebar L n)

theorem

recursiveIntertwiner_hasLinearTerm

L427 ↗

LubinTate.SameUniformizer.recursiveIntertwiner_hasLinearTerm

Documentation

The stabilized recursive series retains the prescribed linear term.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem recursiveIntertwiner_hasLinearTerm
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring) :
    HasLinearTerm (recursiveIntertwiner hpi e ebar L) L

theorem

coeff_defect_recursiveIntertwiner_eq_zero

L445 ↗

LubinTate.SameUniformizer.coeff_defect_recursiveIntertwiner_eq_zero

Documentation

Every coefficient of the defect of the stabilized recursive series vanishes.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_defect_recursiveIntertwiner_eq_zero
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring)
    (d : sigma →₀ ℕ) :
    MvPowerSeries.coeff d
        (defect e ebar (recursiveIntertwiner hpi e ebar L)) = 0

theorem

recursiveIntertwiner_intertwines

L493 ↗

LubinTate.SameUniformizer.recursiveIntertwiner_intertwines

Documentation

The stabilized recursive series solves the same-uniformizer Lubin--Tate intertwining 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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem recursiveIntertwiner_intertwines
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring) :
    Intertwines e ebar (recursiveIntertwiner hpi e ebar L)

theorem

hasLinearTerm_add_monomial

L503 ↗

LubinTate.SameUniformizer.hasLinearTerm_add_monomial

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem hasLinearTerm_add_monomial
    {H : MvPowerSeries sigma F.valuationSubring}
    {L : sigma → F.valuationSubring}
    (hH : HasLinearTerm H L)
    (d : sigma →₀ ℕ) (hd : 2 ≤ d.degree)
    (c : F.valuationSubring) :
    HasLinearTerm (H + MvPowerSeries.monomial d c) L

def

replacementStep

L532 ↗

LubinTate.SameUniformizer.replacementStep

Documentation

Replace one coefficient in a fixed total degree by the corresponding coefficient of a target series.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

def replacementStep
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (target : MvPowerSeries sigma F.valuationSubring)
    (H : Approximation (F := F) L)
    (d : {d : sigma →₀ ℕ // d.degree = m}) :
    Approximation (F := F) L

def

replaceList

L547 ↗

LubinTate.SameUniformizer.replaceList

Documentation

Replace the coefficients indexed by a list in a fixed total degree.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

def replaceList
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (target : MvPowerSeries sigma F.valuationSubring)
    (ds : List {d : sigma →₀ ℕ // d.degree = m})
    (H : Approximation (F := F) L) :
    Approximation (F := F) L

theorem

coeff_replacementStep_self

L556 ↗

LubinTate.SameUniformizer.coeff_replacementStep_self

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_replacementStep_self
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (target : MvPowerSeries sigma F.valuationSubring)
    (H : Approximation (F := F) L)
    (d : {d : sigma →₀ ℕ // d.degree = m}) :
    MvPowerSeries.coeff d.1 (replacementStep hm target H d).1 =
      MvPowerSeries.coeff d.1 target

theorem

coeff_replacementStep_eq_of_ne

L566 ↗

LubinTate.SameUniformizer.coeff_replacementStep_eq_of_ne

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_replacementStep_eq_of_ne
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (target : MvPowerSeries sigma F.valuationSubring)
    (H : Approximation (F := F) L)
    (q d : {d : sigma →₀ ℕ // d.degree = m})
    (hqd : q ≠ d) :
    MvPowerSeries.coeff q.1 (replacementStep hm target H d).1 =
      MvPowerSeries.coeff q.1 H.1

theorem

coeff_replaceList_eq_of_degree_lt

L580 ↗

LubinTate.SameUniformizer.coeff_replaceList_eq_of_degree_lt

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_replaceList_eq_of_degree_lt
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (target : MvPowerSeries sigma F.valuationSubring)
    (ds : List {d : sigma →₀ ℕ // d.degree = m})
    (H : Approximation (F := F) L)
    (q : sigma →₀ ℕ) (hq : q.degree < m) :
    MvPowerSeries.coeff q (replaceList hm target ds H).1 =
      MvPowerSeries.coeff q H.1

theorem

coeff_replaceList_eq_of_not_mem

L611 ↗

LubinTate.SameUniformizer.coeff_replaceList_eq_of_not_mem

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_replaceList_eq_of_not_mem
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (target : MvPowerSeries sigma F.valuationSubring)
    (ds : List {d : sigma →₀ ℕ // d.degree = m})
    (H : Approximation (F := F) L)
    (q : {d : sigma →₀ ℕ // d.degree = m})
    (hq : q ∉ ds) :
    MvPowerSeries.coeff q.1 (replaceList hm target ds H).1 =
      MvPowerSeries.coeff q.1 H.1

theorem

coeff_replaceList_eq_target_of_mem

L645 ↗

LubinTate.SameUniformizer.coeff_replaceList_eq_target_of_mem

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_replaceList_eq_target_of_mem
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (target : MvPowerSeries sigma F.valuationSubring)
    (ds : List {d : sigma →₀ ℕ // d.degree = m})
    (H : Approximation (F := F) L)
    (hds : ds.Nodup)
    (q : {d : sigma →₀ ℕ // d.degree = m})
    (hq : q ∈ ds) :
    MvPowerSeries.coeff q.1 (replaceList hm target ds H).1 =
      MvPowerSeries.coeff q.1 target

theorem

coeff_defect_replacementStep_eq_of_ne

L686 ↗

LubinTate.SameUniformizer.coeff_defect_replacementStep_eq_of_ne

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_defect_replacementStep_eq_of_ne
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (target : MvPowerSeries sigma F.valuationSubring)
    (H : Approximation (F := F) L)
    (q d : {d : sigma →₀ ℕ // d.degree = m})
    (hqd : q ≠ d) :
    MvPowerSeries.coeff q.1
        (defect e ebar (replacementStep hm target H d).1) =
      MvPowerSeries.coeff q.1 (defect e ebar H.1)

theorem

coeff_defect_replaceList_eq_of_not_mem

L709 ↗

LubinTate.SameUniformizer.coeff_defect_replaceList_eq_of_not_mem

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_defect_replaceList_eq_of_not_mem
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (target : MvPowerSeries sigma F.valuationSubring)
    (ds : List {d : sigma →₀ ℕ // d.degree = m})
    (H : Approximation (F := F) L)
    (q : {d : sigma →₀ ℕ // d.degree = m})
    (hq : q ∉ ds) :
    MvPowerSeries.coeff q.1
        (defect e ebar (replaceList hm target ds H).1) =
      MvPowerSeries.coeff q.1 (defect e ebar H.1)

theorem

coeff_defect_replaceList_of_mem

L749 ↗

LubinTate.SameUniformizer.coeff_defect_replaceList_of_mem

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_defect_replaceList_of_mem
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    {m : ℕ} (hm : 2 ≤ m)
    (target : MvPowerSeries sigma F.valuationSubring)
    (ds : List {d : sigma →₀ ℕ // d.degree = m})
    (H : Approximation (F := F) L)
    (hds : ds.Nodup)
    (q : {d : sigma →₀ ℕ // d.degree = m})
    (hq : q ∈ ds) :
    MvPowerSeries.coeff q.1
        (defect e ebar (replaceList hm target ds H).1) =
      MvPowerSeries.coeff q.1 (defect e ebar H.1) +
        pi * ((1 - pi ^ (m - 1)) *
          (MvPowerSeries.coeff q.1 target -
            MvPowerSeries.coeff q.1 H.1))

def

replaceDegree

L839 ↗

LubinTate.SameUniformizer.replaceDegree

Documentation

Replace every coefficient of one total degree by the corresponding coefficient of a target series.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

def replaceDegree
    {L : sigma → F.valuationSubring}
    (target : MvPowerSeries sigma F.valuationSubring)
    (H : Approximation (F := F) L)
    (m : ℕ) (hm : 2 ≤ m) :
    Approximation (F := F) L

theorem

coeff_replaceDegree_eq_target_of_degree_le

L847 ↗

LubinTate.SameUniformizer.coeff_replaceDegree_eq_target_of_degree_le

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_replaceDegree_eq_target_of_degree_le
    {L : sigma → F.valuationSubring}
    (target : MvPowerSeries sigma F.valuationSubring)
    (H : Approximation (F := F) L)
    (m : ℕ) (hm : 2 ≤ m)
    (hlower : ∀ q : sigma →₀ ℕ, q.degree < m →
      MvPowerSeries.coeff q H.1 =
        MvPowerSeries.coeff q target)
    (q : sigma →₀ ℕ) (hq : q.degree ≤ m) :
    MvPowerSeries.coeff q (replaceDegree target H m hm).1 =
      MvPowerSeries.coeff q target

theorem

coeff_defect_replaceDegree

L873 ↗

LubinTate.SameUniformizer.coeff_defect_replaceDegree

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_defect_replaceDegree
    (e ebar : LubinTateSeries F pi)
    {L : sigma → F.valuationSubring}
    (target : MvPowerSeries sigma F.valuationSubring)
    (H : Approximation (F := F) L)
    (m : ℕ) (hm : 2 ≤ m)
    (q : sigma →₀ ℕ) (hq : q.degree = m) :
    MvPowerSeries.coeff q
        (defect e ebar (replaceDegree target H m hm).1) =
      MvPowerSeries.coeff q (defect e ebar H.1) +
        pi * ((1 - pi ^ (m - 1)) *
          (MvPowerSeries.coeff q target -
            MvPowerSeries.coeff q H.1))

theorem

coeff_eq_linearForm_of_hasLinearTerm

L893 ↗

LubinTate.SameUniformizer.coeff_eq_linearForm_of_hasLinearTerm

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem coeff_eq_linearForm_of_hasLinearTerm
    {H : MvPowerSeries sigma F.valuationSubring}
    {L : sigma → F.valuationSubring}
    (hH : HasLinearTerm H L)
    (d : sigma →₀ ℕ) (hd : d.degree < 2) :
    MvPowerSeries.coeff d H =
      MvPowerSeries.coeff d (linearForm L)

theorem

eq_recursiveIntertwiner_of_hasLinearTerm_of_intertwines

L909 ↗

LubinTate.SameUniformizer.eq_recursiveIntertwiner_of_hasLinearTerm_of_intertwines

Documentation

Any intertwiner with a prescribed linear term is the recursively constructed intertwiner.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem eq_recursiveIntertwiner_of_hasLinearTerm_of_intertwines
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring)
    {H : MvPowerSeries sigma F.valuationSubring}
    (hH : HasLinearTerm H L)
    (hI : Intertwines e ebar H) :
    H = recursiveIntertwiner hpi e ebar L

theorem

eq_of_hasLinearTerm_of_intertwines

L1004 ↗

LubinTate.SameUniformizer.eq_of_hasLinearTerm_of_intertwines

Documentation

Two same-uniformizer intertwiners with the same prescribed linear term are equal.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem eq_of_hasLinearTerm_of_intertwines
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring)
    {H H' : MvPowerSeries sigma F.valuationSubring}
    (hH : HasLinearTerm H L) (hI : Intertwines e ebar H)
    (hH' : HasLinearTerm H' L) (hI' : Intertwines e ebar H') :
    H = H'

theorem

existsUnique_intertwiner

L1019 ↗

LubinTate.SameUniformizer.existsUnique_intertwiner

Documentation

There is a unique same-uniformizer intertwiner with any prescribed linear term.

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} {pi : F.valuationSubring}
variable {sigma : Type w} [Fintype sigma]

Lean source · statement

theorem existsUnique_intertwiner
    (hpi : F.toCompleteDVF.valuation.IsUniformizer (pi : K))
    (e ebar : LubinTateSeries F pi)
    (L : sigma → F.valuationSubring) :
    ∃! H : MvPowerSeries sigma F.valuationSubring,
      HasLinearTerm H L ∧ Intertwines e ebar H

Module documentation

Finite-degree approximations to Lubin--Tate intertwiners

Declarations