The Jacobson–Morozov theorem and conjugacy of sl₂ triples

Let L be a finite-dimensional Lie algebra over a field K of characteristic zero.

The Jacobson–Morozov theorem says that, when the Killing form of L is nondegenerate, every nonzero e ∈ L with ad e nilpotent is the nilpositive element of an sl₂ triple (h, e, f). It is assembled here from its two halves: TauCeti.exists_mem_range_ad_lie_eq_two_nsmul_of_isNilpotent_ad finds h ∈ [e, L] with ⁅h, e⁆ = 2 • e, and Morozov's lemma TauCeti.existsUnique_isSl2Triple_of_isNilpotent_ad completes (h, e) to a triple.

Write 𝔲 = ker (ad e) ⊓ [e, L]. Every y ∈ 𝔲 has nilpotent adjoint action (Jacobson's lemma, TauCeti.isNilpotent_ad_of_mem_ker_inf_range), so exp (ad y) is an automorphism of L fixing e. Kostant's conjugacy theorem says that the triple attached to e is unique up to the subgroup generated by these automorphisms: if (h, e, f) and (h', e, f') are two triples, then a product of such automorphisms carries the first to the second. Moreover the neutral elements of the triples containing e are exactly the points of the affine space h + 𝔲.

The argument

The proof runs along the filtration 𝔲ₖ = ker (ad e) ⊓ range ((ad e) ^ k) of the centralizer of e, which reaches 0 at the nilpotency index of ad e. It is compatible with brackets, ⁅𝔲ᵢ, 𝔲ⱼ⁆ ⊆ 𝔲ᵢ₊ⱼ (TauCeti.lie_mem_ker_inf_range_pow_add, in TauCeti.Algebra.Lie.AdjointAction.CentralizerFiltration), so exp (ad y) with y ∈ 𝔲ₖ acts as 1 + ad y up to 𝔲₂ₖ (TauCeti.expAd_apply_sub_sub_mem, in TauCeti.Algebra.Lie.AdjointAction.ExpAdSubgroup). By Morozov's eigenvalue analysis ad h acts on 𝔲ₖ / 𝔲ₖ₊₁ by the scalar k (TauCeti.lie_sub_smul_mem_ker_inf_range_pow_succ). Hence if h' - h = z ∈ 𝔲ₖ with k ≥ 1, then for y = k⁻¹ • z the automorphism exp (ad y) moves h' to a neutral element h'' with h'' - h ∈ 𝔲ₖ₊₁. A descending induction on k finishes the construction. The third elements then correspond by the uniqueness half of Morozov's lemma.

Main results

• TauCeti.exists_isSl2Triple_of_isNilpotent_ad: the Jacobson–Morozov theorem.
• TauCeti.exists_isSl2Triple_iff: in such a Lie algebra, e is the nilpositive element of an sl₂ triple if and only if e ≠ 0 and ad e is nilpotent.
• IsSl2Triple.exists_isSl2Triple_iff_sub_mem: the neutral elements of the triples containing e form the affine space h + (ker (ad e) ⊓ [e, L]).
• IsSl2Triple.exists_lieEquiv_apply_eq: Kostant's conjugacy theorem. Two triples with the same nilpositive element are conjugate by an automorphism in TauCeti.expAdSubgroup, the subgroup generated by the exp (ad y) with y ∈ ker (ad e) ⊓ [e, L] (in TauCeti.Algebra.Lie.AdjointAction.ExpAdSubgroup).

References

• N. Jacobson, Lie Algebras, Interscience, 1962, Chapter III, §11.
• B. Kostant, The principal three-dimensional subgroup and the Betti numbers of a complex simple Lie group, Amer. J. Math. 81 (1959), 973–1032.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 7–9, Chapter VIII, §11.
• D. H. Collingwood and W. M. McGovern, Nilpotent Orbits in Semisimple Lie Algebras, Van Nostrand Reinhold, 1993, §3.3 and §3.4.

The Jacobson–Morozov theorem

theorem TauCeti.exists_isSl2Triple_of_isNilpotent_ad {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {e : L} (he : IsNilpotent ((LieAlgebra.ad K L) e)) (he0 : e ≠ 0) : ∃ (h : L) (f : L), IsSl2Triple h e f

The Jacobson–Morozov theorem. In a finite-dimensional Lie algebra with nondegenerate Killing form over a field of characteristic zero, every nonzero ad-nilpotent element e is the nilpositive element of an sl₂ triple (h, e, f).

theorem TauCeti.exists_isSl2Triple_iff {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {e : L} : (∃ (h : L) (f : L), IsSl2Triple h e f) ↔ IsNilpotent ((LieAlgebra.ad K L) e) ∧ e ≠ 0

In a finite-dimensional Lie algebra with nondegenerate Killing form over a field of characteristic zero, the nilpositive elements of sl₂ triples are exactly the nonzero ad-nilpotent elements.

Conjugacy of triples with a common nilpositive element

theorem IsSl2Triple.exists_isSl2Triple_iff_sub_mem {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f : L} (t : IsSl2Triple h e f) {h' : L} : (∃ (f' : L), IsSl2Triple h' e f') ↔ h' - h ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e)

The neutral elements attached to a nilpositive element. Given an sl₂ triple (h, e, f) in a finite-dimensional Lie algebra over a field of characteristic zero, the elements h' completing e to a triple (h', e, f') are exactly those of the affine space h + (ker (ad e) ⊓ [e, L]).

theorem IsSl2Triple.exists_lieEquiv_apply_eq {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {h e f : L} [LieAlgebra ℚ L] (t : IsSl2Triple h e f) {h' f' : L} (t' : IsSl2Triple h' e f') : ∃ (φ : L ≃ₗ⁅K⁆ L), φ.toLinearEquiv ∈ TauCeti.expAdSubgroup K e ∧ φ e = e ∧ φ h = h' ∧ φ f = f'

Kostant's conjugacy theorem. Two sl₂ triples (h, e, f) and (h', e, f') with the same nilpositive element in a finite-dimensional Lie algebra over a field of characteristic zero are conjugate by an automorphism of L that fixes e and lies in the subgroup TauCeti.expAdSubgroup K e generated by the automorphisms exp (ad y) with y ∈ ker (ad e) ⊓ [e, L].