The invariant form is positive definite on the integral weights #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field K of
characteristic zero and let H be a splitting Cartan subalgebra. The invariant form
Ado.invForm of TauCeti/Algebra/Lie/Weights/InvariantForm.lean is symmetric and
non-degenerate on Module.Dual K H, but K carries no order, so "positive definite" cannot be
said of it directly: over ℂ a non-degenerate form may perfectly well vanish on a nonzero vector.
What is true, and what this file proves, is that the form is positive definite on the rational
form of the weight space. A weight is integral (Ado.IsIntegralWeight) when it takes
integer values on every coroot; the weights of finite-dimensional modules are integral
(Ado.exists_int_apply_coroot), and so are the dominant integral weights of the highest-weight
classification. On such a weight lam the scalar ⟨lam, lam⟩ is the image of a rational number,
that rational number is nonnegative, and it is positive unless lam = 0
(Ado.IsIntegralWeight.exists_pos_rat_invForm_self). In particular ⟨lam, lam⟩ ≠ 0.
The argument #
Everything rests on one identity. The Killing form restricted to H is the sum
κ(x, y) = ∑_α α x * α y over the roots (Mathlib's
LieAlgebra.IsKilling.restrict_killingForm_eq_sum), and invForm is the transport of κ|H along
LieAlgebra.IsKilling.cartanEquivDual, so
⟨a, b⟩ = ∑_α ⟨α, a⟩ ⟨α, b⟩
(Ado.invForm_eq_sum_root): the form is a sum of products of the coordinates that the roots
define. Two consequences follow at once. A weight orthogonal to every root is zero
(Ado.eq_zero_of_forall_invForm_root_eq_zero), and ⟨lam, lam⟩ = ∑_α ⟨lam, α⟩².
It remains to see that each coordinate ⟨lam, α⟩ is rational when lam is integral. The
normalisation Ado.invForm_coroot_weight reads ⟨lam, α⟩ = ⟨α, α⟩ lam(α^∨) / 2, so this is
the rationality of the root length ⟨α, α⟩, which the same sum-over-roots identity supplies:
Ado.traceForm_coroot_self_mul_invForm_self_eq_four gives κ(α^∨, α^∨) ⟨α, α⟩ = 4 while
κ(α^∨, α^∨) = ∑_β β(α^∨)² is a sum of squares of Cartan integers, hence an integer, nonnegative
and nonzero.
Main definitions and results #
Ado.invForm_eq_sum_root: the invariant form is the sum over the roots of the products of the coordinates the roots define.Ado.exists_pos_rat_invForm_root_self: a root has positive rational length.Ado.IsIntegralWeight.exists_pos_rat_invForm_self: the invariant form of a nonzero integral weight with itself is a positive rational.Ado.IsIntegralWeight.invForm_self_ne_zero: in particular it is nonzero.
References #
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §8.5, where the form is shown to be positive definite on the rational span of the roots.
This is the positivity behind the Casimir argument of Layer 5 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.
The invariant form as a sum over the roots #
The invariant form is the sum over the roots: ⟨a, b⟩ = ∑_α ⟨α, a⟩ ⟨α, b⟩. The roots
supply a coordinate system in which the form is a sum of products of coordinates, which is all that
positivity needs.
A weight orthogonal to every root vanishes. This is the span of the roots, in the form in which the sum-over-roots identity delivers it.
The length of a root is a positive rational #
The length of a coroot is a nonnegative integer: κ(α^∨, α^∨) = ∑_β β(α^∨)² is a sum of
squares of Cartan integers.
A root has positive rational length. Combining κ(α^∨, α^∨) ⟨α, α⟩ = 4 with the
integrality of κ(α^∨, α^∨) gives ⟨α, α⟩ = 4 / κ(α^∨, α^∨), a positive rational.
Integral weights #
An integral weight has rational coordinates: ⟨lam, α⟩ = ⟨α, α⟩ lam(α^∨) / 2 is rational,
both factors being so.
The invariant form of an integral weight with itself is a nonnegative rational, namely the
sum ∑_α ⟨lam, α⟩² of the squares of its rational coordinates; it vanishes only at lam = 0.
The invariant form is positive definite on the integral weights. For a nonzero integral
weight the scalar ⟨lam, lam⟩ is the image of a positive rational.
A nonzero integral weight has nonzero length.