Jordan–Chevalley decomposition and the adjoint action

This file contains results about the interaction between the adjoint action LieAlgebra.ad and the Jordan–Chevalley decomposition.

Main results

• LieAlgebra.ad_mem_adjoin_of_isSemisimple: for a JC decomposition, ad(s) ∈ K[ad(n + s)].
• LieAlgebra.ad_mem_adjoin_of_isNilpotent: for a JC decomposition, ad(n) ∈ K[ad(n + s)].

theorem LieAlgebra.ad_mem_adjoin_of_isSemisimple {K : Type u_1} {V : Type u_2} [Field K] [PerfectField K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {n s : Module.End K V} (hc : Commute n s) (hn : IsNilpotent n) (hs : s.IsSemisimple) : (ad K (Module.End K V)) s ∈ K[(ad K (Module.End K V)) (n + s)]

The adjoint of the semisimple part of a JC decomposition lies in the subalgebra generated by the adjoint of the sum.

theorem LieAlgebra.ad_mem_adjoin_of_isNilpotent {K : Type u_1} {V : Type u_2} [Field K] [PerfectField K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {n s : Module.End K V} (hc : Commute n s) (hn : IsNilpotent n) (hs : s.IsSemisimple) : (ad K (Module.End K V)) n ∈ K[(ad K (Module.End K V)) (n + s)]

The adjoint of the nilpotent part of a JC decomposition lies in the subalgebra generated by the adjoint of the sum.