Unipotent elements and p-power order in characteristic p

In a ring of exponential characteristic p the binomial theorem degenerates to (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n for commuting x and y (sub_pow_expChar_pow_of_commute). Taking y = 1 turns an equation x ^ p ^ n = 1 into (x - 1) ^ p ^ n = 0: an element of p-power order is unipotent. Only exponential characteristic p is needed, so the statement is read equally in characteristic zero, where it says that an element with x ^ 1 = 1 is 1.

The converse — a unipotent element has p-power order — is not proved here. It fails in exponential characteristic 1: in a ℚ-algebra containing a nonzero element ε of square zero, 1 + ε is unipotent while (1 + ε) ^ n = 1 + n • ε is 1 only for n = 0.

Main results

• TauCeti.isNilpotent_sub_one_of_pow_expChar_pow_eq_one: an element of p-power order is unipotent.

References

The implication is the standard characteristic-p dictionary between unipotent and p-unipotent elements; see J. E. Humphreys, Linear Algebraic Groups, §15.3, and T. A. Springer, Linear Algebraic Groups, §2.4.

theorem TauCeti.isNilpotent_sub_one_of_pow_expChar_pow_eq_one {R : Type u_1} [Ring R] {x : R} (p n : ℕ) [ExpChar R p] (h : x ^ p ^ n = 1) : IsNilpotent (x - 1)

An element of p-power order is unipotent in a ring of exponential characteristic p: subtracting 1 and raising to the power p ^ n commutes with the subtraction, so x ^ p ^ n = 1 forces (x - 1) ^ p ^ n = 0.