The p-power roots of unity in a local field

The p-power roots of unity form the p-primary component of the multiplicative group. In a nonarchimedean local field of characteristic different from p, this group is finite: every root has valuation zero, and sufficiently deep principal units have no p-power torsion. The resulting injection into a finite unit-filtration quotient proves finiteness. A finite subgroup of a field's unit group is cyclic. These facts make its order an arithmetic invariant of finite extensions of ℚ_p.

The finiteness argument uses the unit-filtration results in this library. For the standard structure theorem see Serre, Local Fields, Chapter II, §§4–5.

noncomputable def TauCeti.localRootOfUnityOrder (p : ℕ) (K : Type u_1) [CommMonoid K] (_h : Finite ↥(pPowerRootsOfUnity p K)) : ℕ

The order of the p-power roots of unity, with finiteness made explicit. In local-field applications the witness is finite_pPowerRootsOfUnity.

Equations

• TauCeti.localRootOfUnityOrder p K _h = Nat.card ↥(TauCeti.pPowerRootsOfUnity p K)

@[simp]

theorem TauCeti.localRootOfUnityOrder_def (p : ℕ) (K : Type u_1) [CommMonoid K] (h : Finite ↥(pPowerRootsOfUnity p K)) : localRootOfUnityOrder p K h = Nat.card ↥(pPowerRootsOfUnity p K)

The order of the p-power roots of unity is the cardinality of its subgroup.

theorem TauCeti.localRootOfUnityOrder_pos (p : ℕ) (K : Type u_1) [CommMonoid K] (h : Finite ↥(pPowerRootsOfUnity p K)) : 0 < localRootOfUnityOrder p K h

The order of a finite p-power root group is positive.

theorem TauCeti.localRootOfUnityOrder_isPow (p : ℕ) (K : Type u_1) [CommMonoid K] [Fact (Nat.Prime p)] (h : Finite ↥(pPowerRootsOfUnity p K)) : ∃ (n : ℕ), localRootOfUnityOrder p K h = p ^ n

The order of the p-power roots of unity is a power of p.

theorem TauCeti.prime_eq_two_of_localRootOfUnityOrder_eq_two (p : ℕ) (K : Type u_1) [CommMonoid K] [Fact (Nat.Prime p)] (h : Finite ↥(pPowerRootsOfUnity p K)) (horder : localRootOfUnityOrder p K h = 2) : p = 2

If the p-power roots of unity have order two, then p = 2.

theorem TauCeti.pPowerRootsOfUnity_eq_rootsOfUnity_order (p : ℕ) (K : Type u_1) [CommMonoid K] [Fact (Nat.Prime p)] (h : Finite ↥(pPowerRootsOfUnity p K)) : pPowerRootsOfUnity p K = rootsOfUnity (localRootOfUnityOrder p K h) K

Once the p-power roots of unity are finite, a single level of the root tower contains them all: that level is their order.

theorem TauCeti.primitiveRoot_pow_iff_dvd_localRootOfUnityOrder_of_finite (p : ℕ) (K : Type u_1) [CommRing K] [IsDomain K] [NeZero p] (hfinite : Finite ↥(pPowerRootsOfUnity p K)) (n : ℕ) : (∃ (ζ : K), IsPrimitiveRoot ζ (p ^ n)) ↔ p ^ n ∣ localRootOfUnityOrder p K hfinite

A domain with finitely many p-power roots of unity contains a primitive p^n-th root precisely when p^n divides the order of their group.

theorem TauCeti.pPowerRootsOfUnity_le_unitFiltration_zero {p : ℕ} {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hp : p ≠ 0) : pPowerRootsOfUnity p K ≤ unitFiltration K 0

Every p-power root of unity has valuation zero.

theorem TauCeti.disjoint_pPowerRootsOfUnity_unitFiltration {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {i : ℕ} (hpK : ↑p ≠ 0) (hi : natCastValuation K p hpK < (p - 1) * i) : Disjoint (pPowerRootsOfUnity p K) (unitFiltration K i)

A sufficiently deep principal-unit group contains no nontrivial p-power root of unity.

theorem TauCeti.finite_pPowerRootsOfUnity {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hpK : ↑p ≠ 0) : Finite ↥(pPowerRootsOfUnity p K)

The p-power roots of unity in a local field of characteristic different from p form a finite group.

theorem TauCeti.primitiveRoot_pow_iff_dvd_localRootOfUnityOrder {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hpK : ↑p ≠ 0) (n : ℕ) : (∃ (ζ : K), IsPrimitiveRoot ζ (p ^ n)) ↔ p ^ n ∣ localRootOfUnityOrder p K ⋯

A local field contains a primitive p^n-th root of unity precisely when p^n divides the order of its p-power root group.

theorem TauCeti.primitiveRoot_iff_dvd_localRootOfUnityOrder {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hpK : ↑p ≠ 0) : (∃ (ζ : K), IsPrimitiveRoot ζ p) ↔ p ∣ localRootOfUnityOrder p K ⋯

A local field contains a primitive p-th root of unity exactly when p divides the order of its p-power root group.

theorem TauCeti.localRootOfUnityOrder_ne_two_iff {K : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : localRootOfUnityOrder 2 K ⋯ ≠ 2 ↔ ∃ (ζ : K), IsPrimitiveRoot ζ 4

In a dyadic local field, the 2-power root group has order greater than two exactly when there is a primitive fourth root of unity. This distinguishes the two dyadic presentation branches.