Module

CompletedFrobeniusBaseEquiv.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusBaseEquiv

6 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: the completed Frobenius lift over the Laurent base

The prescribed completed lift is semilinear over the completed maximal unramified field. Arithmetic Frobenius on that field fixes the embedded Laurent base k((T)); hence the lift is an actual k((T))-automorphism.

Imports1

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusContinuity

Imported by4

instance

equalCharacteristicCompletedFrobeniusBaseAlgebra

L32 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusBaseAlgebra

Source context 7 commands

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

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

Lean source · statement

instance equalCharacteristicCompletedFrobeniusBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)

instance

equalCharacteristicCompletedFrobeniusLevelAlgebra

L38 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLevelAlgebra

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

instance equalCharacteristicCompletedFrobeniusLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicCompletedFrobeniusScalarTower

L48 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusScalarTower

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  RingHom.toAlgebra
    ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)).comp
      (algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)))

Lean source · statement

instance equalCharacteristicCompletedFrobeniusScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)

theorem

equalCharacteristicCompletedFrobeniusLiftEquiv_fixesLaurentBase

L59 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLiftEquiv_fixesLaurentBase

Documentation

The completed theta-intertwining theorem completed lift fixes every element of the embedded Laurent base k((T)).

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  RingHom.toAlgebra
    ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)).comp
      (algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)))
local instance equalCharacteristicCompletedFrobeniusScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

theorem equalCharacteristicCompletedFrobeniusLiftEquiv_fixesLaurentBase
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (b : F.residueField⸨X⸩) :
    equalCharacteristicCompletedFrobeniusLiftEquiv F n u⁻¹
        (algebraMap F.residueField⸨X⸩
          (equalCharacteristicCompletedLevelField F n) b) =
      algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedLevelField F n) b

def

equalCharacteristicCompletedFrobeniusAlgEquiv

L81 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusAlgEquiv

Documentation

The prescribed the completed theta-intertwining theorem lift, regarded as an automorphism over the original Laurent field k((T)).

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  RingHom.toAlgebra
    ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)).comp
      (algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)))
local instance equalCharacteristicCompletedFrobeniusScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

def equalCharacteristicCompletedFrobeniusAlgEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicCompletedLevelField F n ≃ₐ[F.residueField⸨X⸩]
      equalCharacteristicCompletedLevelField F n

theorem

equalCharacteristicCompletedFrobeniusAlgEquiv_apply

L92 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusAlgEquiv_apply

Documentation

States the theorem equalCharacteristicCompletedFrobeniusAlgEquiv_apply.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  RingHom.toAlgebra
    ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)).comp
      (algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)))
local instance equalCharacteristicCompletedFrobeniusScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

theorem equalCharacteristicCompletedFrobeniusAlgEquiv_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (x : equalCharacteristicCompletedLevelField F n) :
    equalCharacteristicCompletedFrobeniusAlgEquiv F u n x =
      equalCharacteristicCompletedFrobeniusLiftEquiv F n u⁻¹ x

Module documentation

The completed theta-intertwining theorem: the completed Frobenius lift over the Laurent base

Declarations

equalCharacteristicCompletedFrobeniusBaseAlgebra

equalCharacteristicCompletedFrobeniusLevelAlgebra

equalCharacteristicCompletedFrobeniusScalarTower

equalCharacteristicCompletedFrobeniusLiftEquiv_fixesLaurentBase

equalCharacteristicCompletedFrobeniusAlgEquiv

equalCharacteristicCompletedFrobeniusAlgEquiv_apply