ModuleHigherUnitFixedFieldMembership.lean
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.HigherUnitFixedFieldMembership
4 declarations indexed from sourceView source ↗ Module documentation
LubinTate the explicit norm-subgroup computation: the standard level lies in the higher-unit
fixed field
Declarations
LubinTate.EqualCharacteristic.equalCharacteristicHigherUnitMembershipBaseAlgebra
Source context 6 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]
LubinTate.EqualCharacteristic.equalCharacteristicHigherUnitMembershipLevelAlgebra
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]
noncomputable local instance equalCharacteristicHigherUnitMembershipBaseAlgebra
(F : LocalField K) :
Algebra F.residueField⸨X⸩
(equalCharacteristicCompletedUnramifiedField F.residueField) :=
equalCharacteristicCompletedFrobeniusFixedBaseAlgebra F
LubinTate.EqualCharacteristic.equalCharacteristicHigherUnitMembershipScalarTower
Source context 8 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]
noncomputable local instance equalCharacteristicHigherUnitMembershipBaseAlgebra
(F : LocalField K) :
Algebra F.residueField⸨X⸩
(equalCharacteristicCompletedUnramifiedField F.residueField) :=
equalCharacteristicCompletedFrobeniusFixedBaseAlgebra F
noncomputable local instance equalCharacteristicHigherUnitMembershipLevelAlgebra
(F : LocalField K) (n : ℕ) :
Algebra F.residueField⸨X⸩
(equalCharacteristicCompletedLevelField F n) :=
equalCharacteristicCompletedFrobeniusFixedLevelAlgebra F n
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldToCompleted_mem_fixedField_of_mem_higherUnit
DocumentationStates the theorem equalCharacteristicLubinTateLevelFieldToCompleted_mem_fixedField_of_mem_higherUnit.
Source context 9 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]
noncomputable local instance equalCharacteristicHigherUnitMembershipBaseAlgebra
(F : LocalField K) :
Algebra F.residueField⸨X⸩
(equalCharacteristicCompletedUnramifiedField F.residueField) :=
equalCharacteristicCompletedFrobeniusFixedBaseAlgebra F
noncomputable local instance equalCharacteristicHigherUnitMembershipLevelAlgebra
(F : LocalField K) (n : ℕ) :
Algebra F.residueField⸨X⸩
(equalCharacteristicCompletedLevelField F n) :=
equalCharacteristicCompletedFrobeniusFixedLevelAlgebra F n
local instance equalCharacteristicHigherUnitMembershipScalarTower
(F : LocalField K) (n : ℕ) :
IsScalarTower F.residueField⸨X⸩
(equalCharacteristicCompletedUnramifiedField F.residueField)
(equalCharacteristicCompletedLevelField F n) :=
IsScalarTower.of_algebraMap_eq' rfl