Module

LubinTateAction.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FormalModule.LubinTateAction

18 declarations indexed from sourceView source ↗

Module documentation

Equal-characteristic Lubin--Tate action

This file proves the algebraic identities needed to turn the finite brackets from EqualCharacteristicLubinTateEnd into the action of (κ⟦T⟧ / T^n)ˣ on the T^n-division points.

Imports1

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FormalModule.LubinTateEndomorphism

Imported by5

theorem

addMonoidHom_map_finset_sum

L32 ↗

LubinTate.EqualCharacteristic.addMonoidHom_map_finset_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 addMonoidHom_map_finset_sum
    {A I : Type*} [AddCommMonoid A]
    (f : AddMonoid.End A) (s : Finset I) (g : I → A) :
    f (∑ i ∈ s, g i) = ∑ i ∈ s, f (g i)

def

equalCharacteristicPowerSeriesTail

L46 ↗

LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesTail

Documentation

Delete the constant coefficient of a power series and shift all remaining coefficients down by one place.

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 equalCharacteristicPowerSeriesTail
    {k : Type*} [Semiring k] (a : k⟦X⟧) : k⟦X⟧

theorem

equalCharacteristicPowerSeriesTail_coeff

L52 ↗

LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesTail_coeff

Documentation

States the theorem equalCharacteristicPowerSeriesTail_coeff.

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 equalCharacteristicPowerSeriesTail_coeff
    {k : Type*} [Semiring k] (a : k⟦X⟧) (i : ℕ) :
    PowerSeries.coeff i (equalCharacteristicPowerSeriesTail a) =
      PowerSeries.coeff (i + 1) a

theorem

equalCharacteristicPowerSeries_eq_X_mul_tail_add_C

L59 ↗

LubinTate.EqualCharacteristic.equalCharacteristicPowerSeries_eq_X_mul_tail_add_C

Documentation

Split a power series into its constant coefficient and shifted tail.

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 equalCharacteristicPowerSeries_eq_X_mul_tail_add_C
    {k : Type*} [Semiring k] (a : k⟦X⟧) :
    a = PowerSeries.X * equalCharacteristicPowerSeriesTail a +
      PowerSeries.C (PowerSeries.coeff 0 a)

theorem

equalCharacteristicPowerSeriesTail_mul

L69 ↗

LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesTail_mul

Documentation

Product rule for the shifted tail: tail(ab) = C(a₀) tail(b) + tail(a)b.

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 equalCharacteristicPowerSeriesTail_mul
    {k : Type*} [CommRing k] (a b : k⟦X⟧) :
    equalCharacteristicPowerSeriesTail (a * b) =
      PowerSeries.C (PowerSeries.coeff 0 a) *
          equalCharacteristicPowerSeriesTail b +
        equalCharacteristicPowerSeriesTail a * b

def

IsEqualCharacteristicLubinTateTorsion

L144 ↗

LubinTate.EqualCharacteristic.IsEqualCharacteristicLubinTateTorsion

Documentation

A point killed by the n-fold distinguished 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 IsEqualCharacteristicLubinTateTorsion
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (x : F.residueField⸨X⸩) : Prop

theorem

equalCharacteristicLubinTatePiIterate_add

L152 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiIterate_add

Documentation

Iterating e i+j times is the same as first iterating j times and then i times.

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_add
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (i j : ℕ) (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTatePiIterate F (i + j) x =
      equalCharacteristicLubinTatePiIterate F i
        (equalCharacteristicLubinTatePiIterate F j x)

theorem

equalCharacteristicLubinTatePiIterate_eq_zero_of_le

L167 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiIterate_eq_zero_of_le

Documentation

A point killed at level n is killed at every higher level.

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_eq_zero_of_le
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {n m : ℕ} (hnm : n ≤ m) (x : F.residueField⸨X⸩)
    (hx : IsEqualCharacteristicLubinTateTorsion F n x) :
    equalCharacteristicLubinTatePiIterate F m x = 0

theorem

equalCharacteristicLubinTatePiEnd_torsion_pred

L177 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiEnd_torsion_pred

Documentation

If x is killed at level n+1, then e(x) is killed at level n.

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_torsion_pred
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (x : F.residueField⸨X⸩)
    (hx : IsEqualCharacteristicLubinTateTorsion F (n + 1) x) :
    IsEqualCharacteristicLubinTateTorsion F n
      (equalCharacteristicLubinTatePiEnd F x)

theorem

equalCharacteristicLubinTateBracket_succ_apply

L187 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracket_succ_apply

Documentation

Recursive evaluation formula for a finite bracket.

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_succ_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧)
    (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTateBracket F (n + 1) a x =
      algebraMap F.residueField F.residueField⸨X⸩
          (PowerSeries.coeff 0 a) * x +
        equalCharacteristicLubinTateBracket F n
          (equalCharacteristicPowerSeriesTail a)
          (equalCharacteristicLubinTatePiEnd F x)

theorem

equalCharacteristicLubinTatePiIterate_one

L211 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiIterate_one

Documentation

States the theorem equalCharacteristicLubinTatePiIterate_one.

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_one
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTatePiIterate F 1 x =
      equalCharacteristicLubinTatePiEnd F x

theorem

equalCharacteristicLubinTatePiEnd_iterate

L220 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiEnd_iterate

Documentation

The distinguished endomorphism commutes with all of its iterates.

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_iterate
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (i : ℕ) (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTatePiEnd F
        (equalCharacteristicLubinTatePiIterate F i x) =
      equalCharacteristicLubinTatePiIterate F i
        (equalCharacteristicLubinTatePiEnd F x)

theorem

equalCharacteristicLubinTateBracket_coefficient_mul_apply

L249 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracket_coefficient_mul_apply

Documentation

A bracket is linear for the residue-field coefficient action on its argument.

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_coefficient_mul_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧) (c : F.residueField)
    (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTateBracket F n a
        (algebraMap F.residueField F.residueField⸨X⸩ c * x) =
      algebraMap F.residueField F.residueField⸨X⸩ c *
        equalCharacteristicLubinTateBracket F n a x

theorem

equalCharacteristicLubinTateBracket_C_mul_apply

L267 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracket_C_mul_apply

Documentation

Multiplying the coefficient series by the constant series C(c) has the same effect as multiplying the bracket value by c.

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_mul_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (c : F.residueField) (a : F.residueField⟦X⟧)
    (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTateBracket F n (PowerSeries.C c * a) x =
      algebraMap F.residueField F.residueField⸨X⸩ c *
        equalCharacteristicLubinTateBracket F n a x

theorem

equalCharacteristicLubinTatePiEnd_bracket

L284 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiEnd_bracket

Documentation

The bracket commutes with the distinguished 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 equalCharacteristicLubinTatePiEnd_bracket
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧)
    (x : F.residueField⸨X⸩) :
    equalCharacteristicLubinTatePiEnd F
        (equalCharacteristicLubinTateBracket F n a x) =
      equalCharacteristicLubinTateBracket F n a
        (equalCharacteristicLubinTatePiEnd F x)

theorem

equalCharacteristicLubinTateBracket_succ_eq_of_torsion

L303 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracket_succ_eq_of_torsion

Documentation

On a point killed by e^n, the (n+1)-term bracket equals the n-term bracket.

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_succ_eq_of_torsion
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧)
    (x : F.residueField⸨X⸩)
    (hx : IsEqualCharacteristicLubinTateTorsion F n x) :
    equalCharacteristicLubinTateBracket F (n + 1) a x =
      equalCharacteristicLubinTateBracket F n a x

theorem

equalCharacteristicLubinTatePiEnd_bracket_succ_of_torsion

L317 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePiEnd_bracket_succ_of_torsion

Documentation

If x is killed by e^(n+1), applying e to an (n+1)-term bracket drops it to the n-term bracket at e(x).

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_bracket_succ_of_torsion
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧)
    (x : F.residueField⸨X⸩)
    (hx : IsEqualCharacteristicLubinTateTorsion F (n + 1) x) :
    equalCharacteristicLubinTatePiEnd F
        (equalCharacteristicLubinTateBracket F (n + 1) a x) =
      equalCharacteristicLubinTateBracket F n a
        (equalCharacteristicLubinTatePiEnd F x)

theorem

equalCharacteristicLubinTateBracket_mul_apply_of_torsion

L334 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracket_mul_apply_of_torsion

Documentation

Multiplicativity of the genuine truncated Lubin--Tate brackets on e^n-division points.

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_mul_apply_of_torsion
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a b : F.residueField⟦X⟧)
    (x : F.residueField⸨X⸩)
    (hx : IsEqualCharacteristicLubinTateTorsion F n x) :
    equalCharacteristicLubinTateBracket F n (a * b) x =
      equalCharacteristicLubinTateBracket F n a
        (equalCharacteristicLubinTateBracket F n b x)

Module documentation

Equal-characteristic Lubin--Tate action

Declarations