ModuleCompletedFrobeniusFixedFieldGeneration.lean
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusFixedFieldGeneration
4 declarations indexed from sourceView source ↗ Module documentation
The completed theta-intertwining theorem: generation of the completed Frobenius fixed field
The coefficient-descent inclusion and the already proved fixedness of the direct theta value identify the fixed field with its simple Laurent-base extension.
Declarations
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldGenerationBaseAlgebra
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]
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldGenerationLevelAlgebra
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
equalCharacteristicCompletedFrobeniusFixedFieldGenerationBaseAlgebra
(F : LocalField.{u, v} K) :
Algebra F.residueField⸨X⸩
(equalCharacteristicCompletedUnramifiedField F.residueField) :=
laurentSeriesCoefficientAlgebra
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldGenerationScalarTower
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
equalCharacteristicCompletedFrobeniusFixedFieldGenerationBaseAlgebra
(F : LocalField.{u, v} K) :
Algebra F.residueField⸨X⸩
(equalCharacteristicCompletedUnramifiedField F.residueField) :=
laurentSeriesCoefficientAlgebra
noncomputable local instance
equalCharacteristicCompletedFrobeniusFixedFieldGenerationLevelAlgebra
(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)))
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedField_eq_adjoin_directTheta
DocumentationThe Frobenius fixed field is exactly the finite target Lubin--Tate level generated by theta(lambda) inside the completed field.
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
equalCharacteristicCompletedFrobeniusFixedFieldGenerationBaseAlgebra
(F : LocalField.{u, v} K) :
Algebra F.residueField⸨X⸩
(equalCharacteristicCompletedUnramifiedField F.residueField) :=
laurentSeriesCoefficientAlgebra
noncomputable local instance
equalCharacteristicCompletedFrobeniusFixedFieldGenerationLevelAlgebra
(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
equalCharacteristicCompletedFrobeniusFixedFieldGenerationScalarTower
(F : LocalField.{u, v} K) (n : ℕ) :
IsScalarTower F.residueField⸨X⸩
(equalCharacteristicCompletedUnramifiedField F.residueField)
(equalCharacteristicCompletedLevelField F n) :=
IsScalarTower.of_algebraMap_eq' rfl