NYLL
Module

Reduction.lean

Nyll.ClassFieldTheory.LubinTate.FormalModule.Reduction
6 declarations indexed from sourceView source ↗

Module documentation

Reduction of a Lubin--Tate intertwining defect

After reduction to the finite residue field, both series become the Frobenius power series. The two sides of the intertwining equation then agree, so every coefficient of the defect is divisible by the chosen uniformizer.

Imports5
Imported by2

Declarations

theorem

mvPowerSeries_expand_natCard

L34 ↗
LubinTate.SameUniformizer.mvPowerSeries_expand_natCard
Documentation

Multivariable finite-field Frobenius: replacing each variable by its qth power is the same as taking the qth power of the whole series.

Source context 5 commands

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

noncomputable section
universe u v w
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem mvPowerSeries_expand_natCard
    {k : Type u} [Field k] [Finite k]
    {σ : Type w} [Finite σ] (f : MvPowerSeries σ k) :
    MvPowerSeries.expand (Nat.card k) (Nat.ne_of_gt Nat.card_pos) f =
      f ^ Nat.card k
theorem

map_inVariable

L63 ↗
LubinTate.SameUniformizer.map_inVariable
Documentation

Reduction of e(X_i) is X_i ^ q.

Source context 9 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 σ]
omit [Fintype σ] in
Lean source · statement
theorem map_inVariable (e : LubinTateSeries F π) (i : σ) :
    MvPowerSeries.map F.residueMap (inVariable e i) =
      (MvPowerSeries.X i : MvPowerSeries σ F.residueField) ^
        Nat.card F.residueField
theorem

map_subst_lubinTateSeries

L78 ↗
LubinTate.SameUniformizer.map_subst_lubinTateSeries
Documentation

The reduced left side e(H) is Hbar ^ q.

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 map_subst_lubinTateSeries
    (e : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L) :
    MvPowerSeries.map F.residueMap
        (PowerSeries.subst H e.toPowerSeries) =
      (MvPowerSeries.map F.residueMap H) ^
        Nat.card F.residueField
theorem

map_subst_inVariables

L97 ↗
LubinTate.SameUniformizer.map_subst_inVariables
Documentation

The reduced right side H(ebar(X_i)) is the expansion Hbar(X_i ^ q).

Source context 9 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 σ]
omit [Fintype σ] in
Lean source · full declaration
theorem map_subst_inVariables [Finite σ]
    (ebar : LubinTateSeries F π)
    (H : MvPowerSeries σ F.valuationSubring) :
    MvPowerSeries.map F.residueMap
        (MvPowerSeries.subst
          (fun i : σ ↦ inVariable ebar i) H) =
      MvPowerSeries.expand (Nat.card F.residueField)
        (Nat.ne_of_gt Nat.card_pos)
        (MvPowerSeries.map F.residueMap H) := by
  rw [MvPowerSeries.map_subst (inVariable_hasSubst ebar) H]
  simp_rw [map_inVariable]
  rw [MvPowerSeries.expand, MvPowerSeries.substAlgHom_apply]
theorem

map_defect_eq_zero

L111 ↗
LubinTate.SameUniformizer.map_defect_eq_zero
Documentation

The same-uniformizer intertwining defect vanishes after reduction.

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 map_defect_eq_zero
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L) :
    MvPowerSeries.map F.residueMap (defect e ebar H) = 0
theorem

uniformizer_dvd_coeff_defect

L123 ↗
LubinTate.SameUniformizer.uniformizer_dvd_coeff_defect
Documentation

Every coefficient of the defect is divisible by 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
theorem uniformizer_dvd_coeff_defect
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) :
    π ∣ MvPowerSeries.coeff d (defect e ebar H)

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