The Weyl vector and dominance through the coroot pairings #
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 its root
system. TauCeti/Algebra/Lie/Weights/WeightLattice.lean builds the integral weight lattice
TauCeti.integralWeightLattice H and the integer coroot pairings
TauCeti.coweightPairing lam i = ⟨lam, αᵢ^∨⟩; this file adds what the highest-weight theory needs
of them, namely the Weyl vector ρ of b and the reading of dominance through those integers.
The Weyl vector pairs to 1 with every simple coroot, so it is a dominant integral weight and in
particular lies in the lattice. Dominance itself becomes an inequality between integers:
TauCeti.IsDominantIntegral b lam says exactly that lam is integral and that every simple coroot
pairing ⟨lam, αᵢ^∨⟩ is nonnegative. That reformulation is what makes the ρ-shift usable: the
pairings of lam + ρ are those of lam raised by one, hence strictly positive. Over a field
with no order none of this can be said about the values in K at all.
Main results #
TauCeti.isDominantIntegral_weylVectorandTauCeti.weylVector_mem_integralWeightLattice: the Weyl vectorρis a dominant integral weight, and so lies in the integral weight lattice.TauCeti.coweightPairing_weylVector:⟨ρ, αᵢ^∨⟩ = 1for a simple rootαᵢ, as an integer, andTauCeti.coweightPairing_weylVector_ne_zero:⟨ρ, α^∨⟩ ≠ 0for every rootα.TauCeti.coweightPairing_add_weylVector: theρ-shift raises every simple coroot pairing by one.TauCeti.isDominantIntegral_iff_isIntegralWeight_and_forall_coweightPairing_nonneg: a weight is dominant exactly when it is integral and its simple coroot pairings are nonnegative integers.TauCeti.IsDominantIntegral.coweightPairing_add_weylVector_pos: theρ-shift of a dominant integral weight has strictly positive simple coroot pairings.
References #
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §13.2.
The Weyl vector #
The Weyl vector is dominant integral: it pairs to 1 with every simple coroot.
The Weyl vector lies in the integral weight lattice. Dominance gives its values on the
simple coroots, and TauCeti.IsDominantIntegral.isIntegralWeight propagates integrality to all of
them.
The Weyl vector pairs to one with every simple coroot, ⟨ρ, αᵢ^∨⟩ = 1, as an integer.
The Weyl vector pairs to a nonzero integer with every coroot, simple or not: the pairing
is the height of the coroot (TauCeti.coroot'_weylVector_eq_height_flip). These are the
denominators of the Weyl dimension formula.
The ρ-shift raises every simple coroot pairing by one, as an identity of integers.
Dominance through the coroot pairings #
A dominant integral weight has nonnegative pairings against every positive coroot, not only the simple ones.
A dominant integral weight has nonnegative simple coroot pairings, a simple root being positive.
Dominance is integrality together with nonnegativity of the simple coroot pairings. The
dominance condition of TauCeti.IsDominantIntegral is exactly an inequality between integers,
dominance supplying the integrality that makes those integers meaningful.
The ρ-shift of a dominant integral weight is strictly dominant. This is the role of ρ
in the highest-weight theory, and it is an inequality between integers: over a field with no order
it cannot be stated about the values in K at all.