The maximal submodule of a highest weight module, and its irreducible quotient #
A highest weight module has a greatest proper submodule, namely the sum of all the submodules
that meet its top weight space trivially, and therefore a unique irreducible quotient. This file
builds that submodule, Ado.maximalSubmodule, and proves both statements.
The argument #
The lam-weight space of a highest weight module is the line K ∙ v spanned by the generator
(Ado.genWeightSpace_eq_span_singleton_of_isHighestWeightVector_of_lieSpan_eq_top), so a
submodule meets it trivially exactly when it misses v, which in turn is exactly when it is
proper. What is not formal is that the sum of such submodules still misses v, and that is the
content of the file: a Lie submodule missing v is contained in the span of the weight spaces at
the weights other than lam, a submodule which misses v for the trivial reason that the weight
spaces are independent.
That containment is the statement that a submodule is compatible with the weight grading, in the
one degree where it is needed. Since a highest weight module is spanned by the weight spaces below
lam and its lam-weight space is K ∙ v, an element of a submodule N can be written as
c • v + m with m a sum of finitely many vectors of weights other than lam, and the claim is
that already c • v ∈ N. One weight of m is removed at a time. If m has a component m₀ of
weight chi ≠ lam, pick x : H with chi x ≠ lam x and a k with (x - chi x)^k killing m₀;
applying that operator to c • v + m leaves an element of N of the same shape, with m₀ gone
and c multiplied by (lam x - chi x)^k ≠ 0, since v is an honest eigenvector of x. Both
N and the span of the remaining weight spaces are stable under the operator, so the induction
goes through.
Main definitions #
Ado.maximalSubmodule H M lam: the sum of all Lie submodules ofMmeeting thelam-weight space trivially.
Main results #
Ado.genWeightSpace_sup_genWeightSpaceSpan_eq_top_of_isHighestWeightVector_of_lieSpan_eq_top: a highest weight module is the sum of itslam-weight space and the span of its other weight spaces, andAdo.disjoint_genWeightSpace_genWeightSpaceSpan_nesays the two meet trivially.Ado.le_genWeightSpaceSpan_ne_of_notMem_of_isHighestWeightVector_of_lieSpan_eq_top: a Lie submodule of a highest weight module which misses the generator misses the whole top weight space, being contained in the span of the other weight spaces.Ado.notMem_iff_ne_top_of_isHighestWeightVector_of_lieSpan_eq_topandAdo.disjoint_genWeightSpace_iff_notMem_of_isHighestWeightVector_of_lieSpan_eq_top: for a Lie submodule of a highest weight module, being proper, missing the generator and meeting the top weight space trivially are the same condition.Ado.notMem_maximalSubmodule_of_isHighestWeightVector_of_lieSpan_eq_topandAdo.isGreatest_maximalSubmodule_of_isHighestWeightVector_of_lieSpan_eq_top: the maximal submodule of a highest weight module is its greatest proper submodule, so byAdo.eq_top_of_maximalSubmodule_lt_of_isHighestWeightVector_of_lieSpan_eq_topanything strictly above it is everything.Ado.isCoatom_maximalSubmodule_of_isHighestWeightVector_of_lieSpan_eq_top: it is a coatom of the lattice of Lie submodules, so byAdo.isIrreducible_quotient_iff_isCoatomthe quotient by it is irreducible.Ado.isIrreducible_quotient_maximalSubmodule_of_isHighestWeightVector_of_lieSpan_eq_top: the quotient by it is irreducible, andAdo.isHighestWeightVector_mk_of_isHighestWeightVector_of_lieSpan_eq_toptogether withAdo.lieSpan_mk_eq_top_of_lieSpan_eq_topexhibit that quotient as again a highest weight module of weightlam, generated by the image of the generator.
Implementation notes #
Ado.maximalSubmodule is defined for an arbitrary module, as the sum of the submodules meeting
the lam-weight space trivially; it is only for a highest weight module of weight lam that it is
the greatest proper submodule, and the results asserting that carry the hypotheses. Defining it
intrinsically, rather than as the sum of the submodules missing a chosen generator, is what makes
it manifestly independent of the choice of generator.
Nothing here needs the module to be finite-dimensional: the Verma module of Layer 3 of the roadmap,
whose irreducible quotient is L(lam), is infinite-dimensional, and it is the module this file
exists to be applied to. In particular the weight spaces are the generalized ones throughout, and
the one place where an honest eigenvector is needed is the generator itself, which is one by the
definition of Ado.IsHighestWeightVector.
References #
This is the "irreducible quotient L(λ)" item of Layer 3 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md: "M(λ) has a unique maximal
submodule (the sum of all submodules meeting the λ-weight space trivially), hence a unique
irreducible quotient L(λ)". Since the Verma module M(λ) itself is not yet built, the statements
are proved for an arbitrary highest weight module, which is how L(λ) will consume them.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §20.3.
Powers of a shifted Cartan operator #
The weight spaces other than the top one #
The top weight space is disjoint from the span of the other weight spaces, the weight spaces of a module being independent.
A highest weight module is the sum of its top weight space and the span of its other weight
spaces. Every weight space of a highest weight module sits at a weight lam - nu, which is
either lam itself or one of the others.
Submodules missing the generator #
A Lie submodule of a highest weight module which misses the generator misses the whole top weight space: it is contained in the span of the weight spaces at the other weights.
This is the weight-compatibility of submodules, in the degree where it is needed: the lam-part of
an element of a submodule already lies in that submodule, so a submodule with no lam-part at all
is supported on the other weights.
The maximal submodule #
The sum of all the Lie submodules meeting the lam-weight space trivially. For a highest
weight module of weight lam this is the greatest proper submodule
(Ado.isGreatest_maximalSubmodule_of_isHighestWeightVector_of_lieSpan_eq_top), and the
quotient by it is the unique irreducible quotient; for an arbitrary module it is only the sum
named.
Equations
- Ado.maximalSubmodule H M lam = sSup {N : LieSubmodule K L M | Disjoint ↑N ↑(LieModule.genWeightSpace M ⇑lam)}
Instances For
The supremum description underlying maximalSubmodule.
A Lie submodule meeting the lam-weight space trivially lies in the maximal submodule.
The maximal submodule lies in P exactly when every submodule meeting the lam-weight space
trivially lies in P.
In a highest weight module, meeting the top weight space trivially is missing the generator, the top weight space being the line the generator spans.
In a highest weight module, a Lie submodule is proper exactly when it misses the generator.
The maximal submodule of a highest weight module misses the generator: each of the
submodules summed to build it is supported on the weights other than lam, hence so is the sum,
and the generator is not.
The maximal submodule of a highest weight module is its greatest proper submodule.
A Lie submodule of a highest weight module lies in the maximal submodule exactly when it is proper.
A Lie submodule of a highest weight module lies in the maximal submodule exactly when it misses the highest weight generator.
A Lie submodule of a highest weight module lies in the maximal submodule exactly when it meets the highest weight space trivially.
A Lie submodule of a highest weight module strictly containing the maximal submodule is everything.
The irreducible quotient #
The image of the generator generates the quotient.
The image of the generator in the quotient by the maximal submodule is again a highest weight
vector of weight lam. It is nonzero because the maximal submodule misses the generator, and the
two equations defining a highest weight vector pass to the quotient.
The maximal submodule of a highest weight module is a coatom of its lattice of Lie submodules: it is proper because it misses the generator, and anything strictly above it is everything.
The quotient of a highest weight module by its maximal submodule is irreducible, the maximal submodule being a coatom.
The kernel of every surjection from a highest weight module to a nontrivial irreducible module is its maximal submodule.
The canonical irreducible quotient of a highest weight module is equivalent to every nontrivial irreducible quotient.
Equations
- One or more equations did not get rendered due to their size.