Roots of unity of p-power order

For a commutative monoid, the p-power roots of unity form the primary component of its unit group. In a reduced ring of exponential characteristic p this subgroup is trivial, and in a domain it is cyclic when finite.

@[reducible, inline]

abbrev TauCeti.pPowerRootsOfUnity (p : ℕ) (K : Type u_1) [CommMonoid K] : Subgroup Kˣ

The subgroup of Kˣ consisting of roots of unity of p-power order.

Equations

• TauCeti.pPowerRootsOfUnity p K = CommGroup.primaryComponent Kˣ p

theorem TauCeti.mem_pPowerRootsOfUnity_iff (p : ℕ) (K : Type u_1) [CommMonoid K] (x : Kˣ) : x ∈ pPowerRootsOfUnity p K ↔ ∃ (n : ℕ), x ^ p ^ n = 1

A unit is a p-power root of unity exactly when some power of p kills it.

theorem TauCeti.pPowerRootsOfUnity_eq_iSup_rootsOfUnity (p : ℕ) (K : Type u_1) [CommMonoid K] : pPowerRootsOfUnity p K = ⨆ (n : ℕ), rootsOfUnity (p ^ n) K

The p-power roots of unity are the union of the finite-level root groups.

@[simp]

theorem TauCeti.pPowerRootsOfUnity_eq_bot (p : ℕ) (R : Type u_2) [CommRing R] [IsReduced R] [ExpChar R p] : pPowerRootsOfUnity p R = ⊥

In a reduced ring of exponential characteristic p, the only root of unity of p-power order is 1, since the Frobenius is injective.

theorem TauCeti.isCyclic_pPowerRootsOfUnity (p : ℕ) (K : Type u_1) [CommRing K] [IsDomain K] (h : Finite ↥(pPowerRootsOfUnity p K)) : IsCyclic ↥(pPowerRootsOfUnity p K)

A finite group of p-power roots of unity in a domain is cyclic.