NYLL
Module

CompleteDVRExpansion.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.CompleteDVRExpansion
23 declarations indexed from sourceView source ↗

Module documentation

Coefficients for a complete DVR expansion

This file formalizes the recursive coefficient construction in the recursive coefficient proof. Given a section of the residue map and a uniformizer π, every element of the valuation ring has uniquely determined successive representative coefficients and remainders satisfying

u = a 0 + a 1 * π + ... + a (n - 1) * π ^ (n - 1) + π ^ n * b n.

Imports3
Imported by2

Declarations

structure

residueRepresentativeSystemOf

L36 ↗
LubinTate.Valuations.residueRepresentativeSystemOf
Documentation

A normalized system of representatives for the residue field of a local ring. This common structure is used both for the original valuation ring and for the valuation ring in its completion.

Source context 5 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
Lean source · full declaration
structure residueRepresentativeSystemOf
    (O : Type u) [CommRing O] [IsLocalRing O] where
  /-- The chosen representative of each residue class. -/
  repr : IsLocalRing.ResidueField O → O
  /-- Reducing a chosen representative recovers its residue class. -/
  residue_repr : ∀ a : IsLocalRing.ResidueField O,
    IsLocalRing.residue O (repr a) = a
  /-- The zero residue class is represented by zero. -/
  repr_zero : repr 0 = 0
def

ofChoice

L52 ↗
LubinTate.Valuations.residueRepresentativeSystemOf.ofChoice
Documentation

A normalized representative system exists by surjectivity of the residue map.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
namespace residueRepresentativeSystemOf
variable (O : Type u) [CommRing O] [IsLocalRing O]
Lean source · statement
def ofChoice : residueRepresentativeSystemOf O
abbrev

residueRepresentativeSystem

L70 ↗
LubinTate.Valuations.residueRepresentativeSystem
Documentation

A system of representatives for the residue field of a complete DVF valuation ring, encoded as a section of the residue map and normalized at zero.

Source context 5 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
Lean source · statement
abbrev residueRepresentativeSystem
    {K : Type u} [Field K]
    (F : CompleteDVF.{u, v} K)
def

ofChoice

L81 ↗
LubinTate.Valuations.residueRepresentativeSystem.ofChoice
Documentation

A representative system exists by surjectivity of the residue map.

Source context 8 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
namespace residueRepresentativeSystem
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
def ofChoice : residueRepresentativeSystem F
theorem

exists_remainder_step

L91 ↗
LubinTate.Valuations.exists_remainder_step
Documentation

One step of the digit expansion: subtract the chosen residue representative, then divide by the uniformizer.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem exists_remainder_step
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (r : F.valuationSubring) :
    ∃ b : F.valuationSubring,
      r = R.repr (F.residueMap r) + π * b
def

remainder

L113 ↗
LubinTate.Valuations.remainder
Documentation

The recursively defined remainders in the expansion of u.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · full declaration
def remainder
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (u : F.valuationSubring) :
    ℕ → F.valuationSubring
  | 0 => u
  | n + 1 =>
      Classical.choose
        (exists_remainder_step F R π hπ
          (remainder R π hπ u n))
def

coeff

L126 ↗
LubinTate.Valuations.coeff
Documentation

The recursively defined representative coefficients in the expansion of u.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
def coeff
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (u : F.valuationSubring) (n : ℕ) :
    F.valuationSubring
theorem

remainder_step

L134 ↗
LubinTate.Valuations.remainder_step
Documentation

The defining recursion for the remainders and coefficients.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem remainder_step
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (u : F.valuationSubring) (n : ℕ) :
    remainder F R π hπ u n =
      coeff F R π hπ u n +
        π * remainder F R π hπ u (n + 1)
theorem

residueMap_add_uniformizer_mul

L147 ↗
LubinTate.Valuations.residueMap_add_uniformizer_mul
Documentation

Adding a multiple of the uniformizer does not change the residue class.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem residueMap_add_uniformizer_mul
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (a b : F.valuationSubring) :
    F.residueMap (a + π * b) = F.residueMap a
theorem

coeff_remainder_unique

L157 ↗
LubinTate.Valuations.coeff_remainder_unique
Documentation

Recursive uniqueness of the coefficient and remainder sequences in the valuation-ring part of the complete-DVR expansion.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem coeff_remainder_unique
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (u : F.valuationSubring)
    (c b : ℕ → F.valuationSubring)
    (hb0 : b 0 = u)
    (hstep : ∀ n : ℕ, b n = c n + π * b (n + 1))
    (hcoeff_repr : ∀ n : ℕ, ∃ a : F.residueField, c n = R.repr a) :
    ∀ n : ℕ,
      b n = remainder F R π hπ u n ∧
        c n = coeff F R π hπ u n
theorem

exists_laurent_unit

L219 ↗
LubinTate.Valuations.exists_laurent_unit
Documentation

Laurent-unit decomposition in a complete DVF: every nonzero field element is a power of the chosen uniformizer times a valuation-ring unit.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem exists_laurent_unit
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    {x : K} (hx : x ≠ 0) :
    ∃ m : ℤ, ∃ u : F.valuationSubring,
      IsUnit u ∧ x = (π : K) ^ m * (u : K)
theorem

laurent_exponent_unique

L292 ↗
LubinTate.Valuations.laurent_exponent_unique
Documentation

The uniformizer exponent in a Laurent-unit decomposition is unique.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem laurent_exponent_unique
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    {m n : ℤ} {u w : F.valuationSubring}
    (hu : IsUnit u) (hw : IsUnit w)
    (h : (π : K) ^ m * (u : K) = (π : K) ^ n * (w : K)) :
    m = n
theorem

laurent_unit_unique

L318 ↗
LubinTate.Valuations.laurent_unit_unique
Documentation

The Laurent-unit part of the complete-DVR expansion is unique: if two unit decompositions with powers of the same uniformizer represent the same field element, then both the exponent and the unit agree.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem laurent_unit_unique
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    {m n : ℤ} {u w : F.valuationSubring}
    (hu : IsUnit u) (hw : IsUnit w)
    (h : (π : K) ^ m * (u : K) = (π : K) ^ n * (w : K)) :
    m = n ∧ u = w
def

partialSum

L332 ↗
LubinTate.Valuations.partialSum
Documentation

Finite partial sums of the π-adic representative expansion.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · full declaration
def partialSum
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (u : F.valuationSubring) :
    ℕ → F.valuationSubring
  | 0 => 0
  | n + 1 =>
      partialSum R π hπ u n +
        coeff F R π hπ u n * π ^ n
theorem

partialSum_add_remainder

L343 ↗
LubinTate.Valuations.partialSum_add_remainder
Documentation

Finite-stage expansion with a remainder term.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem partialSum_add_remainder
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (u : F.valuationSubring) (n : ℕ) :
    u =
      partialSum F R π hπ u n +
        π ^ n * remainder F R π hπ u n
theorem

partialSum_congr

L379 ↗
LubinTate.Valuations.partialSum_congr
Documentation

The finite expansion gives the correct residue modulo π ^ n.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem partialSum_congr
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (u : F.valuationSubring) (n : ℕ) :
    u - partialSum F R π hπ u n ∈ F.maximalIdeal ^ n
def

PartialSumsConvergeAdically

L405 ↗
LubinTate.Valuations.PartialSumsConvergeAdically
Documentation

Convergence of the finite partial sums in the maximal-ideal adic topology, represented on a type-level topological copy of the valuation ring.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
def PartialSumsConvergeAdically
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (u : F.valuationSubring) : Prop
theorem

partialSum_tendsto_adic

L419 ↗
LubinTate.Valuations.partialSum_tendsto_adic
Documentation

The finite partial sums converge to u in the type-level model of the maximal-ideal adic topology.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem partialSum_tendsto_adic
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (u : F.valuationSubring) :
    PartialSumsConvergeAdically F R π hπ u
theorem

residue_coeff

L448 ↗
LubinTate.Valuations.residue_coeff
Documentation

The residue of each coefficient is the residue of the corresponding remainder.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem residue_coeff
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (u : F.valuationSubring) (n : ℕ) :
      F.residueMap (coeff F R π hπ u n) =
      F.residueMap (remainder F R π hπ u n)
theorem

coeff_zero_ne_zero_of_isUnit

L457 ↗
LubinTate.Valuations.coeff_zero_ne_zero_of_isUnit
Documentation

The first digit of a unit is nonzero.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem coeff_zero_ne_zero_of_isUnit
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    {u : F.valuationSubring} (hu : IsUnit u) :
    coeff F R π hπ u 0 ≠ 0
theorem

exists_laurent_expansion_data

L478 ↗
LubinTate.Valuations.exists_laurent_expansion_data
Documentation

The complete-DVR expansion, existence-side Laurent expansion data for a nonzero field element: after extracting the uniformizer power, the unit part has a convergent representative expansion with nonzero first digit.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem exists_laurent_expansion_data
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    {x : K} (hx : x ≠ 0) :
    ∃ m : ℤ, ∃ u : F.valuationSubring,
      IsUnit u ∧
        x = (π : K) ^ m * (u : K) ∧
        coeff F R π hπ u 0 ≠ 0 ∧
        PartialSumsConvergeAdically F R π hπ u ∧
        ∀ n : ℕ,
          x =
            (π : K) ^ m *
              (((partialSum F R π hπ u n +
                π ^ n * remainder F R π hπ u n) :
                  F.valuationSubring) : K)
def

isLaurentExpansion

L511 ↗
LubinTate.Valuations.isLaurentExpansion
Documentation

The complete-DVR expansion, the canonical Laurent-series representation predicate. The element x is represented as π^m * (a₀ + a₁π + a₂π² + ⋯), where the coefficients are the canonical representatives attached to the unit part u.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
def isLaurentExpansion
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    (x : K) (m : ℤ) (u : F.valuationSubring) : Prop
theorem

exists_unique_laurent_expansion

L529 ↗
LubinTate.Valuations.exists_unique_laurent_expansion
Documentation

The complete-DVR expansion, public form: every nonzero element of a complete discretely valued field has a unique convergent Laurent expansion with respect to the chosen uniformizer and residue representative system.

Source context 7 commands

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

noncomputable section
namespace LubinTate
namespace Valuations
universe u v
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable (F : CompleteDVF.{u, v} K)
Lean source · statement
theorem exists_unique_laurent_expansion
    (R : residueRepresentativeSystem F)
    (π : F.valuationSubring) (hπ : F.valuation.IsUniformizer (π : K))
    {x : K} (hx : x ≠ 0) :
    ∃! p : ℤ × F.valuationSubring,
      isLaurentExpansion F R π hπ x p.1 p.2

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.