Finite-dimensionality of dominant irreducible highest weight modules

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically closed field of characteristic zero. An irreducible highest weight L-module is finite-dimensional exactly when its highest weight is dominant integral.

The forward implication is the rank-one argument of TauCeti.IsHighestWeightVector.isDominantIntegral. For the reverse implication, two earlier milestones supply the necessary finiteness:

• TauCeti.finite_setOf_genWeightSpace_ne_bot_of_isHighestWeightVector says that a dominant irreducible highest weight module has only finitely many nonzero weight spaces;
• TauCeti.finiteDimensional_genWeightSpace_of_isHighestWeightVector_of_lieSpan_eq_top says that each of those weight spaces is finite-dimensional.

The weight-cone decomposition of a highest weight module says that these spaces span the whole module. Their finite supremum is therefore finitely generated, which proves the result without assuming finite-dimensionality of the ambient module at any intermediate step.

The criterion is then read at the named carrier TauCeti.irreducibleQuotient b lam, that is L(lam), in the two directions a consumer wants: L(lam) is finite-dimensional whenever lam is dominant integral, with no side condition on the Verma module M(lam) because L(lam) is the zero module when M(lam) vanishes; and conversely every finite-dimensional irreducible module is a copy of L(lam) for a dominant integral lam, which is the classification of the finite-dimensional irreducibles.

Main results

• TauCeti.finiteDimensional_of_isHighestWeightVector_of_isDominantIntegral: the difficult implication, from dominance to finite-dimensionality.
• TauCeti.finiteDimensional_iff_isDominantIntegral_of_isHighestWeightVector: the complete finite-dimensionality criterion for an irreducible highest weight module.
• TauCeti.finiteDimensional_irreducibleQuotient_of_isDominantIntegral: L(lam) is finite-dimensional at a dominant integral weight, unconditionally.
• TauCeti.finrank_irreducibleQuotient_zero: L(0) is one-dimensional, the dimension of the named carrier at the zero weight.
• TauCeti.exists_isDominantIntegral_nonempty_lieModuleEquiv_irreducibleQuotient: a finite-dimensional irreducible module is a copy of L(lam) for a dominant integral lam.

References

This closes the finite-dimensionality milestone of Layer 4 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md. It is the last assembly step in the proof that the irreducible highest weight module L(lam) is finite-dimensional precisely for dominant integral lam.

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §21.2.

theorem TauCeti.finiteDimensional_of_isHighestWeightVector_of_isDominantIntegral {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.IsIrreducible K L M] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) (hlam : IsDominantIntegral b lam) : FiniteDimensional K M

An irreducible highest weight module of dominant integral highest weight is finite-dimensional. Its nonzero weight spaces form a finite family, every member of that family is finite-dimensional, and the family spans the module.

theorem TauCeti.finiteDimensional_iff_isDominantIntegral_of_isHighestWeightVector {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.IsIrreducible K L M] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) : FiniteDimensional K M ↔ IsDominantIntegral b lam

Finite-dimensionality criterion for an irreducible highest weight module. Such a module is finite-dimensional if and only if its highest weight is dominant integral.

The criterion at the named carrier L(lam)

theorem TauCeti.finiteDimensional_irreducibleQuotient_of_isDominantIntegral {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} (hlam : IsDominantIntegral b lam) : FiniteDimensional K (irreducibleQuotient b lam)

L(lam) is finite-dimensional at a dominant integral weight. L(lam) is an irreducible highest weight module of dominant integral weight, and TauCeti.finiteDimensional_of_isHighestWeightVector_of_isDominantIntegral applies.

@[simp]

theorem TauCeti.finrank_irreducibleQuotient_zero {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (b : (LieAlgebra.IsKilling.rootSystem H).Base) : Module.finrank K (irreducibleQuotient b 0) = 1

L(0) is one-dimensional. The zero weight is dominant integral, and L(0) is a highest weight module of weight 0; such a module is trivial (TauCeti.isTrivial_of_isHighestWeightVector_weight_zero_of_lieSpan_eq_top), and a trivial module generated by one vector is the line through it.

theorem TauCeti.exists_isDominantIntegral_nonempty_lieModuleEquiv_irreducibleQuotient {K : Type u} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.IsIrreducible K L M] (b : (LieAlgebra.IsKilling.rootSystem H).Base) [FiniteDimensional K M] : ∃ (lam : Module.Dual K ↥H), IsDominantIntegral b lam ∧ Nonempty (M ≃ₗ⁅K,L⁆ irreducibleQuotient b lam)

A finite-dimensional irreducible module is a copy of L(lam), for a dominant integral weight lam. It carries a highest weight vector of a dominant integral weight (TauCeti.exists_isHighestWeightVector_and_isDominantIntegral_of_irreducible), and two irreducible modules with highest weight vectors of the same weight are equivalent.