Module

DefectCorrection.lean

Nyll.ClassFieldTheory.LubinTate.Padic.ChangedUniformizerIntertwiner.DefectCorrection

20 declarations indexed from sourceView source ↗

Module documentation

Changed-uniformizer defect correction

This module computes how a degreewise correction changes the semilinear substitution defect and constructs the unique coefficient that kills that defect.

Imports5

Nyll.ClassFieldTheory.LubinTate.Padic.ChangedUniformizerIntertwiner.CompletedSeries
Nyll.ClassFieldTheory.LubinTate.Padic.ChangedUniformizerCoefficient
Mathlib.RingTheory.PowerSeries.Expand
Mathlib.RingTheory.PowerSeries.Order
Mathlib.RingTheory.PowerSeries.Trunc

Imported by4

def

padicChangedUniformizerDefect

L33 ↗

LubinTate.padicChangedUniformizerDefect

Documentation

The defect of a candidate changed-uniformizer intertwiner: the difference between its Frobenius-twisted multiplicative substitution and its changed-standard substitution.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

def padicChangedUniformizerDefect
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (H : PowerSeries (padicCompletedUnramifiedWittRing p)) :
    PowerSeries (padicCompletedUnramifiedWittRing p)

theorem

padicChangedUniformizerFrobenius_map_constantCoeff

L46 ↗

LubinTate.padicChangedUniformizerFrobenius_map_constantCoeff

Documentation

Reduction modulo p commutes with coefficientwise Witt-vector Frobenius through residue-field Frobenius.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizerFrobenius_map_constantCoeff
    (p : ℕ) [Fact p.Prime]
    (H : PowerSeries (padicCompletedUnramifiedWittRing p)) :
    PowerSeries.map WittVector.constantCoeff
        (PowerSeries.map WittVector.frobenius H) =
      PowerSeries.map
        (frobenius (AlgebraicClosure (ZMod p)) p)
        (PowerSeries.map WittVector.constantCoeff H)

theorem

padicChangedUniformizerDefect_map_constantCoeff

L61 ↗

LubinTate.padicChangedUniformizerDefect_map_constantCoeff

Documentation

The changed-uniformizer defect vanishes after coefficientwise reduction modulo p.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizerDefect_map_constantCoeff
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0) :
    PowerSeries.map WittVector.constantCoeff
        (padicChangedUniformizerDefect p u H) = 0

theorem

padicChangedUniformizerDefect_coeff_mem_span_p

L124 ↗

LubinTate.padicChangedUniformizerDefect_coeff_mem_span_p

Documentation

Every coefficient of the changed-uniformizer defect is divisible by p in the completed unramified Witt ring.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizerDefect_coeff_mem_span_p
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0)
    (m : ℕ) :
    PowerSeries.coeff m (padicChangedUniformizerDefect p u H) ∈
      Ideal.span ({(p : padicCompletedUnramifiedWittRing p)} : Set _)

theorem

exists_padicChangedUniformizerNormalizedDefect

L141 ↗

LubinTate.exists_padicChangedUniformizerNormalizedDefect

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem exists_padicChangedUniformizerNormalizedDefect
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0)
    (m : ℕ) :
    ∃ b : padicCompletedUnramifiedWittRing p,
      (p : padicCompletedUnramifiedWittRing p) * b =
        PowerSeries.coeff m
          (padicChangedUniformizerDefect p u H)

def

padicChangedUniformizerNormalizedDefect

L157 ↗

LubinTate.padicChangedUniformizerNormalizedDefect

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

def padicChangedUniformizerNormalizedDefect
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0)
    (m : ℕ) :
    padicCompletedUnramifiedWittRing p

theorem

padicChangedUniformizerNormalizedDefect_spec

L167 ↗

LubinTate.padicChangedUniformizerNormalizedDefect_spec

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizerNormalizedDefect_spec
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0)
    (m : ℕ) :
    (p : padicCompletedUnramifiedWittRing p) *
        padicChangedUniformizerNormalizedDefect p u H hH m =
      PowerSeries.coeff m
        (padicChangedUniformizerDefect p u H)

theorem

padicCompletedMultiplicativeSeries_order

L181 ↗

LubinTate.padicCompletedMultiplicativeSeries_order

Documentation

The completed multiplicative Lubin--Tate series has order one.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicCompletedMultiplicativeSeries_order
    (p : ℕ) [Fact p.Prime] :
    (padicCompletedMultiplicativeSeries p).order = 1

theorem

padicCompletedMultiplicativeSeries_coeff_pow_self

L197 ↗

LubinTate.padicCompletedMultiplicativeSeries_coeff_pow_self

Documentation

The degree-m coefficient of the m-th power of the completed multiplicative series is p ^ m.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicCompletedMultiplicativeSeries_coeff_pow_self
    (p : ℕ) [Fact p.Prime] (m : ℕ) :
    PowerSeries.coeff m
        ((padicCompletedMultiplicativeSeries p) ^ m) =
      (p : padicCompletedUnramifiedWittRing p) ^ m

theorem

padicChangedUniformizer_coeff_pow_add_monomial

L226 ↗

LubinTate.padicChangedUniformizer_coeff_pow_add_monomial

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizer_coeff_pow_add_monomial
    (p : ℕ) [Fact p.Prime]
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0)
    (m : ℕ) (hm : 2 ≤ m)
    (c : padicCompletedUnramifiedWittRing p) :
    PowerSeries.coeff m
        ((H + PowerSeries.monomial m c) ^ p) =
      PowerSeries.coeff m (H ^ p)

theorem

padicChangedUniformizer_subst_monomial

L321 ↗

LubinTate.padicChangedUniformizer_subst_monomial

Documentation

Substituting the completed multiplicative series into a monomial scales its m-th power by the monomial coefficient.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizer_subst_monomial
    (p : ℕ) [Fact p.Prime]
    (m : ℕ) (c : padicCompletedUnramifiedWittRing p) :
    PowerSeries.subst
        (padicCompletedMultiplicativeSeries p)
        (PowerSeries.monomial m c) =
      PowerSeries.C c *
        (padicCompletedMultiplicativeSeries p) ^ m

theorem

padicChangedUniformizerFrobenius_add_monomial

L340 ↗

LubinTate.padicChangedUniformizerFrobenius_add_monomial

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem
    padicChangedUniformizerFrobenius_add_monomial
    (p : ℕ) [Fact p.Prime]
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (m : ℕ) (c : padicCompletedUnramifiedWittRing p) :
    PowerSeries.map WittVector.frobenius
        (H + PowerSeries.monomial m c) =
      PowerSeries.map WittVector.frobenius H +
        PowerSeries.monomial m (WittVector.frobenius c)

theorem

padicChangedUniformizer_coeff_subst_frobenius_add_monomial

L356 ↗

LubinTate.padicChangedUniformizer_coeff_subst_frobenius_add_monomial

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizer_coeff_subst_frobenius_add_monomial
    (p : ℕ) [Fact p.Prime]
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (m : ℕ) (c : padicCompletedUnramifiedWittRing p) :
    PowerSeries.coeff m
        (PowerSeries.subst
          (padicCompletedMultiplicativeSeries p)
          (PowerSeries.map WittVector.frobenius
            (H + PowerSeries.monomial m c))) =
      PowerSeries.coeff m
          (PowerSeries.subst
            (padicCompletedMultiplicativeSeries p)
            (PowerSeries.map WittVector.frobenius H)) +
        (p : padicCompletedUnramifiedWittRing p) ^ m *
          WittVector.frobenius c

theorem

padicChangedUniformizer_coeff_subst_changed_add_monomial

L382 ↗

LubinTate.padicChangedUniformizer_coeff_subst_changed_add_monomial

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizer_coeff_subst_changed_add_monomial
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0)
    (m : ℕ) (hm : 2 ≤ m)
    (c : padicCompletedUnramifiedWittRing p) :
    PowerSeries.coeff m
        (PowerSeries.subst
          (H + PowerSeries.monomial m c)
          (padicCompletedChangedStandardSeries p u)) =
      PowerSeries.coeff m
          (PowerSeries.subst H
            (padicCompletedChangedStandardSeries p u)) +
        ((padicValuationUnitToCompletedUnramifiedWittUnit p u) :
            padicCompletedUnramifiedWittRing p) *
          (p : padicCompletedUnramifiedWittRing p) * c

theorem

padicChangedUniformizerDefect_coeff_add_monomial

L445 ↗

LubinTate.padicChangedUniformizerDefect_coeff_add_monomial

Documentation

Adding a monomial in degree m changes the degree-m defect by the explicit Frobenius-linear correction term.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizerDefect_coeff_add_monomial
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0)
    (m : ℕ) (hm : 2 ≤ m)
    (c : padicCompletedUnramifiedWittRing p) :
    PowerSeries.coeff m
        (padicChangedUniformizerDefect p u
          (H + PowerSeries.monomial m c)) =
      PowerSeries.coeff m
          (padicChangedUniformizerDefect p u H) +
        (p : padicCompletedUnramifiedWittRing p) ^ m *
          WittVector.frobenius c -
        ((padicValuationUnitToCompletedUnramifiedWittUnit p u) :
            padicCompletedUnramifiedWittRing p) *
          (p : padicCompletedUnramifiedWittRing p) * c

def

padicChangedUniformizerCorrectionCoefficient

L471 ↗

LubinTate.padicChangedUniformizerCorrectionCoefficient

Documentation

The unique coefficient that corrects the changed-uniformizer defect in degree m.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

def padicChangedUniformizerCorrectionCoefficient
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0)
    (m : ℕ) (hm : 2 ≤ m) :
    padicCompletedUnramifiedWittRing p

theorem

padicChangedUniformizerCorrectionCoefficient_spec

L486 ↗

LubinTate.padicChangedUniformizerCorrectionCoefficient_spec

Documentation

The correction coefficient satisfies its defining Frobenius fixed-point equation.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizerCorrectionCoefficient_spec
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0)
    (m : ℕ) (hm : 2 ≤ m) :
    padicChangedUniformizerCorrectionCoefficient p u H hH m hm =
      (↑((padicValuationUnitToCompletedUnramifiedWittUnit p u)⁻¹) :
          padicCompletedUnramifiedWittRing p) *
        padicChangedUniformizerNormalizedDefect p u H hH m +
      (↑((padicValuationUnitToCompletedUnramifiedWittUnit p u)⁻¹) :
          padicCompletedUnramifiedWittRing p) *
        (p : padicCompletedUnramifiedWittRing p) ^ (m - 1) *
        WittVector.frobenius
          (padicChangedUniformizerCorrectionCoefficient
            p u H hH m hm)

theorem

padicChangedUniformizerCorrectionCoefficient_kills_defect

L510 ↗

LubinTate.padicChangedUniformizerCorrectionCoefficient_kills_defect

Documentation

Adding the correction coefficient in degree m kills the degree-m defect.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizerCorrectionCoefficient_kills_defect
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (H : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hH : PowerSeries.constantCoeff H = 0)
    (m : ℕ) (hm : 2 ≤ m) :
    PowerSeries.coeff m
        (padicChangedUniformizerDefect p u
          (H + PowerSeries.monomial m
            (padicChangedUniformizerCorrectionCoefficient
              p u H hH m hm))) = 0

theorem

powerSeries_truncTotal_succ_eq_of_coeff_eq_le

L576 ↗

LubinTate.powerSeries_truncTotal_succ_eq_of_coeff_eq_le

Documentation

Two one-variable power series have the same total truncation through degree m when their coefficients agree through degree m.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem powerSeries_truncTotal_succ_eq_of_coeff_eq_le
    {R : Type*} [CommRing R]
    {H H' : PowerSeries R} (m : ℕ)
    (hcoeff : ∀ q : ℕ, q ≤ m →
      PowerSeries.coeff q H = PowerSeries.coeff q H') :
    H.truncTotal (m + 1) = H'.truncTotal (m + 1)

theorem

padicChangedUniformizerDefect_coeff_eq_of_coeff_eq_le

L594 ↗

LubinTate.padicChangedUniformizerDefect_coeff_eq_of_coeff_eq_le

Documentation

The degree-m defect depends only on coefficients through degree m.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicChangedUniformizerDefect_coeff_eq_of_coeff_eq_le
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    {H H' : PowerSeries (padicCompletedUnramifiedWittRing p)}
    (hH : PowerSeries.constantCoeff H = 0)
    (hH' : PowerSeries.constantCoeff H' = 0)
    (m : ℕ)
    (hcoeff : ∀ q : ℕ, q ≤ m →
      PowerSeries.coeff q H = PowerSeries.coeff q H') :
    PowerSeries.coeff m
        (padicChangedUniformizerDefect p u H) =
      PowerSeries.coeff m
        (padicChangedUniformizerDefect p u H')

Module documentation

Changed-uniformizer defect correction

Declarations