Module

AmbientDivisionTorsion.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.AmbientDivisionTorsion

10 declarations indexed from sourceView source ↗

Module documentation

Ambient Lubin--Tate division groups

The kernel of the n-fold distinguished endomorphism in any ambient field is stable under all truncated brackets. Units of κ⟦T⟧ therefore act on it by actual additive automorphisms. This is the version needed in the separable closure, where the nonzero division points live.

Imports1

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FormalModule.AmbientBracketAction

Imported by5

def

equalCharacteristicLubinTateAmbientTorsionAddSubgroup

L34 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientTorsionAddSubgroup

Documentation

The level-n division group inside an ambient field.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

def equalCharacteristicLubinTateAmbientTorsionAddSubgroup
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t : A) (n : ℕ) : AddSubgroup A

theorem

mem_equalCharacteristicLubinTateAmbientTorsionAddSubgroup

L42 ↗

LubinTate.EqualCharacteristic.mem_equalCharacteristicLubinTateAmbientTorsionAddSubgroup

Documentation

States the theorem mem_equalCharacteristicLubinTateAmbientTorsionAddSubgroup.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem mem_equalCharacteristicLubinTateAmbientTorsionAddSubgroup
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (t : A) (n : ℕ) (x : A) :
    x ∈ equalCharacteristicLubinTateAmbientTorsionAddSubgroup F t n ↔
      IsEqualCharacteristicLubinTateAmbientTorsion F t n x

theorem

equalCharacteristicLubinTateAmbientPiIterate_bracket

L51 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientPiIterate_bracket

Documentation

Every iterate of e commutes with every ambient bracket.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateAmbientPiIterate_bracket
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (i n : ℕ) (a : F.residueField⟦X⟧) (x : A) :
    equalCharacteristicLubinTateAmbientPiIterate F t i
        (equalCharacteristicLubinTateAmbientBracket F ι t n a x) =
      equalCharacteristicLubinTateAmbientBracket F ι t n a
        (equalCharacteristicLubinTateAmbientPiIterate F t i x)

theorem

equalCharacteristicLubinTateAmbientBracket_torsion

L69 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientBracket_torsion

Documentation

Every bracket preserves the ambient division group.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateAmbientBracket_torsion
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧) (x : A)
    (hx : IsEqualCharacteristicLubinTateAmbientTorsion F t n x) :
    IsEqualCharacteristicLubinTateAmbientTorsion F t n
      (equalCharacteristicLubinTateAmbientBracket F ι t n a x)

def

equalCharacteristicLubinTateAmbientTorsionEnd

L83 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientTorsionEnd

Documentation

The endomorphism of the ambient level-n division group induced by a bracket.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · full declaration

def equalCharacteristicLubinTateAmbientTorsionEnd
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧) :
    AddMonoid.End
      (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F t n) where
  toFun x :=
    ⟨equalCharacteristicLubinTateAmbientBracket F ι t n a x.1,
      equalCharacteristicLubinTateAmbientBracket_torsion
        F ι t n a x.1 x.2⟩
  map_zero' := by
    apply Subtype.ext
    exact (equalCharacteristicLubinTateAmbientBracket F ι t n a).map_zero
  map_add' x y := by
    apply Subtype.ext
    exact (equalCharacteristicLubinTateAmbientBracket F ι t n a).map_add
      x.1 y.1

theorem

equalCharacteristicLubinTateAmbientTorsionEnd_apply

L104 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientTorsionEnd_apply

Documentation

States the theorem equalCharacteristicLubinTateAmbientTorsionEnd_apply.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateAmbientTorsionEnd_apply
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧)
    (x : equalCharacteristicLubinTateAmbientTorsionAddSubgroup F t n) :
    (equalCharacteristicLubinTateAmbientTorsionEnd F ι t n a x).1 =
      equalCharacteristicLubinTateAmbientBracket F ι t n a x.1

theorem

equalCharacteristicLubinTateAmbientBracket_one_apply_of_torsion

L116 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientBracket_one_apply_of_torsion

Documentation

The bracket of 1 fixes all ambient division points, also at level zero.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateAmbientBracket_one_apply_of_torsion
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (x : A)
    (hx : IsEqualCharacteristicLubinTateAmbientTorsion F t n x) :
    equalCharacteristicLubinTateAmbientBracket F ι t n 1 x = x

def

equalCharacteristicLubinTateAmbientTorsionUnitAut

L137 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientTorsionUnitAut

Documentation

A unit power series acts by an automorphism of every ambient division group.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · full declaration

def equalCharacteristicLubinTateAmbientTorsionUnitAut
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    AddEquiv
      (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F t n)
      (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F t n) where
  toFun := equalCharacteristicLubinTateAmbientTorsionEnd F ι t n
    (a : F.residueField⟦X⟧)
  invFun := equalCharacteristicLubinTateAmbientTorsionEnd F ι t n
    (↑(a⁻¹) : F.residueField⟦X⟧)
  left_inv x := by
    apply Subtype.ext
    change equalCharacteristicLubinTateAmbientBracket F ι t n
      (↑(a⁻¹) : F.residueField⟦X⟧)
        (equalCharacteristicLubinTateAmbientBracket F ι t n
          (a : F.residueField⟦X⟧) x.1) = x.1
    rw [← equalCharacteristicLubinTateAmbientBracket_mul_apply_of_torsion
      F ι t n (↑(a⁻¹) : F.residueField⟦X⟧)
        (a : F.residueField⟦X⟧) x.1 x.2]
    simpa using
      equalCharacteristicLubinTateAmbientBracket_one_apply_of_torsion
        F ι t n x.1 x.2
  right_inv x := by
    apply Subtype.ext
    change equalCharacteristicLubinTateAmbientBracket F ι t n
      (a : F.residueField⟦X⟧)
        (equalCharacteristicLubinTateAmbientBracket F ι t n
          (↑(a⁻¹) : F.residueField⟦X⟧) x.1) = x.1
    rw [← equalCharacteristicLubinTateAmbientBracket_mul_apply_of_torsion
      F ι t n (a : F.residueField⟦X⟧)
        (↑(a⁻¹) : F.residueField⟦X⟧) x.1 x.2]
    simpa using
      equalCharacteristicLubinTateAmbientBracket_one_apply_of_torsion
        F ι t n x.1 x.2
  map_add' x y :=
    (equalCharacteristicLubinTateAmbientTorsionEnd F ι t n
      (a : F.residueField⟦X⟧)).map_add x y

theorem

equalCharacteristicLubinTateAmbientTorsionUnitAut_apply

L179 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientTorsionUnitAut_apply

Documentation

States the theorem equalCharacteristicLubinTateAmbientTorsionUnitAut_apply.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateAmbientTorsionUnitAut_apply
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧ˣ)
    (x : equalCharacteristicLubinTateAmbientTorsionAddSubgroup F t n) :
    (equalCharacteristicLubinTateAmbientTorsionUnitAut F ι t n a x).1 =
      equalCharacteristicLubinTateAmbientBracket F ι t n
        (a : F.residueField⟦X⟧) x.1

theorem

equalCharacteristicLubinTateAmbientBracket_eq_of_coeff_eq

L192 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientBracket_eq_of_coeff_eq

Documentation

Equality of the first n coefficients makes two ambient brackets equal.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateAmbientBracket_eq_of_coeff_eq
    (F : LocalField.{u, v} K)
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a b : F.residueField⟦X⟧)
    (hab : ∀ i < n, PowerSeries.coeff i a = PowerSeries.coeff i b) :
    equalCharacteristicLubinTateAmbientBracket F ι t n a =
      equalCharacteristicLubinTateAmbientBracket F ι t n b

Module documentation

Ambient Lubin--Tate division groups

Declarations