Unipotent endomorphisms and p-power order in characteristic p

The endomorphism algebra of a nonzero vector space over a field k of exponential characteristic p has the same exponential characteristic, because k acts faithfully on it, so an operator of p-power order is unipotent: this is the ring-level TauCeti.isNilpotent_sub_one_of_pow_expChar_pow_eq_one read in Module.End k V. Over a zero vector space the conclusion is vacuous, every endomorphism being 0, so no nontriviality hypothesis is needed.

Mathlib records the characteristic of an endomorphism algebra in Mathlib/Algebra/CharP/LinearMaps.lean, whose Module.charP_end transfers a prime characteristic along a non-torsion element; the exponential characteristic of a vector space needs no such element.

Main results

• Module.End.isNilpotent_sub_one_of_pow_expChar_pow_eq_one: an endomorphism of p-power order of a vector space over a field of exponential characteristic p is unipotent.

theorem Module.End.isNilpotent_sub_one_of_pow_expChar_pow_eq_one {k : Type u_1} {V : Type u_2} [Field k] [AddCommGroup V] [Module k V] (p n : ℕ) [ExpChar k p] {f : End k V} (h : f ^ p ^ n = 1) : IsNilpotent (f - 1)

In exponential characteristic p, an endomorphism of p-power order is unipotent. Over a nonzero vector space this is the ring-level TauCeti.isNilpotent_sub_one_of_pow_expChar_pow_eq_one read in the endomorphism algebra, whose exponential characteristic is that of k because k acts faithfully on it; over a zero vector space every endomorphism is 0.