The image of the cyclotomic character

This file reads two properties of the field K off the image of its p-adic cyclotomic character χ = localCyclotomicCharacter p K.

• Roots of unity of the base field. The values of χ modulo p ^ n record the action of Gal(K^alg/K) on the p ^ n-th roots of unity. So when p is invertible in K, the image of χ lies in the principal unit group U^(n) = 1 + p ^ n ℤ_p exactly when K contains a primitive p ^ n-th root of unity.
• Infinitude over a finite extension of ℚ_p. For K finite over ℚ_p, the image of χ is infinite. If it had m elements, every p-power root of unity would have at most m conjugates over K, hence degree at most [K : ℚ_p] · m over ℚ_p. This contradicts the irreducibility of the cyclotomic polynomials Φ_{p ^ n} over ℚ_p.

In the dyadic case these are the two inputs that, together with the classification of the closed subgroups of ℤ₂ˣ, determine the image of χ in each branch of the marked classification.

Main results

• TauCeti.localCyclotomicCharacter_mem_unitsPrincipal: if μ_{p ^ n} ⊆ K, every value of the cyclotomic character lies in U^(n).
• TauCeti.range_localCyclotomicCharacter_le_unitsPrincipal_iff: if p is invertible in K, the image lies in U^(n) if and only if μ_{p ^ n} ⊆ K.
• TauCeti.isClosed_range_localCyclotomicCharacter: the image is closed, since the absolute Galois group is compact.
• TauCeti.infinite_range_localCyclotomicCharacter: the image is infinite when K is a finite extension of ℚ_p.

References

• J.-P. Serre, Local Fields, Chapter IV, §4.

theorem TauCeti.localCyclotomicCharacter_mem_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] {n : ℕ} (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ (p ^ n)) (σ : Field.absoluteGaloisGroup K) : (localCyclotomicCharacter p K) σ ∈ unitsPrincipal p n

If K contains a primitive p ^ n-th root of unity, every value of the cyclotomic character of K is a principal unit ≡ 1 mod p ^ n.

theorem TauCeti.range_localCyclotomicCharacter_le_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] {n : ℕ} (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ (p ^ n)) : (localCyclotomicCharacter p K).range ≤ unitsPrincipal p n

If K contains a primitive p ^ n-th root of unity, the image of the cyclotomic character of K lies in the principal unit group U^(n) = 1 + p ^ n ℤ_p.

theorem TauCeti.range_localCyclotomicCharacter_le_unitsPrincipal_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [NeZero ↑p] (n : ℕ) : (localCyclotomicCharacter p K).range ≤ unitsPrincipal p n ↔ ∃ (ζ : K), IsPrimitiveRoot ζ (p ^ n)

If p is invertible in K, the image of the cyclotomic character lies in the principal unit group U^(n) = 1 + p ^ n ℤ_p exactly when K contains a primitive p ^ n-th root of unity.

theorem TauCeti.isClosed_range_localCyclotomicCharacter (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] : IsClosed ↑(localCyclotomicCharacter p K).range

The image of the cyclotomic character is closed in ℤ_pˣ.

theorem TauCeti.infinite_range_localCyclotomicCharacter (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [FiniteDimensional ℚ_[p] K] : Infinite ↥(localCyclotomicCharacter p K).range

The image of the cyclotomic character of a finite extension K of ℚ_p is infinite.