The simple root values of a dominant neutral element lie in {0, 1, 2}

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field K of characteristic zero, let H be a splitting Cartan subalgebra and let b be a base of the root system LieAlgebra.IsKilling.rootSystem H. Call x : H dominant when every simple root takes a natural-number value at x.

If (h, e, f) is an sl₂ triple whose neutral element h lies in H and is dominant, then every simple root takes one of the values 0, 1 or 2 at h (IsSl2Triple.root_apply_eq_zero_or_eq_one_or_eq_two). Labelling each node of the Dynkin diagram by this value gives the weighted Dynkin diagram of the triple. Because the simple roots span the dual of H, the labels determine h, so the bound leaves only finitely many possible dominant neutral elements in H.

The argument

Suppose a simple root α has α h = n ≥ 3. A nonzero vector y of the root space L_{-α} has h-eigenvalue -n, which is not a natural number, so ⁅e, y⁆ ≠ 0 (IsSl2Triple.disjoint_ker_toEnd_e_eigenspace). On the other hand e lies in the 2-eigenspace of ad h, which is the sum of the root spaces L_χ with χ h = 2 (LieModule.genWeightSpaceOf_eq_iSup_genWeightSpace), and ⁅y, L_χ⁆ ⊆ L_{χ - α}. If χ - α were a root γ, then γ h = 2 - n < 0 forces γ to be negative, while χ h = 2 > 0 forces χ to be positive, so α = χ + (-γ) would be a sum of two positive roots, which a simple root is not (TauCeti.root_ne_add_of_mem_support). Hence every L_{χ - α} vanishes and ⁅e, y⁆ = 0, a contradiction.

The sign information used here comes from dominance alone: a dominant element takes natural values on the positive roots (TauCeti.exists_nat_root_apply_of_mem_posRoots) and the negatives of natural values on the negative ones (TauCeti.exists_nat_root_apply_eq_neg_of_mem_negRoots).

Main results

• IsSl2Triple.root_apply_eq_zero_or_eq_one_or_eq_two: the simple root values of a dominant neutral element lie in {0, 1, 2}.

References

• D. H. Collingwood and W. M. McGovern, Nilpotent Orbits in Semisimple Lie Algebras, Van Nostrand Reinhold, 1993, §3.5.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 7–9, Chapter VIII, §11.

theorem IsSl2Triple.root_apply_eq_zero_or_eq_one_or_eq_two {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {h : ↥H} {e f : L} (t : IsSl2Triple (↑h) e f) (hh : ∀ j ∈ b.support, ∃ (n : ℕ), ↑j h = ↑n) {i : ↥LieSubalgebra.root} (hi : i ∈ b.support) : ↑i h = 0 ∨ ↑i h = 1 ∨ ↑i h = 2

The simple root values of a dominant neutral element lie in {0, 1, 2}. If the neutral element h of an sl₂ triple lies in the Cartan subalgebra H and every simple root takes a natural value at h, then each simple root takes the value 0, 1 or 2 at h. These values label the weighted Dynkin diagram of the triple.