Adjoint nilpotence in a split ideal extension

The projection from a semidirect sum I ⋊⁅ψ⁆ H onto H is a surjective Lie homomorphism. Consequently, if an element of the semidirect sum has nilpotent adjoint action, its right component has nilpotent adjoint action on H.

The internal form says that, for a Lie ideal I and a complementary Lie subalgebra H of L, nilpotence of ad (i + h) on L implies nilpotence of ad h on H. In a Levi decomposition, this extracts the adjoint-nilpotent semisimple component of an adjoint-nilpotent element. The argument only uses the split ideal extension; neither semisimplicity nor solvability, finite dimension, or characteristic zero is required.

Main results

• LieAlgebra.SemiDirectSum.isNilpotent_ad_right: adjoint nilpotence passes to the right component of a semidirect sum.
• LieAlgebra.SemiDirectSum.isNilpotent_derivation_of_isNilpotent_ad_inr: adjoint nilpotence of a complementary element implies nilpotence of its derivation on the ideal.
• LieIdeal.isNilpotent_ad_right_of_isCompl: the corresponding result for an internal split ideal extension, stated on a sum of elements in the two complementary factors.

References

• G. Hochschild, An Addition to Ado's Theorem, Proc. Amer. Math. Soc. 17 (1966), 531–533, for the use of this implication on the semisimple component.

theorem LieAlgebra.SemiDirectSum.isNilpotent_ad_right {R : Type u_1} {I : Type u_2} {H : Type u_3} [CommRing R] [LieRing I] [LieAlgebra R I] [LieRing H] [LieAlgebra R H] {ψ : H →ₗ⁅R⁆ LieDerivation R I I} (x : I ⋊⁅ψ⁆ H) (hx : IsNilpotent ((ad R (I ⋊⁅ψ⁆ H)) x)) : IsNilpotent ((ad R H) x.right)

The right component of an adjoint-nilpotent element of a semidirect sum is adjoint-nilpotent in the right factor.

theorem LieAlgebra.SemiDirectSum.isNilpotent_derivation_of_isNilpotent_ad_inr {R : Type u_1} {I : Type u_2} {H : Type u_3} [CommRing R] [LieRing I] [LieAlgebra R I] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R I I) (h : H) (hh : IsNilpotent ((ad R (I ⋊⁅ψ⁆ H)) ((inr ψ) h))) : IsNilpotent ↑(ψ h)

If a complementary element has nilpotent adjoint action on a semidirect sum, its defining derivation on the ideal is nilpotent. No finiteness assumption is required.

theorem LieIdeal.isNilpotent_ad_right_of_isCompl {R : Type u_1} [CommRing R] {L : Type u_4} [LieRing L] [LieAlgebra R L] (J : LieIdeal R L) (S : LieSubalgebra R L) (h : IsCompl (↑J) S.toSubmodule) (i : ↥J) (s : ↥S) (hx : IsNilpotent ((LieAlgebra.ad R L) (↑i + ↑s))) : IsNilpotent ((LieAlgebra.ad R ↥S) s)

For an ideal and a complementary Lie subalgebra, adjoint nilpotence of the sum of two components implies adjoint nilpotence of the subalgebra component on that subalgebra.

Taking the ideal to be the solvable radical and the subalgebra to be a Levi complement gives the projection step in the nilpotence argument for the semisimple component.