Morozov's lemma

Let L be a Lie algebra over a field K of characteristic zero, and let e, h ∈ L with ad e nilpotent, ⁅h, e⁆ = 2 • e and h ∈ [e, L]. Morozov's lemma says that (h, e) extends to an sl₂ triple: there is f with ⁅e, f⁆ = h and ⁅h, f⁆ = -2 • f. Moreover f is unique. No finite-dimensionality or nondegeneracy assumption on L is needed.

This is the second half of the Jacobson–Morozov theorem: the first half produces, for an ad-nilpotent e in a finite-dimensional Lie algebra with nondegenerate Killing form, an element h ∈ [e, L] with ⁅h, e⁆ = 2 • e. The hypotheses here are exactly that output.

The key point is that the eigenvalues of ad h on the centralizer ker (ad e) are natural numbers. This is proved at the level of operators: if E, H, Z are endomorphisms of a vector space with E nilpotent, E * Z - Z * E = H and H * E - E * H = 2 • E, then H preserves ker E, and on the decreasing filtration ker E ⊓ range (E ^ k) the operator H - k maps the k-th step into the (k + 1)-st. Since the filtration reaches 0 at the nilpotency index of E, the operator H - a is bijective on ker E for every a that is not a natural number. For the Lie algebra statement take E = ad e, H = ad h and Z = ad z where h = ⁅e, z⁆; the operator form applies equally to the images of e, h, z in any representation in which the image of e is nilpotent.

The individual filtration-step lemmas only require k + 1 to be nonzero in K, and are stated over fields of arbitrary characteristic with this assumption.

Mathlib's IsSl2Triple.HasPrimitiveVectorWith.exists_nat reaches the same kind of conclusion for a primitive vector of a complete sl₂ triple acting on a Noetherian module. Here the third element f is what is being constructed and no finiteness is assumed; the nilpotence of E replaces both.

Main results

• TauCeti.Sl2.exists_eq_natCast_of_apply_eq_smul: an eigenvalue of H on ker E is a natural number.
• TauCeti.Sl2.exists_mem_ker_apply_sub_smul_eq: for a not a natural number, H - a maps ker E onto itself.
• TauCeti.Sl2.apply_sub_smul_mem_ker_inf_range_pow_succ and its adjoint form TauCeti.lie_sub_smul_mem_ker_inf_range_pow_succ: H - k maps the k-th step of the filtration ker E ⊓ range (E ^ k) into the next one.
• TauCeti.exists_eq_natCast_of_lie_eq_smul: an eigenvalue of ad h on the centralizer of e is a natural number.
• TauCeti.existsUnique_lie_eq_and_lie_eq_neg_two_nsmul: Morozov's lemma, with uniqueness of the third element, and without assuming h ≠ 0.
• TauCeti.existsUnique_isSl2Triple_of_isNilpotent_ad: the same statement for Mathlib's IsSl2Triple, when h ≠ 0.

References

• V. V. Morozov, On a nilpotent element in a semi-simple Lie algebra, C. R. (Doklady) Acad. Sci. URSS (N.S.) 36 (1942), 83–86.
• N. Jacobson, Lie Algebras, Interscience, 1962, Chapter III, §11, Lemma 7.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 7–9, Chapter VIII, §11, no. 2.

theorem TauCeti.Sl2.apply_sub_smul_mem_ker_inf_range_pow_succ {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {E H Z : Module.End K V} (hEZ : E * Z - Z * E = H) (hHE : H * E - E * H = 2 • E) {k : ℕ} [NeZero ↑(k + 1)] {c : V} (hc : c ∈ LinearMap.ker E ⊓ LinearMap.range (E ^ k)) : H c - ↑k • c ∈ LinearMap.ker E ⊓ LinearMap.range (E ^ (k + 1))

If k + 1 is nonzero in K, then H - k maps the k-th step ker E ⊓ range (E ^ k) of the filtration into the next one.

theorem TauCeti.Sl2.exists_eq_natCast_of_apply_eq_smul {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {E H Z : Module.End K V} [CharZero K] (hE : IsNilpotent E) (hEZ : E * Z - Z * E = H) (hHE : H * E - E * H = 2 • E) {c : V} (hc : E c = 0) (hc0 : c ≠ 0) {a : K} (hHc : H c = a • c) : ∃ (n : ℕ), a = ↑n

Let E be nilpotent, with E * Z - Z * E = H and H * E - E * H = 2 • E. Then every eigenvalue of H on ker E is a natural number.

theorem TauCeti.Sl2.exists_mem_ker_apply_sub_smul_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {E H Z : Module.End K V} [CharZero K] (hE : IsNilpotent E) (hEZ : E * Z - Z * E = H) (hHE : H * E - E * H = 2 • E) {a : K} (ha : ∀ (n : ℕ), a ≠ ↑n) {w : V} (hw : w ∈ LinearMap.ker E) : ∃ c ∈ LinearMap.ker E, H c - a • c = w

Let E be nilpotent, with E * Z - Z * E = H and H * E - E * H = 2 • E. If a is not a natural number, then H - a maps ker E onto ker E.

theorem TauCeti.exists_eq_natCast_of_lie_eq_smul {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] {h e : L} (he : IsNilpotent ((LieAlgebra.ad K L) e)) (hhe : ⁅h, e⁆ = 2 • e) (hh : h ∈ LinearMap.range ((LieAlgebra.ad K L) e)) {c : L} (hc : ⁅e, c⁆ = 0) (hc0 : c ≠ 0) {a : K} (hhc : ⁅h, c⁆ = a • c) : ∃ (n : ℕ), a = ↑n

Let ad e be nilpotent, ⁅h, e⁆ = 2 • e and h ∈ [e, L]. Then every eigenvalue of ad h on the centralizer of e is a natural number.

theorem TauCeti.lie_sub_smul_mem_ker_inf_range_pow_succ {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] {h e : L} (hhe : ⁅h, e⁆ = 2 • e) (hh : h ∈ LinearMap.range ((LieAlgebra.ad K L) e)) {k : ℕ} [NeZero ↑(k + 1)] {c : L} (hc : c ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e ^ k)) : ⁅h, c⁆ - ↑k • c ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e ^ (k + 1))

Let ⁅h, e⁆ = 2 • e and h ∈ [e, L]. If k + 1 is nonzero in K, then ad h - k maps the k-th step ker (ad e) ⊓ range ((ad e) ^ k) of the filtration of the centralizer of e into the next one.

theorem TauCeti.existsUnique_lie_eq_and_lie_eq_neg_two_nsmul {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] {h e : L} (he : IsNilpotent ((LieAlgebra.ad K L) e)) (hhe : ⁅h, e⁆ = 2 • e) (hh : h ∈ LinearMap.range ((LieAlgebra.ad K L) e)) : ∃! f : L, ⁅e, f⁆ = h ∧ ⁅h, f⁆ = -(2 • f)

Morozov's lemma. Let ad e be nilpotent, ⁅h, e⁆ = 2 • e and h ∈ [e, L], over a field of characteristic zero. Then there is a unique f with ⁅e, f⁆ = h and ⁅h, f⁆ = -(2 • f). The case h = 0 is allowed.

theorem TauCeti.existsUnique_isSl2Triple_of_isNilpotent_ad {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] {h e : L} (he : IsNilpotent ((LieAlgebra.ad K L) e)) (hhe : ⁅h, e⁆ = 2 • e) (hh : h ∈ LinearMap.range ((LieAlgebra.ad K L) e)) (h0 : h ≠ 0) : ∃! f : L, IsSl2Triple h e f

Morozov's lemma for sl₂ triples. Let ad e be nilpotent, ⁅h, e⁆ = 2 • e, h ≠ 0 and h ∈ [e, L], over a field of characteristic zero. Then there is a unique f such that (h, e, f) is an sl₂ triple.