The copy of L(lam) generated by a highest weight vector, and the single-weight criterion

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically closed field of characteristic zero. This file proves the two statements that turn Weyl's complete reducibility theorem into a usable decomposition tool.

• A highest weight vector of a finite-dimensional module generates an irreducible submodule, necessarily a copy of the irreducible highest weight module L(lam) (TauCeti.isIrreducible_lieSpan_of_isHighestWeightVector). Finite-dimensionality is essential: in general a highest weight vector generates only a quotient of a Verma module.
• The single-weight criterion: if every highest weight vector of a finite-dimensional module has the same weight lam, the module is L(lam)-isotypic (TauCeti.isotypicComponent_eq_top_of_forall_isHighestWeightVector). This is what a decomposition argument consumes verbatim: exhibit the highest weight vectors, check that they share one weight, conclude that the module is a direct sum of copies of a single irreducible.

Each statement is proved twice over. The general form takes the copy of L(lam) as a parameter: an irreducible module carrying a highest weight vector of weight lam is unique up to equivalence (TauCeti.nonempty_lieModuleEquiv_iff_eq_of_isHighestWeightVector), so an equivalence with an arbitrary such module says exactly "a copy of L(lam)". The form the roadmap pins fixes the carrier to be TauCeti.irreducibleQuotient b lam, with nothing quantified over: that quotient is irreducible and carries a highest weight vector of weight lam (TauCeti.isHighestWeightVector_irreducibleQuotientGenerator).

The argument

Everything rests on one observation about a highest weight module M, that is a module generated by a highest weight vector v of weight lam. If P and P' are complementary Lie submodules of M, then v lies in one of them. Indeed, write v = p + p' along the decomposition. For x in the Cartan subalgebra the vector ⁅x, p⁆ - lam x • p lies in P and is the negative of ⁅x, p'⁆ - lam x • p', which lies in P'; the two submodules being disjoint, both vanish. The same argument at a positive root vector shows that p and p' are each either zero or a highest weight vector of weight lam, hence a nonzero multiple of v (TauCeti.exists_eq_smul_of_isHighestWeightVector_of_lieSpan_eq_top). They cannot both be nonzero, since then v would lie in P ⊓ P' = ⊥.

Weyl's theorem (TauCeti.exists_isCompl_of_isKilling) supplies a complement for every Lie submodule of a finite-dimensional module, so this dichotomy says exactly that a finite-dimensional highest weight module is irreducible. The statement about the submodule generated by a highest weight vector of an arbitrary finite-dimensional module is that statement applied to the submodule, which is again a highest weight module by TauCeti.lieSpan_singleton_eq_top_of_lieSpan_eq. The rank-one precedent is TauCeti.isIrreducible_lieSpan_singleton, which says the same for a primitive vector of an sl₂ triple spanning L; that one is proved by the elementary weight-string argument of Layer 0, since Weyl's theorem is not yet available where it is used.

For the single-weight criterion, every irreducible Lie submodule of a finite-dimensional module carries a highest weight vector (TauCeti.exists_isHighestWeightVector), whose weight is lam by hypothesis; two irreducible modules with highest weight vectors of the same weight are equivalent, so the module is isotypic of that type. Passing from isotypy to the isotypic component being everything is Mathlib's isotypicComponent_eq_top_iff read through the enveloping-algebra dictionary, LieModule.isotypicComponent_eq_top_iff_of_ι_smul.

Main results

• TauCeti.isIrreducible_of_isHighestWeightVector_of_lieSpan_eq_top: a finite-dimensional highest weight module is irreducible.
• TauCeti.isIrreducible_lieSpan_of_isHighestWeightVector and TauCeti.nonempty_lieModuleEquiv_lieSpan_of_isHighestWeightVector: a highest weight vector of a finite-dimensional module generates a copy of L(lam), and TauCeti.finrank_le_of_isHighestWeightVector reads off dim L(lam) ≤ dim M.
• TauCeti.lieSpan_equiv_irreducibleQuotient_of_isHighestWeightVector and TauCeti.finrank_irreducibleQuotient_le_of_isHighestWeightVector: the same two statements at the fixed carrier L(lam).
• TauCeti.isIsotypicOfType_of_forall_isHighestWeightVector and TauCeti.isotypicComponent_eq_top_of_isHighestWeightVector_of_forall_isHighestWeightVector: the single-weight isotypic criterion, with TauCeti.isotypicComponent_eq_top_of_forall_isHighestWeightVector its form at the fixed carrier, which reads the conclusion off the weight hypothesis alone.

References

This supplies the milestone "a highest weight vector generates a copy of L(λ), and the single-weight criterion" of the decomposition toolkit in Layer 6 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

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

The submodule generated by a highest weight vector

A finite-dimensional highest weight module is irreducible

theorem TauCeti.isIrreducible_of_isHighestWeightVector_of_lieSpan_eq_top {K : Type u} {L : Type v} [Field K] [CharZero 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] [IsAlgClosed K] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} [FiniteDimensional K M] (hv : IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) : LieModule.IsIrreducible K L M

A finite-dimensional highest weight module is irreducible. Every Lie submodule has a complement by Weyl's theorem, and the generator lies in one of the two halves; the half containing it is everything.

The copy of L(lam) generated by a highest weight vector

theorem TauCeti.isIrreducible_lieSpan_of_isHighestWeightVector {K : Type u} {L : Type v} [Field K] [CharZero 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] [IsAlgClosed K] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} [FiniteDimensional K M] (hv : IsHighestWeightVector b lam v) : LieModule.IsIrreducible K L ↥(LieSubmodule.lieSpan K L {v})

A highest weight vector of a finite-dimensional module generates an irreducible submodule. The submodule it generates is a highest weight module, and a finite-dimensional highest weight module is irreducible.

theorem TauCeti.nonempty_lieModuleEquiv_lieSpan_of_isHighestWeightVector {K : Type u} {L : Type v} [Field K] [CharZero 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] {N : Type w₁} [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [IsAlgClosed K] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} [FiniteDimensional K M] [LieModule.IsIrreducible K L N] {w : N} (hv : IsHighestWeightVector b lam v) (hw : IsHighestWeightVector b lam w) : Nonempty (↥(LieSubmodule.lieSpan K L {v}) ≃ₗ⁅K,L⁆ N)

A highest weight vector generates a copy of L(lam). In a finite-dimensional module the Lie submodule generated by a highest weight vector of weight lam is equivalent to every irreducible module carrying a highest weight vector of that weight, so it is a copy of L(lam).

Finite-dimensionality is essential: in general a highest weight vector generates a quotient of the Verma module of its weight, not necessarily an irreducible one.

theorem TauCeti.finrank_le_of_isHighestWeightVector {K : Type u} {L : Type v} [Field K] [CharZero 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] {N : Type w₁} [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [IsAlgClosed K] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} [FiniteDimensional K M] [LieModule.IsIrreducible K L N] {w : N} (hv : IsHighestWeightVector b lam v) (hw : IsHighestWeightVector b lam w) : Module.finrank K N ≤ Module.finrank K M

dim L(lam) ≤ dim M whenever M has a highest weight vector of weight lam. The copy of L(lam) generated by that vector is a subspace of M.

The same statements at the named carrier L(lam)

TauCeti.irreducibleQuotient b lam is L(lam), the quotient of the Verma module M(lam) by its maximal submodule; it is irreducible and carries a highest weight vector of weight lam. So each statement above is recorded again at that one fixed carrier, with nothing quantified over.

theorem TauCeti.lieSpan_equiv_irreducibleQuotient_of_isHighestWeightVector {K : Type u} {L : Type v} [Field K] [CharZero 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] [IsAlgClosed K] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} [FiniteDimensional K M] (hv : IsHighestWeightVector b lam v) : Nonempty (↥(LieSubmodule.lieSpan K L {v}) ≃ₗ⁅K,L⁆ irreducibleQuotient b lam)

A highest weight vector generates a copy of L(lam). In a finite-dimensional module the Lie submodule generated by a highest weight vector of weight lam is equivalent to L(lam).

theorem TauCeti.finrank_irreducibleQuotient_le_of_isHighestWeightVector {K : Type u} {L : Type v} [Field K] [CharZero 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] [IsAlgClosed K] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} [FiniteDimensional K M] (hv : IsHighestWeightVector b lam v) : Module.finrank K (irreducibleQuotient b lam) ≤ Module.finrank K M

dim L(lam) ≤ dim M, the copy of L(lam) generated by a highest weight vector of weight lam being a subspace of M.

The single-weight isotypic criterion

theorem TauCeti.isIsotypicOfType_of_forall_isHighestWeightVector {K : Type u} {L : Type v} [Field K] [CharZero 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] {N : Type w₁} [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [IsAlgClosed K] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} [FiniteDimensional K M] [LieModule.IsIrreducible K L N] {w : N} (hw : IsHighestWeightVector b lam w) (h : ∀ (nu : Module.Dual K ↥H) (u : M), IsHighestWeightVector b nu u → nu = lam) : LieModule.IsIsotypicOfType K L M N

The single-weight isotypic criterion. If every highest weight vector of a finite-dimensional module M has weight lam, then every irreducible Lie submodule of M is a copy of L(lam): each such submodule carries a highest weight vector, whose weight is lam by hypothesis, and irreducible modules with highest weight vectors of the same weight agree.

theorem TauCeti.isotypicComponent_eq_top_of_isHighestWeightVector_of_forall_isHighestWeightVector {K : Type u} {L : Type v} [Field K] [CharZero 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] {N : Type w₁} [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [IsAlgClosed K] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} [FiniteDimensional K M] [LieModule.IsIrreducible K L N] {w : N} (hw : IsHighestWeightVector b lam w) (h : ∀ (nu : Module.Dual K ↥H) (u : M), IsHighestWeightVector b nu u → nu = lam) : LieModule.isotypicComponent K L M N = ⊤

The single-weight isotypic criterion, as a statement about the isotypic component. If every highest weight vector of a finite-dimensional module M has weight lam, then the L(lam)-isotypic component of M is all of M, so M is a direct sum of copies of L(lam). Here L(lam) is presented as an arbitrary irreducible module carrying a highest weight vector of weight lam; TauCeti.isotypicComponent_eq_top_of_forall_isHighestWeightVector is the same statement at the fixed carrier.

theorem TauCeti.isotypicComponent_eq_top_of_forall_isHighestWeightVector {K : Type u} {L : Type v} [Field K] [CharZero 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] [IsAlgClosed K] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} [FiniteDimensional K M] (h : ∀ (nu : Module.Dual K ↥H) (u : M), IsHighestWeightVector b nu u → nu = lam) : LieModule.isotypicComponent K L M (irreducibleQuotient b lam) = ⊤

The single-weight isotypic criterion at the fixed carrier L(lam), which is the criterion read off the weight hypothesis alone: a finite-dimensional module all of whose highest weight vectors have weight lam is a direct sum of copies of L(lam).