The dimension count of the root-space decomposition #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field of
characteristic zero, and let H be a splitting Cartan subalgebra. The root-space decomposition
writes L as the internal direct sum of one root space for each weight of H on L; the zero
weight contributes H itself, and every other root space is a line
(LieAlgebra.IsKilling.finrank_rootSpace_eq_one). Counting dimensions there gives
dim L = dim H + #Δ,
and, after choosing a base of the root system, the parity identity
dim L = dim H + 2 · #Δ⁺,
because root negation exchanges the positive and the negative roots
(TauCeti.two_mul_ncard_posRoots). Both identities are stated additively, with no truncated
subtraction, so that a consumer forming the exponents (dim L ± dim H) / 2 reads off an exact
division.
The dim H summand comes from the zero root space, which for a Cartan subalgebra is H itself
(LieAlgebra.rootSpace_zero_eq). TauCeti.finrank_rootSpace_zero_eq_finrank_cartan records this
at the level of dimensions, covering also the degenerate case H = ⊥, where the zero functional is
not a weight at all and both sides vanish; that is why the sum below is split over H.root and its
complement rather than by removing a named zero weight, which need not exist.
Main results #
TauCeti.isInternal_rootSpace:Lis the internal direct sum of the root spaces ofH, indexed by the weights ofHonL. Only nilpotency ofHand triangularizability are needed here.TauCeti.finrank_rootSpace_zero_eq_finrank_cartan: the zero root space has the dimension ofH.TauCeti.finrank_eq_finrank_cartan_add_card_root:dim L = dim H + #Δ.TauCeti.card_root_sum_support_eq_finrank: the roots together with the support of a base have cardinalitydim L.TauCeti.card_root_eq_two_mul_ncard_posRoots:#Δ = 2 · #Δ⁺, andTauCeti.even_card_rootthe parity of#Δit gives.TauCeti.finrank_eq_finrank_cartan_add_two_mul_ncard_posRootsandTauCeti.finrank_eq_finrank_cartan_add_two_mul_card_isPos:dim L = dim H + 2 · #Δ⁺, with the positive roots counted as a set and as aFinset.
References #
This is the numerical shadow of the root-space decomposition of Layer 1 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, "L = H ⊕ ⨁_{α ∈ roots} Lα with
finrank_rootSpace_eq_one making each Lα a line".
It is a prerequisite for, and not an instance of, the bookkeeping pin
finrank_eq_rank_add_two_mul_card_isPos of Layer 9 of
TauCetiRoadmap/RepresentationTheory/SpinRepresentations/README.md: that pin states the parity
identity with LieAlgebra.rank ℂ L where the count below gives dim H. Bridging the two is the
separate Layer 9 target rank_eq_finrank_cartan, which compares Mathlib's LieAlgebra.rank,
defined through the nilpotency degree of a generic element, with the dimension of a Cartan
subalgebra; it is not proved here, and no declaration below claims that pin.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Springer GTM 9 (1972), §8.1 (the root-space decomposition) and §10.1 (the pairing of positive and negative roots).
The root-space decomposition. A finite-dimensional Lie algebra that is triangularizable
over a nilpotent subalgebra H is the internal direct sum of the root spaces of H, indexed by
all the weights of H on L. For a Cartan subalgebra the nonzero weights are the roots, and the
zero weight, when it is a weight at all, contributes H itself.
This is TauCeti.isInternal_genWeightSpace for the adjoint action of H on L, a root space
being by definition the generalized weight space of that action.
The zero root space is the Cartan subalgebra, at the level of dimensions. When the zero
functional is not a weight of H on L both sides vanish, since then H itself is trivial.
The dimension count of the root-space decomposition: the dimension of a Lie algebra with
non-degenerate Killing form is the dimension of a splitting Cartan subalgebra plus the number of
roots. The Cartan subalgebra has to be splitting — that is, L has to be triangularizable over it
— or there are too few roots: over ℝ, the compact form su(2) has a non-degenerate Killing form
and a one-dimensional Cartan subalgebra, but no root at all, and dim L = 3.
The index set consisting of every root and every simple root has cardinality equal to the dimension of the Lie algebra.
The number of roots is twice the number of positive roots for any base, since root negation exchanges the positive and the negative roots.
The parity identity d = l + 2 · #Δ⁺: the dimension of a Lie algebra with non-degenerate
Killing form is the dimension of a splitting Cartan subalgebra plus twice the number of positive
roots, for any base of its root system.
The parity identity d = l + 2 · #Δ⁺, with the positive roots counted as a Finset of the
root index type.
The number of roots is even: root negation pairs them up. No base has to be supplied, since
one always exists (RootPairing.nonempty_base).