NYLL
Module

LubinTateEndomorphism.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FormalModule.LubinTateEndomorphism
18 declarations indexed from sourceView source ↗

Module documentation

The equal-characteristic Lubin–Tate action: the equal-characteristic Lubin--Tate endomorphism

After identifying an equal-characteristic local field with κ((T)), the Lubin--Tate polynomial used in the equal-characteristic construction is

e(Y) = Y ^ q + T * Y, where q = #κ.

This file constructs e as an actual additive endomorphism and constructs the finite bracket

[a]_<n> = ∑_{i<n} a_i e^i, for a = ∑ a_i T^i.

Thus the unit action used below is the genuine Lubin--Tate action, not ordinary scalar multiplication in the ambient field.

Imports4
Imported by4

Declarations

theorem

addMonoidEnd_mul_apply

L44 ↗
LubinTate.EqualCharacteristic.addMonoidEnd_mul_apply
Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem addMonoidEnd_mul_apply
    {R : Type*} [AddCommMonoid R]
    (f g : AddMonoid.End R) (x : R) :
    (f * g) x = f (g x)
theorem

addMonoidEnd_sum_apply

L50 ↗
LubinTate.EqualCharacteristic.addMonoidEnd_sum_apply
Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem addMonoidEnd_sum_apply
    {R : Type*} [AddCommMonoid R] {I : Type*}
    (s : Finset I) (f : I → AddMonoid.End R) (x : R) :
    (∑ i ∈ s, f i) x = ∑ i ∈ s, f i x
instance

equalCharacteristicLaurentCharP

L62 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentCharP
Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
instance equalCharacteristicLaurentCharP
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic] :
    CharP F.residueField⸨X⸩ F.residueCharacteristic
def

equalCharacteristicLubinTatePiEnd

L73 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiEnd
Documentation

The additive Lubin--Tate endomorphism Y ↦ Y^q + T Y on κ((T)). The q-power map is the Frobenius iterate supplied by the residue-cardinality formula from the general Lubin–Tate construction.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · full declaration
def equalCharacteristicLubinTatePiEnd
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic] :
    AddMonoid.End F.residueField⸨X⸩ where
  toFun x :=
    iterateFrobenius F.residueField⸨X⸩ F.residueCharacteristic
        (CompleteDVF.higherPrincipalUnitGroup.iwasawaResidueRank F) x +
      equalCharacteristicLaurentUniformizer F * x
  map_zero' := by simp
  map_add' x y := by
    rw [(iterateFrobenius F.residueField⸨X⸩ F.residueCharacteristic
      (CompleteDVF.higherPrincipalUnitGroup.iwasawaResidueRank F)).map_add,
      mul_add]
    abel
theorem

equalCharacteristicLubinTatePiEnd_apply

L93 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiEnd_apply
Documentation

The Lubin–Tate π-endomorphism is Frobenius plus uniformizer multiplication.

Source context 8 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup (
  residueField_card_eq_residueCharacteristic_pow_iwasawaResidueRank
) in
Lean source · statement
theorem equalCharacteristicLubinTatePiEnd_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTatePiEnd F x =
      x ^ Nat.card F.residueField +
        equalCharacteristicLaurentUniformizer F * x
def

equalCharacteristicCoefficientEnd

L109 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCoefficientEnd
Documentation

Multiplication by a residue-field coefficient, regarded as an additive endomorphism of the Laurent-series field.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · full declaration
def equalCharacteristicCoefficientEnd
    (F : LocalField.{u, v} K) (a : F.residueField) :
    AddMonoid.End F.residueField⸨X⸩ where
  toFun x :=
    algebraMap F.residueField F.residueField⸨X⸩ a * x
  map_zero' := mul_zero _
  map_add' := mul_add _
theorem

equalCharacteristicCoefficientEnd_apply

L119 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCoefficientEnd_apply
Documentation

A residue coefficient endomorphism acts by scalar multiplication.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicCoefficientEnd_apply
    (F : LocalField.{u, v} K) (a : F.residueField)
    (x : F.residueField⸨X⸩) :
    equalCharacteristicCoefficientEnd F a x =
      algebraMap F.residueField F.residueField⸨X⸩ a * x
theorem

equalCharacteristicLubinTatePiEnd_coefficient_mul

L128 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiEnd_coefficient_mul
Documentation

The distinguished endomorphism commutes with the genuine coefficient action.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiEnd_coefficient_mul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField) (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTatePiEnd F
        (algebraMap F.residueField F.residueField⸨X⸩ a * x) =
      algebraMap F.residueField F.residueField⸨X⸩ a *
        equalCharacteristicLubinTatePiEnd F x
def

equalCharacteristicLubinTatePiIterate

L145 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiIterate
Documentation

The i-fold iterate of the distinguished Lubin--Tate endomorphism.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTatePiIterate
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (i : ℕ) : AddMonoid.End F.residueField⸨X⸩
theorem

equalCharacteristicLubinTatePiIterate_zero

L153 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiIterate_zero
Documentation

The zeroth Lubin–Tate π-iterate is the identity.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiIterate_zero
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTatePiIterate F 0 x = x
theorem

equalCharacteristicLubinTatePiIterate_succ

L162 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiIterate_succ
Documentation

A successor π-iterate applies one more Lubin–Tate π-endomorphism.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiIterate_succ
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (i : ℕ) (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTatePiIterate F (i + 1) x =
      equalCharacteristicLubinTatePiIterate F i
        (equalCharacteristicLubinTatePiEnd F x)
theorem

equalCharacteristicLubinTatePiIterate_coefficient_mul

L178 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiIterate_coefficient_mul
Documentation

Every iterate of e commutes with multiplication by a residue-field coefficient.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePiIterate_coefficient_mul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (i : ℕ) (a : F.residueField) (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTatePiIterate F i
        (algebraMap F.residueField F.residueField⸨X⸩ a * x) =
      algebraMap F.residueField F.residueField⸨X⸩ a *
        equalCharacteristicLubinTatePiIterate F i x
def

equalCharacteristicLubinTateBracket

L196 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracket
Documentation

The genuine finite-level bracket [a]_<n> = ∑_{i<n} a_i e^i.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTateBracket
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧) :
    AddMonoid.End F.residueField⸨X⸩
theorem

equalCharacteristicLubinTateBracket_apply

L206 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracket_apply
Documentation

Lubin–Tate bracket evaluation expands as the coefficient-and-iterate sum.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateBracket_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧)
    (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTateBracket F n a x =
      ∑ i ∈ Finset.range n,
        algebraMap F.residueField F.residueField⸨X⸩
            (PowerSeries.coeff i a) *
          equalCharacteristicLubinTatePiIterate F i x
theorem

equalCharacteristicLubinTateBracket_zero

L226 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracket_zero
Documentation

The Lubin–Tate bracket of the zero series is the zero endomorphism.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateBracket_zero
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateBracket F n 0 = 0
theorem

equalCharacteristicLubinTateBracket_add

L241 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracket_add
Documentation

The Lubin–Tate bracket is additive in its power-series parameter.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateBracket_add
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a b : F.residueField⟦X⟧) :
    equalCharacteristicLubinTateBracket F n (a + b) =
      equalCharacteristicLubinTateBracket F n a +
        equalCharacteristicLubinTateBracket F n b
theorem

equalCharacteristicLubinTateBracket_C

L266 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracket_C
Documentation

The bracket of a constant power series is its coefficient endomorphism.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateBracket_C
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField) :
    equalCharacteristicLubinTateBracket F (n + 1) (PowerSeries.C a) =
      equalCharacteristicCoefficientEnd F a
theorem

equalCharacteristicLubinTateBracket_X

L290 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracket_X
Documentation

The bracket of X is the Lubin–Tate π-endomorphism.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateBracket_X
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateBracket F (n + 2)
        (PowerSeries.X : F.residueField⟦X⟧) =
      equalCharacteristicLubinTatePiEnd F

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