Properties of the adjoint action

Theorems about the adjoint action LieAlgebra.ad on associative algebras.

Main results

• LieAlgebra.commute_ad_of_commute: commuting elements have commuting adjoints.
• LieAlgebra.ad_nilpotent_of_nilpotent: the adjoint of a nilpotent element is nilpotent.
• LieAlgebra.ad_isSemisimple_of_isSemisimple: the adjoint of a semisimple element is semisimple.

theorem LieAlgebra.commute_ad_of_commute {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {a b : A} (h : Commute a b) : Commute ((ad R A) a) ((ad R A) b)

Commuting elements have commuting adjoint actions.

theorem LieAlgebra.ad_nilpotent_of_nilpotent {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {a : A} (h : IsNilpotent a) : IsNilpotent ((ad R A) a)

The adjoint of a nilpotent element is nilpotent.

theorem LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad {R : Type u_1} [CommRing R] {L : Type u_3} [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) {x : ↥K} (h : IsNilpotent ((LieAlgebra.ad R L) ↑x)) : IsNilpotent ((LieAlgebra.ad R ↥K) x)

theorem LieAlgebra.isNilpotent_ad_of_isNilpotent {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {L : LieSubalgebra R A} {x : ↥L} (h : IsNilpotent ↑x) : IsNilpotent ((ad R ↥L) x)

theorem LieAlgebra.ad_isSemisimple_of_isSemisimple {K : Type u_1} {V : Type u_2} [Field K] [PerfectField K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {a : Module.End K V} (ha : a.IsSemisimple) : ((ad K (Module.End K V)) a).IsSemisimple

The adjoint of a semisimple element is semisimple.