Roots of unity in local cyclotomic extensions

The extension ℚ_p(μ_{p^(n+1)}) has degree p^n (p - 1) and its p-power roots of unity are exactly μ_{p^(n+1)}. In particular q(ℚ_p(μ_p)) = p, including at p = 2. These arithmetic invariants determine the rank and torsion parameter of its maximal pro-p Galois group.

The statements use IsCyclotomicExtension, so they apply to any field model of the extension. They need no choice of valuation or topology. The positive exponent is essential: ℚ₂ itself already contains μ₂, although it is the cyclotomic extension generated by μ₁.

References

• J.-P. Serre, Local Fields, Chapter IV, §4.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (7.5.12).

theorem TauCeti.finrank_cyclotomic_prime_pow_ratPadic (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] (n : ℕ) [IsCyclotomicExtension {p ^ (n + 1)} ℚ_[p] K] : Module.finrank ℚ_[p] K = p ^ n * (p - 1)

The degree of ℚ_p(μ_{p^(n+1)}) is p^n (p - 1).

theorem TauCeti.pPowerRootsOfUnity_eq_rootsOfUnity_cyclotomic_prime_pow_ratPadic (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] (n : ℕ) [IsCyclotomicExtension {p ^ (n + 1)} ℚ_[p] K] : pPowerRootsOfUnity p K = rootsOfUnity (p ^ (n + 1)) K

There are no additional p-power roots of unity in ℚ_p(μ_{p^(n+1)}).

theorem TauCeti.finite_pPowerRootsOfUnity_cyclotomic_prime_pow_ratPadic (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] (n : ℕ) [IsCyclotomicExtension {p ^ (n + 1)} ℚ_[p] K] : Finite ↥(pPowerRootsOfUnity p K)

The p-power roots of unity in a positive level of the local cyclotomic tower are finite.

theorem TauCeti.localRootOfUnityOrder_cyclotomic_prime_pow_ratPadic (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] (n : ℕ) [IsCyclotomicExtension {p ^ (n + 1)} ℚ_[p] K] (h : Finite ↥(pPowerRootsOfUnity p K)) : localRootOfUnityOrder p K h = p ^ (n + 1)

The root-of-unity invariant of ℚ_p(μ_{p^(n+1)}) is p^(n+1). The formula holds for any finiteness witness, in particular the finiteness theorem for this cyclotomic tower.