Derivations carry the solvable radical into the nilradical

Over a field of characteristic zero, every derivation of a finite-dimensional Lie algebra L maps the solvable radical radical K L into the nilradical nilradical K L. In particular every derivation of a solvable Lie algebra has image in the nilradical, the nilradical is stable under all derivations, and ⁅L, radical K L⁆ ≤ nilradical K L. The last inclusion gives the radical criterion: an element of the radical with nilpotent adjoint action lies in the nilradical. Stability under derivations gives the nilradical of an ideal: for every ideal I of L, the nilradical of I consists of the elements of I lying in the nilradical of L.

These are the facts on derivation values used to refine a cofinite enveloping ideal into one stable under all lifted derivations, without assuming that the original ideal is stable, and to compare nilradicals along a flag of ideals between the nilradical and the radical. The radical criterion places the radical component of an ad-nilpotent element in the nilradical, which is how Hochschild shows that ad-nilpotent elements act nilpotently on modules where the nilradical does.

Main results

• LieIdeal.nilradical_le_restrict_nilradical_of_forall: if the nilradical of an ideal I of a Noetherian Lie algebra is stable under every derivation of I, it lies in the nilradical of the ambient Lie algebra.
• LieDerivation.apply_mem_nilradical_of_isSolvable: every derivation of a finite-dimensional solvable Lie algebra in characteristic zero takes values in its nilradical.
• Ado.LieAlgebra.lie_radical_le_nilradical: ⁅L, radical K L⁆ ≤ nilradical K L.
• Ado.LieAlgebra.mem_nilradical_of_mem_radical_of_isNilpotent_ad: the radical criterion, an ad-nilpotent element of the radical lies in the nilradical.
• LieDerivation.apply_mem_nilradical_of_mem_radical: every derivation maps the radical into the nilradical.
• LieDerivation.apply_mem_nilradical_of_mem_nilradical: the nilradical is stable under every derivation.
• LieIdeal.restrict_nilradical: the nilradical of an ideal I is the nilradical of L read inside I.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E, §E.2, the derivation argument in the proof of Proposition E.5.
• [N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1-3][bourbaki1975], Chapter I, §5, for the radical and the nilradical under derivations.
• G. Hochschild, An Addition to Ado's Theorem, Proc. Amer. Math. Soc. 17 (1966), 531–533, for the radical criterion.

theorem LieIdeal.nilradical_le_restrict_nilradical_of_forall {R : Type u_1} {M : Type u_2} [CommRing R] [LieRing M] [LieAlgebra R M] [IsNoetherian R M] (I : LieIdeal R M) (h : ∀ (D : LieDerivation R ↥I ↥I), ∀ z ∈ Ado.LieAlgebra.nilradical R ↥I, D z ∈ Ado.LieAlgebra.nilradical R ↥I) : Ado.LieAlgebra.nilradical R ↥I ≤ I.restrict (Ado.LieAlgebra.nilradical R M)

If the nilradical of an ideal I of a Noetherian Lie algebra M is stable under every derivation of I, then it is an ideal of M, hence contained in the nilradical of M.

theorem LieDerivation.apply_mem_nilradical_of_isSolvable {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [CharZero K] [LieAlgebra.IsSolvable L] (D : LieDerivation K L L) (x : L) : D x ∈ Ado.LieAlgebra.nilradical K L

Every derivation of a finite-dimensional solvable Lie algebra in characteristic zero takes values in its nilradical.

theorem Ado.LieAlgebra.lie_radical_le_nilradical (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [CharZero K] : ⁅⊤, LieAlgebra.radical K L⁆ ≤ nilradical K L

The bracket of a Lie algebra with its radical lies in the nilradical, over a field of characteristic zero.

theorem Ado.LieAlgebra.mem_nilradical_of_mem_radical_of_isNilpotent_ad {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [CharZero K] {x : L} (hx : x ∈ LieAlgebra.radical K L) (hnil : IsNilpotent ((LieAlgebra.ad K L) x)) : x ∈ nilradical K L

The radical criterion: over a field of characteristic zero, an element of the solvable radical of a finite-dimensional Lie algebra whose adjoint action is nilpotent lies in the nilradical.

theorem LieDerivation.apply_mem_nilradical_of_mem_radical {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [CharZero K] (D : LieDerivation K L L) {x : L} (hx : x ∈ LieAlgebra.radical K L) : D x ∈ Ado.LieAlgebra.nilradical K L

Every derivation maps the radical into the nilradical: for a derivation D of a finite-dimensional Lie algebra over a field of characteristic zero, D (radical K L) is contained in nilradical K L.

theorem LieDerivation.apply_mem_nilradical_of_mem_nilradical {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [CharZero K] (D : LieDerivation K L L) {x : L} (hx : x ∈ Ado.LieAlgebra.nilradical K L) : D x ∈ Ado.LieAlgebra.nilradical K L

The nilradical of a finite-dimensional Lie algebra over a field of characteristic zero is stable under every derivation.

@[simp]

theorem LieIdeal.restrict_nilradical {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [CharZero K] (I : LieIdeal K L) : I.restrict (Ado.LieAlgebra.nilradical K L) = Ado.LieAlgebra.nilradical K ↥I

The nilradical of an ideal: over a field of characteristic zero, the nilradical of an ideal I of a finite-dimensional Lie algebra L consists of the elements of I lying in the nilradical of L.