Ad-nilpotent elements in finite-dimensional representations

Over a field of characteristic zero, an ad-nilpotent element of a finite-dimensional Lie algebra with nondegenerate Killing form acts nilpotently in every finite-dimensional representation. This is the semisimple part of the nilpotence-preservation argument in Hochschild's strengthening of Ado's theorem.

The Killing form supplies t with ⁅x, t⁆ = x. Applying a representation gives a nonzero commutator eigenvalue for the operator representing x. This operator is algebraic because the representation is finite dimensional, so the associative derivation result proves it nilpotent. Neither algebraic closedness nor a choice of sl₂-triple is needed.

For a Killing Lie subalgebra S of a finite-dimensional L, apply the result to the restricted adjoint action on L and the restricted action on a finite-dimensional L-module M. Nilpotence of ad_S s implies nilpotence of ad_L s and of the action of s on M. These applications use the subalgebra and its Killing form, without requiring a decomposition of L.

For an arbitrary finite-dimensional L in characteristic zero, the same conclusion holds on every finite-dimensional L-module on which the nilradical acts nilpotently. Given a Levi complement S, a Lie subalgebra complementary to the solvable radical R, write an ad-nilpotent x as r + s with r ∈ R and s ∈ S. The component s is ad-nilpotent in S, and S ≅ L ⧸ R is Killing, so s acts nilpotently on L and on the module. The nilpotent-extension lemma, applied on L to the span of s and the nilradical N and then to its extension by x, which normalizes it because ⁅L, R⁆ ≤ N, shows that r = x - s is ad-nilpotent; the radical criterion gives r ∈ N. On the module, s and N act nilpotently, hence so does x = s + r.

Main results

• TauCeti.isNilpotent_apply_of_lie_eq_smul: a nonzero adjoint eigenvalue forces nilpotence in every finite-dimensional representation.
• TauCeti.isNilpotent_toEnd_of_isNilpotent_ad: ad-nilpotence in a finite-dimensional Killing Lie algebra implies nilpotence in every finite-dimensional Lie module.
• TauCeti.isNilpotent_apply_of_isNilpotent_ad: the same result for an explicit Lie homomorphism into an endomorphism algebra.
• LieHom.isNilpotent_apply_iff_isNilpotent_ad: under a faithful representation, ad-nilpotence is detected by nilpotence of the image.
• LieSubalgebra.isNilpotent_toEnd_of_isNilpotent_ad_of_isCompl_radical: in characteristic zero, an ad-nilpotent element acts nilpotently on every finite-dimensional module on which the nilradical acts nilpotently.
• LieSubalgebra.isNilpotent_apply_of_isNilpotent_ad_of_isCompl_radical: the same result for an explicit Lie homomorphism into an endomorphism algebra.

References

• G. Hochschild, An Addition to Ado's Theorem, Proc. Amer. Math. Soc. 17 (1966), 531–533.

theorem TauCeti.isNilpotent_apply_of_lie_eq_smul {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [FiniteDimensional K M] {ρ : L →ₗ⁅K⁆ Module.End K M} {x y : L} {c : K} (hc : c ≠ 0) (hxy : ⁅y, x⁆ = c • x) : IsNilpotent (ρ x)

An element with nonzero eigenvalue for an adjoint action has nilpotent image in every finite-dimensional representation in characteristic zero. The Lie algebra need not be finite dimensional or semisimple.

theorem TauCeti.isNilpotent_apply_of_isNilpotent_ad {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [FiniteDimensional K M] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {ρ : L →ₗ⁅K⁆ Module.End K M} {x : L} (hx : IsNilpotent ((LieAlgebra.ad K L) x)) : IsNilpotent (ρ x)

An ad-nilpotent element has nilpotent image under every finite-dimensional representation of a Killing Lie algebra over a characteristic-zero field.

theorem TauCeti.isNilpotent_toEnd_of_isNilpotent_ad {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [FiniteDimensional K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {x : L} (hx : IsNilpotent ((LieAlgebra.ad K L) x)) : IsNilpotent ((LieModule.toEnd K L M) x)

An ad-nilpotent element of a finite-dimensional Killing Lie algebra acts nilpotently in every finite-dimensional Lie module over a characteristic-zero field.

theorem LieHom.isNilpotent_apply_iff_isNilpotent_ad {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (ρ : L →ₗ⁅K⁆ Module.End K M) (hρ : Function.Injective ⇑ρ) (x : L) : IsNilpotent (ρ x) ↔ IsNilpotent ((LieAlgebra.ad K L) x)

Under a faithful finite-dimensional representation, an element of a Killing Lie algebra over a field of characteristic zero is ad-nilpotent exactly when its image is nilpotent.

theorem LieSubalgebra.isNilpotent_toEnd_of_isNilpotent_ad_of_isCompl_radical {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [FiniteDimensional K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K L] (S : LieSubalgebra K L) (hS : IsCompl (↑(LieAlgebra.radical K L)) S.toSubmodule) (hM : ∀ n ∈ TauCeti.LieAlgebra.nilradical K L, IsNilpotent ((LieModule.toEnd K L M) n)) {x : L} (hx : IsNilpotent ((LieAlgebra.ad K L) x)) : IsNilpotent ((LieModule.toEnd K L M) x)

Hochschild's nilpotence theorem in characteristic zero: if the nilradical of a finite-dimensional Lie algebra L acts nilpotently on a finite-dimensional L-module M, then so does every ad-nilpotent element of L. The Lie subalgebra S is any Levi complement, that is, any complement of the solvable radical; the conclusion does not depend on it.

theorem LieSubalgebra.isNilpotent_apply_of_isNilpotent_ad_of_isCompl_radical {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [FiniteDimensional K M] [FiniteDimensional K L] (S : LieSubalgebra K L) (hS : IsCompl (↑(LieAlgebra.radical K L)) S.toSubmodule) {ρ : L →ₗ⁅K⁆ Module.End K M} (hρ : ∀ n ∈ TauCeti.LieAlgebra.nilradical K L, IsNilpotent (ρ n)) {x : L} (hx : IsNilpotent ((LieAlgebra.ad K L) x)) : IsNilpotent (ρ x)

The form of isNilpotent_toEnd_of_isNilpotent_ad_of_isCompl_radical for an explicit Lie homomorphism into an endomorphism algebra: if every element of the nilradical has nilpotent image, then so does every ad-nilpotent element.