NYLL
Module

CompletedFrobeniusFixedNorm.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusFixedNorm
13 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: the fixed-field prime element and its norm

The fixed field of the prescribed completed Frobenius lift is the finite Lubin--Tate level for the changed uniformizer aT. Under this identification its generator is the distinguished element pi_delta = theta(lambda). Its minimal polynomial is the genuine changed primitive Eisenstein polynomial, and the chosen sign convention gives N(-pi_delta) = aT.

Imports1
Imported by4

Declarations

instance

equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra

L35 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
Source context 7 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField)
instance

equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra

L41 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n)
instance

equalCharacteristicCompletedFrobeniusFixedNormScalarTower

L51 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedNormScalarTower
Source context 9 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (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 equalCharacteristicCompletedFrobeniusFixedNormScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
instance

equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra

L58 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (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 equalCharacteristicCompletedFrobeniusFixedNormScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n)
instance

equalCharacteristicCompletedFrobeniusFixedNormChangedLevelSMul

L72 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedNormChangedLevelSMul
Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (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 equalCharacteristicCompletedFrobeniusFixedNormScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  letI : Algebra (LaurentSeries F.residueField)
      (SeparableClosure (LaurentSeries F.residueField)) :=
    (separableClosure (LaurentSeries F.residueField)
      (AlgebraicClosure (LaurentSeries F.residueField))).algebra'
  Subalgebra.algebra
    (equalCharacteristicChangedLevelField F a n).toSubalgebra
Lean source · statement
instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n)
instance

equalCharacteristicCompletedFrobeniusFixedNormChangedLevelModule

L83 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedNormChangedLevelModule
Source context 12 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (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 equalCharacteristicCompletedFrobeniusFixedNormScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  letI : Algebra (LaurentSeries F.residueField)
      (SeparableClosure (LaurentSeries F.residueField)) :=
    (separableClosure (LaurentSeries F.residueField)
      (AlgebraicClosure (LaurentSeries F.residueField))).algebra'
  Subalgebra.algebra
    (equalCharacteristicChangedLevelField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
Lean source · statement
instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n)
def

equalCharacteristicCompletedFrobeniusTargetLevelEquiv

L96 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusTargetLevelEquiv
Documentation

The target aT Lubin--Tate level is the fixed field of the prescribed completed Frobenius lift.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (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 equalCharacteristicCompletedFrobeniusFixedNormScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  letI : Algebra (LaurentSeries F.residueField)
      (SeparableClosure (LaurentSeries F.residueField)) :=
    (separableClosure (LaurentSeries F.residueField)
      (AlgebraicClosure (LaurentSeries F.residueField))).algebra'
  Subalgebra.algebra
    (equalCharacteristicChangedLevelField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toModule _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
Lean source · statement
def equalCharacteristicCompletedFrobeniusTargetLevelEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedLevelField F a n
      ≃ₐ[LaurentSeries F.residueField]
        equalCharacteristicCompletedFrobeniusFixedField F a n
theorem

equalCharacteristicCompletedFrobeniusTargetLevelEquiv_generator

L130 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusTargetLevelEquiv_generator
Documentation

States the theorem equalCharacteristicCompletedFrobeniusTargetLevelEquiv_generator.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (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 equalCharacteristicCompletedFrobeniusFixedNormScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  letI : Algebra (LaurentSeries F.residueField)
      (SeparableClosure (LaurentSeries F.residueField)) :=
    (separableClosure (LaurentSeries F.residueField)
      (AlgebraicClosure (LaurentSeries F.residueField))).algebra'
  Subalgebra.algebra
    (equalCharacteristicChangedLevelField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toModule _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusTargetLevelEquiv_generator
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicCompletedFrobeniusTargetLevelEquiv F a n
        (equalCharacteristicChangedLevelGenerator F a n) =
      ⟨(equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F a n :
          equalCharacteristicCompletedLevelField F n),
        equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_mem_fixedField
          F a n⟩
def

equalCharacteristicCompletedFrobeniusPrimeElement

L145 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusPrimeElement
Documentation

The distinguished element pi_delta = theta(lambda), regarded as an element of the fixed field.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (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 equalCharacteristicCompletedFrobeniusFixedNormScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  letI : Algebra (LaurentSeries F.residueField)
      (SeparableClosure (LaurentSeries F.residueField)) :=
    (separableClosure (LaurentSeries F.residueField)
      (AlgebraicClosure (LaurentSeries F.residueField))).algebra'
  Subalgebra.algebra
    (equalCharacteristicChangedLevelField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toModule _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
Lean source · statement
def equalCharacteristicCompletedFrobeniusPrimeElement
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicCompletedFrobeniusFixedField F a n
theorem

equalCharacteristicCompletedFrobeniusPrimeElement_eq_equiv_generator

L156 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusPrimeElement_eq_equiv_generator
Documentation

States the theorem equalCharacteristicCompletedFrobeniusPrimeElement_eq_equiv_generator.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (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 equalCharacteristicCompletedFrobeniusFixedNormScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  letI : Algebra (LaurentSeries F.residueField)
      (SeparableClosure (LaurentSeries F.residueField)) :=
    (separableClosure (LaurentSeries F.residueField)
      (AlgebraicClosure (LaurentSeries F.residueField))).algebra'
  Subalgebra.algebra
    (equalCharacteristicChangedLevelField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toModule _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusPrimeElement_eq_equiv_generator
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicCompletedFrobeniusPrimeElement F a n =
      equalCharacteristicCompletedFrobeniusTargetLevelEquiv F a n
        (equalCharacteristicChangedLevelGenerator F a n)
theorem

equalCharacteristicCompletedFrobeniusPrimeElement_minpoly

L168 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusPrimeElement_minpoly
Documentation

The minimal polynomial of the fixed-field generator is precisely the target primitive polynomial for aT.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (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 equalCharacteristicCompletedFrobeniusFixedNormScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  letI : Algebra (LaurentSeries F.residueField)
      (SeparableClosure (LaurentSeries F.residueField)) :=
    (separableClosure (LaurentSeries F.residueField)
      (AlgebraicClosure (LaurentSeries F.residueField))).algebra'
  Subalgebra.algebra
    (equalCharacteristicChangedLevelField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toModule _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusPrimeElement_minpoly
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    minpoly (LaurentSeries F.residueField)
        (equalCharacteristicCompletedFrobeniusPrimeElement F a n) =
      equalCharacteristicChangedPrimitivePolynomial F a n
theorem

equalCharacteristicCompletedFrobeniusPrimeElement_eisenstein

L185 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusPrimeElement_eisenstein
Documentation

The genuine integral minimal polynomial is Eisenstein at (T). This is the prime-element (uniformizer) certificate used in the proof of the completed theta-intertwining theorem.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (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 equalCharacteristicCompletedFrobeniusFixedNormScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  letI : Algebra (LaurentSeries F.residueField)
      (SeparableClosure (LaurentSeries F.residueField)) :=
    (separableClosure (LaurentSeries F.residueField)
      (AlgebraicClosure (LaurentSeries F.residueField))).algebra'
  Subalgebra.algebra
    (equalCharacteristicChangedLevelField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toModule _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusPrimeElement_eisenstein
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedIntegralPrimitivePolynomial F a n).IsEisensteinAt
        (Ideal.span ({PowerSeries.X} : Set F.residueField⟦X⟧)) ∧
      (equalCharacteristicChangedIntegralPrimitivePolynomial F a n).map
          (algebraMap F.residueField⟦X⟧
            (LaurentSeries F.residueField)) =
        minpoly (LaurentSeries F.residueField)
          (equalCharacteristicCompletedFrobeniusPrimeElement F a n)
theorem

equalCharacteristicCompletedFrobenius_norm_neg_primeElement

L207 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobenius_norm_neg_primeElement
Documentation

The completed theta-intertwining theorem, with the canonical sign: N_{Sigma/k((T))}(-pi_delta) = aT.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedFrobeniusFixedNormLevelAlgebra
    (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 equalCharacteristicCompletedFrobeniusFixedNormScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  letI : Algebra (LaurentSeries F.residueField)
      (SeparableClosure (LaurentSeries F.residueField)) :=
    (separableClosure (LaurentSeries F.residueField)
      (AlgebraicClosure (LaurentSeries F.residueField))).algebra'
  Subalgebra.algebra
    (equalCharacteristicChangedLevelField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedNormChangedLevelModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module (LaurentSeries F.residueField)
      (equalCharacteristicChangedLevelField F a n) :=
  @Algebra.toModule _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedNormChangedLevelAlgebra
      F a n)
Lean source · statement
theorem equalCharacteristicCompletedFrobenius_norm_neg_primeElement
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.norm (LaurentSeries F.residueField)
        (-equalCharacteristicCompletedFrobeniusPrimeElement F a n) =
      equalCharacteristicChangedLaurentUniformizer F a

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