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.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.