LubinTate.equalCharacteristicLubinTate_galoisAction_eq_bracket_unique
Equal-characteristic Lubin--Tate action frontier: every automorphism of the explicit level-n+1 field acts on the primitive generator through a unique visible unit-parameter bracket.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped LaurentSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
universe u v
variable {K : Type u} [Field K]Lean source · statement
theorem equalCharacteristicLubinTate_galoisAction_eq_bracket_unique
(F : LocalField.{u, v} K)
[CharP K F.residueCharacteristic]
(n : ℕ)
(σ : Gal((equalCharacteristicLubinTateLevelField F n)/F.residueField⸨X⸩)) :
∃! a : equalCharacteristicLubinTateUnitParameter F n,
σ (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
equalCharacteristicLubinTateLevelBracket F n (n + 1)
(equalCharacteristicLubinTateUnitParameterSeries F n a)
(equalCharacteristicLubinTateLevelPowerBasis F n).gen