LocalClassFieldTheory.normSubgroup_eq_unramifiedNormSubgroup_padic_prime_pow_sub_one
Let L/ℚ_p be generated by a primitive root of order p ^ f - 1. The unramified cyclotomic theorem identifies L with the unramified extension of degree f; consequently its norm subgroup is ⟨p ^ f⟩ × U¹.
The proof compares the complete-DVF valuation with the spectral valuation used by the unramified norm theorem. Uniqueness of the extended valuation on the finite separable extension transports ramification index one between the two presentations.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory.Padic
open ValuationTheory
open scoped NNReal ValuativeRelLean source · statement
theorem normSubgroup_eq_unramifiedNormSubgroup_padic_prime_pow_sub_one
(p f : ℕ) [Fact p.Prime] (hf : 0 < f)
(L : Type) [Field L] [Algebra ℚ_[p] L]
[FiniteDimensional ℚ_[p] L] [IsGalois ℚ_[p] L]
[IsNonarchimedeanLocalField ℚ_[p]]
{ζ : L} (hζ : IsPrimitiveRoot ζ (p ^ f - 1))
(hζgen : Algebra.adjoin ℚ_[p] ({ζ} : Set L) = ⊤) :
LocalFieldTheory.localNormSubgroup ℚ_[p] L = unramifiedNormSubgroup ℚ_[p] f