Structure constants along a root string #
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 α and β be roots with
α non-zero. Writing the α-string through β as β - pα, …, β, …, β + qα, so that
p = chainBotCoeff α β and q = chainTopCoeff α β, this file proves the ladder identity
⁅f, ⁅e, y⁆⁆ = (q * (p + 1)) • y for y ∈ Lβ
for an sl₂ triple (h, e, f) with e ∈ Lα and f ∈ L(-α), together with the consequences that
make it the first step of the Chevalley basis theorem. Choosing non-zero root vectors y ∈ Lβ and
z ∈ L(α + β) and writing ⁅e, y⁆ = N • z and ⁅f, z⁆ = N' • y, the identity gives the product
constraint N * N' = q * (p + 1). Integrality of the individual constants and the normalization
N = ±(p + 1) additionally require a coherent normalization of root vectors and symmetry
relations among the constants.
Main results #
TauCeti.lie_f_lie_e_eq_nsmul_of_mem_rootSpace: the ladder identity above, andTauCeti.lie_e_lie_f_eq_nsmul_of_mem_rootSpaceits mirror⁅e, ⁅f, y⁆⁆ = (p * (q + 1)) • y.TauCeti.lie_ne_zero_of_mem_rootSpace: ifα + βis a root then⁅e, y⁆ ≠ 0for every non-zeroe ∈ Lαandy ∈ Lβ.TauCeti.exists_mem_rootSpace_lie_eq:⁅e, ·⁆mapsLβontoL(α + β), so that⁅Lα, Lβ⁆ = L(α + β).TauCeti.exists_lie_eq_smulandTauCeti.ne_zero_of_lie_eq_smul: the structure constant of a pair of root vectors exists and is non-zero.TauCeti.mul_eq_of_lie_eq_smul: the two structure constants of a root string multiply toq * (p + 1).TauCeti.IsSl2System.chainTopCoeff_mul_killingForm_root_neg_eq: normalized Killing pairings at consecutive roots have the reciprocal root-length ratio.
Implementation notes #
The proof is the standard sl₂ ladder computation, run against the primitive vector at the top of
the string. Mathlib already builds that primitive vector, in the course of proving
LieAlgebra.IsKilling.exists_mem_rootSpace_lie_ne_zero, but only records the existence of a pair
of root vectors with non-zero bracket. Because each root space is a line
(LieAlgebra.IsKilling.finrank_rootSpace_eq_one), the value of ⁅f, ⁅e, ·⁆⁆ on the whole of Lβ
is determined by its value on f ^ q applied to that primitive vector, which is what turns the
existential into the identity proved here; TauCeti.lie_ne_zero_of_mem_rootSpace is then the
universally quantified form of Mathlib's lemma.
The scalar is stated as an ℕ-scalar action rather than as a cast into K to expose the
combinatorial root-string coefficient directly.
The root-length ratio at the end reads the chain coefficients off the root system through the
invariant form on weights, which is TauCeti.rootInvariantForm.
References #
This file advances the target "The Chevalley--Demazure construction" of Layer 9 of
TauCetiRoadmap/ReductiveGroups/README.md, which builds the pinned group scheme over ℤ "via a
Chevalley basis and the Kostant ℤ-form of the enveloping algebra": the structure constants of a
Chevalley basis are the numbers N above. The product constraint N * N' = q * (p + 1), together
with a coherent normalization of root vectors and additional symmetry relations, leads to the
integral normalization N = ±(p + 1).
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §25.1--25.2.
- R. W. Carter, Simple Groups of Lie Type, §4.1.
The ladder identity #
The ladder identity along a root string. If (h, e, f) is an sl₂ triple with e in the
root space of a non-zero root α and f in the root space of -α, then for every y in the
root space of a non-zero root β,
⁅f, ⁅e, y⁆⁆ = (q * (p + 1)) • y,
where β - pα, …, β, …, β + qα is the α-string through β.
The scalar is a natural number; this is Humphreys, Introduction to Lie Algebras and Representation Theory, §25.1.
The ladder identity read down the string instead of up it: with the same notation,
⁅e, ⁅f, y⁆⁆ = (p * (q + 1)) • y for y ∈ Lβ.
Consequences for the structure constants #
If α + β is a root then every non-zero root vector of α brackets every non-zero root
vector of β to something non-zero. This is the universally quantified form of Mathlib's
LieAlgebra.IsKilling.exists_mem_rootSpace_lie_ne_zero.
The bracket with a non-zero root vector of α maps the root space of β onto the root
space of α + β. Together with TauCeti.lie_ne_zero_of_mem_rootSpace this is the statement
⁅Lα, Lβ⁆ = L(α + β) for roots α, β whose sum is a root.
The structure constant of a triple of root vectors exists: the bracket of a root vector of α
with one of β is a multiple of any non-zero root vector of α + β.
A structure constant of a pair of roots whose sum is a root is non-zero.
The two structure constants of a root string multiply to q * (p + 1), where
β - pα, …, β, …, β + qα is the α-string through β. Choosing e, f and z so that
⁅e, y⁆ = N • z and ⁅f, z⁆ = N' • y, this says N * N' = q * (p + 1). Integrality of the
individual constants and the Chevalley normalization N = ±(p + 1) additionally require a
coherent normalization of root vectors and symmetry relations among the constants.
The root-length ratio #
The root system of a Killing Lie algebra and its Lie weight strings have the same ascending and descending chain coefficients.
Root-string ratio for normalized Killing pairings. If γ = α + β, then
q B(x β, x (-β)) = (p + 1) B(x γ, x (-γ)),
where p = chainBotCoeff α β and q = chainTopCoeff α β. This reciprocal form of the
invariant root-length identity supplies the cancellation used to normalize Chevalley structure
constants.