ModuleCompletedFrobeniusFixedFieldPowerBasis.lean
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusFixedFieldPowerBasis
3 declarations indexed from sourceView source ↗ Module documentation
The completed theta-intertwining theorem: the fixed primitive completed power basis
The direct theta value supplies the power basis used to descend coefficients of elements fixed by the prescribed completed Frobenius.
Declarations
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldCompletedPowerBasisBaseAlgebra
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.equalCharacteristicDirectThetaCompletedPowerBasis
DocumentationDefines equalCharacteristicDirectThetaCompletedPowerBasis.
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
equalCharacteristicCompletedFrobeniusFixedFieldCompletedPowerBasisBaseAlgebra
(F : LocalField.{u, v} K) :
Algebra F.residueField⸨X⸩
(equalCharacteristicCompletedUnramifiedField F.residueField) :=
laurentSeriesCoefficientAlgebra
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaCompletedPowerBasis_gen
DocumentationStates the theorem equalCharacteristicDirectThetaCompletedPowerBasis_gen.
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
equalCharacteristicCompletedFrobeniusFixedFieldCompletedPowerBasisBaseAlgebra
(F : LocalField.{u, v} K) :
Algebra F.residueField⸨X⸩
(equalCharacteristicCompletedUnramifiedField F.residueField) :=
laurentSeriesCoefficientAlgebra