LubinTate.EqualCharacteristic.equalCharacteristicTransportedLubinTateNormSubgroup_eq_uniformizerPrincipalSubgroup
The transported level-m+1 Lubin--Tate norm subgroup is exactly ⟨ϖ⟩ · U^(m+1) in the target local field.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped LaurentSeries ValuativeRel
namespace LubinTate
namespace EqualCharacteristic
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]Lean source · statement
theorem
equalCharacteristicTransportedLubinTateNormSubgroup_eq_uniformizerPrincipalSubgroup
(p : ℕ) [Fact p.Prime] [hKp : CharP K p]
(ϖ : Kˣ)
(hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
(m : ℕ) :
equalCharacteristicTransportedLubinTateNormSubgroup
K p ϖ hϖ m =
LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ 1 (m + 1)