The highest weight of a Weyl module #
The Weyl module of a μ-tableau t is the image of the Young symmetrizer c_t acting on the
tensor power (kⁿ)^{⊗|μ|} of the standard representation of GL n k. The tensor power is the
internal direct sum of its weight spaces, which are the coordinate subspaces spanned by the
monomial basis vectors of a given content, and c_t preserves each of them, so the Weyl module
inherits a weight decomposition. This file proves that decomposition, bounds the surviving weights
from above, and shows that the shape weight attains the bound.
The answer is the dominance bound: writing r for the row filling of t
(TauCeti.YoungTableau.rowFilling, the filling of the labels by their row indices), every weight
l of the Weyl module satisfies
∑_{j < m} l j ≤ ∑_{j < m} μ.rowLen j
for every bound m. The same bound holds for the weakly decreasing rearrangement
TauCeti.dominantWeightOf l, and the right-hand side is the weight TauCeti.weightOfShape n μ
of the shape itself. Over a field that is a ℚ-algebra, when μ.colLen 0 ≤ n, this weight occurs
and is the highest weight of the Weyl module in the dominance order, carried by the image of the
monomial basis vector e_r.
When n < μ.colLen 0, the Weyl module is zero (TauCeti.YoungTableau.weylModule_eq_bot).
Both halves come from the vanishing criterion of
TauCeti.RepresentationTheory.ClassicalGroups.WeylModule.Basic, read one monomial basis vector at
a time. The symmetrizer annihilates e_p as soon as the filling p gives two labels of one
column the same basis index; so a filling whose basis vector survives is injective on columns, and
such a filling takes small values no more often than the row index does
(TauCeti.YoungTableau.card_filter_lt_le_card_filter_rowIndex_lt), which is the displayed
inequality once both counts are read as partial sums of contents. Conversely, when
μ.colLen 0 ≤ n, e_r itself has content the row lengths of μ and is not annihilated,
so the bound is attained.
The dominance bound is proved over a field that is a ℚ-algebra: it has characteristic zero,
so it is infinite and its weight characters separate weights, which is the hypothesis under which
the weight spaces of the tensor power are its coordinate subspaces. The occurrence of the shape
weight only requires a nontrivial commutative ℚ-algebra.
Main results #
TauCeti.YoungTableau.weightOfMultiset_ofFn_rowFilling: the content of the row filling is the weight of the shape.TauCeti.YoungTableau.weightSpace_weylRep_eq_bot_of_card_filter_lt: a weight whose partial sums exceed those of the row lengths does not occur in the Weyl module, withTauCeti.YoungTableau.weylModule_toSubmodule_inf_weightSpace_eq_botits form inside the tensor power.TauCeti.YoungTableau.sum_le_sum_weightOfShape_of_weightSpace_weylRep_ne_bot: the partial sums of each weight are bounded by those of the shape, andTauCeti.YoungTableau.sum_dominantWeightOf_le_sum_weightOfShape_of_weightSpace_weylRep_ne_bot: the same bound for its dominant representative.TauCeti.YoungTableau.nonneg_and_sum_eq_of_weightSpace_weylRep_ne_bot: the weights are nonnegative of total degree|μ|, so the bounds give the dominance comparison.TauCeti.YoungTableau.weightSpace_weylRep_weightOfShape_ne_bot: whenμ.colLen 0 ≤ n, the weight of the shape occurs in the Weyl module, so over a field it is the highest weight.TauCeti.isInternal_weightSpace_weylRepOfShape: the inherited weight decomposition of the shape-indexed Weyl module.TauCeti.weightSpace_weylRepOfShape_eq_bot_iff: transfers vanishing between the shape-indexed Weyl module and its row-superstandard tableau.TauCeti.sum_le_sum_weightOfShape_of_weightSpace_weylRepOfShape_ne_bot,TauCeti.sum_dominantWeightOf_le_sum_weightOfShape_of_weightSpace_weylRepOfShape_ne_bot, andTauCeti.nonneg_and_sum_eq_of_weightSpace_weylRepOfShape_ne_bot: the bounds and total degree for the shape-indexed Weyl module, hence forTauCeti.schurFunctor.TauCeti.weightSpace_weylRepOfShape_weightOfShape_ne_bot: occurrence in the shape-indexed Weyl module whenμ.colLen 0 ≤ n.
Implementation notes #
The weight spaces of the Weyl module are spelled weightSpace (W := _) (weylRep k n t) l, with the
carrier supplied. TauCeti.weightSpace asks for an additive group, while a subrepresentation
carries the additive monoid structure of a submodule, and the elaborator will not invert
AddCommGroup.toAddCommMonoid while the carrier is still a metavariable; naming the carrier lets
instance search produce the group structure first.
References #
- W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lectures 6 and 15.
The content of the row filling #
The content of the row filling is the weight of the shape: the number of labels of a
μ-tableau lying in row j is the length of that row.
The dominance bound #
The Weyl module meets a weight space trivially when its partial sum ∑_{j < m} l j
exceeds the number of labels in the first m rows of t. The tensor power is spanned by its
weight spaces and the symmetrizer preserves each of them, so the image of the symmetrizer lies in
the sum of the weight spaces away from l, which is disjoint from the weight space at l.
A weight whose partial sums exceed those of the row lengths does not occur in the Weyl module.
The weights of the Weyl module are dominated by the weight of its shape: every weight l
of the Weyl module satisfies the dominance inequalities
∑_{j < m} l j ≤ ∑_{j < m} μ.rowLen j,
the right-hand side being the corresponding partial sum of TauCeti.weightOfShape n μ.
The dominant representative of every Weyl-module weight is dominated by the shape weight: permuting the coordinates preserves occurrence, so the partial-sum bound applies after sorting.
The weights of the Weyl module are nonnegative and of total degree |μ|: a weight of a
subrepresentation is a weight of the ambient tensor power, whose weights are the exponent vectors
of the degree-|μ| monomials in n variables. Together with the dominance bound this is the
statement that every weight of the Weyl module is dominated by TauCeti.weightOfShape n μ in the
dominance order on the weights of degree |μ|.
The highest weight #
When μ.colLen 0 ≤ n, the weight of the shape occurs in the Weyl module: the image under
the symmetrizer of the monomial basis vector of the row filling is a nonzero vector of that weight.
Over a field, together with
TauCeti.YoungTableau.sum_le_sum_weightOfShape_of_weightSpace_weylRep_ne_bot, this says that
TauCeti.weightOfShape n μ is the highest weight, in the dominance order, of the Weyl module of
any μ-tableau whose shape satisfies μ.colLen 0 ≤ n.
The Weyl module of a shape #
Over a field that is a ℚ-algebra, the integer weight spaces of a Weyl module form an
internal direct sum. The rational algebra structure is required to define the Weyl module.
A shape-indexed Weyl weight space vanishes exactly when the corresponding weight space for its row-superstandard tableau vanishes.
The weights of the Weyl module of a shape are dominated by the weight of that shape: the
shape-indexed form of TauCeti.YoungTableau.sum_le_sum_weightOfShape_of_weightSpace_weylRep_ne_bot
at the row-superstandard tableau.
The dominant representatives of shape-indexed Weyl-module weights are dominated by the shape weight, by the bound for the row-superstandard tableau.
The weights of the shape-indexed Weyl module are nonnegative of total degree |μ|,
since it is a subrepresentation of that tensor power of the standard representation.
When μ.colLen 0 ≤ n, the weight of a shape occurs in the Weyl module of that shape.
Over a field it is therefore the highest weight of TauCeti.weylRepOfShape — and hence, over ℂ,
of TauCeti.schurFunctor — in the dominance order.