Minuscule weights #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically
closed field of characteristic zero, let H be a Cartan subalgebra and b a base of its root
system. A dominant integral weight mu is minuscule when every weight of the irreducible
module L(mu) lies in the Weyl orbit of mu; if L(mu) is nonzero its weights are then exactly
that orbit. This file defines TauCeti.IsMinuscule and proves the dimension count that the orbit
condition buys: a highest weight module whose weights lie in one Weyl orbit has
dim M = |W · lam|,
the dimension being the size of a Weyl orbit — a purely combinatorial count, with no Weyl character formula in sight.
Why the orbit condition does all the work #
Two facts about the formal character of TauCeti/Algebra/Lie/Weights/FormalCharacter.lean combine
to give everything. Its coefficient at the highest weight of a highest weight module is 1
(TauCeti.formalCharacter_coeff_eq_one_of_isHighestWeightVector_of_lieSpan_eq_top, the top weight
space being the line spanned by the generator); and it is Weyl-invariant
(TauCeti.formalCharacter_coeff_weylGroup_smul, the Weyl invariance of weight multiplicities,
proved from the rank-one theory and not from the character formula). So every weight in the orbit
of the highest weight already has multiplicity 1, whatever the module
(formalCharacter_coeff_weylGroup_smul_eq_one_of_isHighestWeightVector_of_lieSpan_eq_top); the
orbit condition is exactly the statement that there are no other weights, and the dimension is
then the number of coefficients, all of them 1.
Accordingly the substance of the file is stated for an arbitrary finite-dimensional module
generated by a highest weight vector whose weights lie in one orbit
(TauCeti.finrank_eq_card_orbit_of_isHighestWeightVector_of_lieSpan_eq_top). That statement is
unconditional: it assumes a highest weight vector and produces the dimension of its orbit.
The named carrier #
TauCeti.irreducibleQuotient is built from the Verma module, and its canonical generator is a
highest weight vector of weight mu (TauCeti.isHighestWeightVector_irreducibleQuotientGenerator).
So at a minuscule weight the count applies to the named carrier,
TauCeti.IsMinuscule.finrank_irreducibleQuotient_eq_card_orbit, dim L(mu) = |W · mu|.
At the zero weight the count is complete: TauCeti.isMinuscule_zero proves 0 minuscule, and
TauCeti.finrank_irreducibleQuotient_zero, which needs only triviality, agrees that
dim L(0) = 1.
Main definitions #
TauCeti.IsMinuscule:muis dominant integral and every weight ofL(mu)is Weyl-conjugate tomu, withTauCeti.isMinuscule_iffits defining characterization.
Main results #
TauCeti.finrank_eq_card_orbit_of_isHighestWeightVector_of_lieSpan_eq_top: a highest weight module whose weights lie in one Weyl orbit has the dimension of that orbit, the substance of the file. It rests on the fact that the orbit of the highest weight consists of weights, all of them simple (formalCharacter_coeff_weylGroup_smul_eq_one_of_isHighestWeightVector_of_lieSpan_eq_top), and hence that the orbit condition makes the weights exactly the orbit (genWeightSpace_ne_bot_iff_mem_orbit_of_isHighestWeightVector_of_lieSpan_eq_top).TauCeti.IsMinuscule.finrank_irreducibleQuotient_eq_card_orbit:dim L(mu) = |W · mu|, the dimension count at the named carrier.TauCeti.isMinuscule_zero: the zero weight is minuscule, so the notion is not empty. It is unconditional, and the point orbit it exhibits matches the one-dimensionality ofL(0)recorded byTauCeti.finrank_irreducibleQuotient_zero.
Implementation notes #
The Weyl group acts here as (LieAlgebra.IsKilling.rootSystem H).weylGroup acting on
Module.Dual K H, which is the action the invariance of weight multiplicities
(TauCeti.formalCharacter_coeff_weylGroup_smul) is stated for; the orbit is Mathlib's
MulAction.orbit, counted with Nat.card.
References #
- N. Bourbaki, Groupes et algèbres de Lie, Ch. VIII, §7.3, where minuscule weights are introduced.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §13 and §21.2.
The weights of a highest weight module whose weights lie in one Weyl orbit are exactly that orbit: a linear form has a nonzero weight space in such a module precisely when it lies in the Weyl orbit of the highest weight.
A highest weight module whose weights lie in a single Weyl orbit has the dimension of that
orbit: a finite-dimensional module generated by a highest weight vector of weight lam, all of
whose weights are Weyl-conjugate to lam, has dimension the cardinality of the Weyl orbit of
lam. This is the dimension count that minusculeness buys, stated before TauCeti.IsMinuscule
names the condition.
The formal-character coefficient of a highest-weight module whose weights lie in one Weyl orbit is the indicator of that orbit: every Weyl translate of its highest weight occurs with multiplicity one, and the orbit-support hypothesis excludes every other weight.
A minuscule weight: a dominant integral weight mu every companion weight of which in
L(mu) is Weyl-conjugate to it, so that the weights of a nonzero L(mu) are exactly one Weyl
orbit.
The condition is on the weights of TauCeti.irreducibleQuotient, so it holds vacuously at a
weight where that module vanishes; see the module docstring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining condition on a minuscule weight, matching TauCeti.isDominantIntegral_iff beside
TauCeti.IsDominantIntegral.
A minuscule weight is dominant integral.
Every weight of a minuscule L(mu) is Weyl-conjugate to mu.
The character of a minuscule module is the orbit indicator: every Weyl translate of its highest weight occurs with multiplicity one, and minuscule-ness excludes every other weight.
The dimension of a minuscule module is the size of the Weyl orbit of its highest weight,
dim L(mu) = |W · mu|.
The zero weight is minuscule. Its module L(0) is the trivial one-dimensional module, so
its only weight is 0, which is its own Weyl orbit.