NYLL
Module

CompletedFrobeniusFixedFieldCoefficientDescent.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusFixedFieldCoefficientDescent
4 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: coefficient descent in the completed fixed field

Expansion in the direct-theta power basis turns Frobenius fixedness into coefficientwise fixedness. The coefficients therefore descend from the completed unramified field to the original Laurent base.

Imports1
Imported by4

Declarations

instance

equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentBaseAlgebra

L33 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentBaseAlgebra
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
    equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
instance

equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentLevelAlgebra

L40 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentLevelAlgebra
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
    equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
instance
    equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n)
instance

equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentScalarTower

L51 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentScalarTower
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
    equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentLevelAlgebra
    (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
    equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
theorem

equalCharacteristicCompletedFrobenius_fixed_mem_adjoin_directTheta

L60 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobenius_fixed_mem_adjoin_directTheta
Documentation

States the theorem equalCharacteristicCompletedFrobenius_fixed_mem_adjoin_directTheta.

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
    equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentLevelAlgebra
    (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
    equalCharacteristicCompletedFrobeniusFixedFieldCoefficientDescentScalarTower
    (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 equalCharacteristicCompletedFrobenius_fixed_mem_adjoin_directTheta
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ)
    (x : equalCharacteristicCompletedLevelField F n)
    (hx : equalCharacteristicCompletedFrobeniusAlgEquiv F a n x = x) :
    x ∈ IntermediateField.adjoin F.residueField⸨X⸩
      ({(equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F a n :
        equalCharacteristicCompletedLevelField F n)} :
        Set (equalCharacteristicCompletedLevelField F n))

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