LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldEquivFixedFieldOfHigherUnit
Defines equalCharacteristicLubinTateLevelFieldEquivFixedFieldOfHigherUnit.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped LaurentSeries PowerSeries
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
attribute [local instance]
equalCharacteristicCompletedFrobeniusFixedBaseAlgebra
equalCharacteristicLubinTateLevelFieldAlgebra
equalCharacteristicLubinTateLevelFieldSMul
equalCharacteristicLubinTateLevelFieldModule
equalCharacteristicCompletedFrobeniusFixedFieldAlgebra
equalCharacteristicCompletedFrobeniusFixedFieldSMul
equalCharacteristicCompletedFrobeniusFixedFieldModuleLean source · statement
def
equalCharacteristicLubinTateLevelFieldEquivFixedFieldOfHigherUnit
(F : LocalField K)
[CharP K F.residueCharacteristic]
(a : F.residueField⟦X⟧ˣ) (n : ℕ)
(ha : a ∈ equalCharacteristicLubinTateHigherUnitSubgroup F n) :
@AlgEquiv
F.residueField⸨X⸩
↥(equalCharacteristicLubinTateLevelField F n)
↥(equalCharacteristicCompletedFrobeniusFixedField F a n)
inferInstance
inferInstance
inferInstance
(equalCharacteristicLubinTateLevelFieldAlgebra F n)
(equalCharacteristicCompletedFrobeniusFixedFieldAlgebra F a n)