Algebraic eigenvectors of associative derivations

Over a characteristic-zero domain, an algebraic element of a torsion-free associative algebra that is an eigenvector of a derivation with nonzero eigenvalue is nilpotent. Commutativity of the algebra is not required. Indeed, its powers have eigenvalues n * c; if none vanishes, their distinct eigenvalues make them linearly independent, contradicting a polynomial relation.

Applied to inner derivations of endomorphism algebras, this gives the nilpotence of the operator representing x whenever ⁅y, x⁆ = c • x with c ≠ 0. In particular it converts a bracket relation into nilpotence without extending the coefficient field.

Main results

• TauCeti.derivationLieAlgebra.apply_pow_of_apply_eq_smul: powers of an eigenvector of a derivation have eigenvalues multiplied by their exponents.
• TauCeti.derivationLieAlgebra.isNilpotent_of_isAlgebraic_of_apply_eq_smul: an algebraic eigenvector with nonzero eigenvalue is nilpotent in characteristic zero.

References

• G. Hochschild, An Addition to Ado's Theorem, Proc. Amer. Math. Soc. 17 (1966), 531–533, for the use of bracket relations to prove nilpotence in finite-dimensional representations.

theorem TauCeti.derivationLieAlgebra.apply_pow_of_apply_eq_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (D : ↥(derivationLieAlgebra R A)) {x : A} {c : R} (hx : ↑D x = c • x) (n : ℕ) : ↑D (x ^ n) = (↑n * c) • x ^ n

If a derivation acts on x by the scalar c, it acts on xⁿ by n * c.

theorem TauCeti.derivationLieAlgebra.isNilpotent_of_isAlgebraic_of_apply_eq_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [IsDomain R] [CharZero R] [Module.IsTorsionFree R A] (D : ↥(derivationLieAlgebra R A)) {x : A} {c : R} (hx : IsAlgebraic R x) (hc : c ≠ 0) (hDx : ↑D x = c • x) : IsNilpotent x

Over a characteristic-zero domain, an algebraic eigenvector of a derivation with nonzero eigenvalue in a torsion-free algebra is nilpotent. Only the element needs to be algebraic; the ambient algebra may be infinite dimensional.