Irreducible highest weight modules are classified by their weight

An irreducible highest weight module of weight lam is an irreducible L-module carrying a highest weight vector of weight lam; it is automatically generated by that vector, an irreducible module being generated by any of its nonzero elements (TauCeti.lieSpan_singleton_eq_top_of_ne_zero). This file proves that such a module is determined by lam up to isomorphism, and determines lam in turn:

TauCeti.nonempty_lieModuleEquiv_iff_eq_of_isHighestWeightVector, two irreducible modules carrying highest weight vectors of weights lam and mu are isomorphic if and only if lam = mu.

Neither module is assumed finite-dimensional, so this is the classification of all irreducible highest weight modules, and it is what makes the irreducible quotient L(lam) of a highest weight module well defined: any two constructions of it agree.

The argument

Uniqueness of the weight is a transport: an isomorphism carries a highest weight vector to a highest weight vector of the same weight (TauCeti.IsHighestWeightVector.congr), and a module is a highest weight module for at most one weight (TauCeti.eq_of_isHighestWeightVector_of_lieSpan_eq_top).

Uniqueness of the module is the classical diagonal argument, and it is the reason this file needs the product of two Lie modules of TauCeti/Algebra/Lie/Prod.lean. Given highest weight vectors v : M and w : N of the same weight lam, the vector (v, w) is a highest weight vector of M × N, and the submodule D it generates is the graph of the isomorphism sought. Two facts identify it as such.

• D is a proper submodule of M × N. Were it everything, M × N would be a highest weight module of weight lam, so its lam-weight space would be the line K ∙ (v, w) (TauCeti.genWeightSpace_eq_span_singleton_of_isHighestWeightVector_of_lieSpan_eq_top); but (v, 0) is another highest weight vector of weight lam, and it is not a multiple of (v, w).
• Consequently D meets neither factor. If it met N, then by irreducibility it would contain (0, w), hence also (v, w) - (0, w) = (v, 0), hence — again by irreducibility — both factors whole, so D = ⊤; the same argument runs with the factors exchanged.

The two projections restricted to D are therefore injective, and they are surjective because their images are nonzero submodules of irreducible modules. So M ≃ D ≃ N.

Main results

• TauCeti.lieModuleEquivOfIsHighestWeightVector: the equivalence between two irreducible modules of the same highest weight, chosen to carry one specified highest weight vector to the other.
• TauCeti.nonempty_lieModuleEquiv_of_isHighestWeightVector: two irreducible modules carrying highest weight vectors of the same weight are isomorphic.
• TauCeti.nonempty_lieModuleEquiv_iff_eq_of_isHighestWeightVector: and conversely, so isomorphism of irreducible highest weight modules is exactly equality of their weights.
• TauCeti.IsHighestWeightVector.unique_of_isIrreducible: an irreducible module carries highest weight vectors of at most one weight.

References

This file supplies the classification half of the "irreducible quotient L(λ)" item of Layer 3 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md: "L(λ) is the unique irreducible highest weight module of weight λ, and L(λ) ≅ L(μ) iff λ = μ. This is the classification of all irreducible highest weight modules, finite-dimensional or not." The target signature irreducibleQuotient_nonempty_equiv_iff of the accompanying Suggested.lean is the instance of TauCeti.nonempty_lieModuleEquiv_iff_eq_of_isHighestWeightVector at the irreducible quotients of two Verma modules.

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

The diagonal highest weight vector

Everything below compares two modules M and N through the submodule of M × N generated by the diagonal vector (v, w).

The diagonal submodule meets neither factor

The diagonal submodule is the graph of an isomorphism

The classification

noncomputable def TauCeti.lieModuleEquivOfIsHighestWeightVector {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] [LieModule.IsTriangularizable K (↥H) L] {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} {w : N} [LieModule.IsIrreducible K L M] [LieModule.IsIrreducible K L N] (hv : IsHighestWeightVector b lam v) (hw : IsHighestWeightVector b lam w) : M ≃ₗ⁅K,L⁆ N

The equivalence between two irreducible modules of the same highest weight. It is obtained by identifying both modules with the diagonal submodule of their product.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.lieModuleEquivOfIsHighestWeightVector_apply {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] [LieModule.IsTriangularizable K (↥H) L] {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} {w : N} [LieModule.IsIrreducible K L M] [LieModule.IsIrreducible K L N] (hv : IsHighestWeightVector b lam v) (hw : IsHighestWeightVector b lam w) : (lieModuleEquivOfIsHighestWeightVector hv hw) v = w

theorem TauCeti.nonempty_lieModuleEquiv_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] [LieModule.IsTriangularizable K (↥H) L] {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} {w : N} [LieModule.IsIrreducible K L M] [LieModule.IsIrreducible K L N] (hv : IsHighestWeightVector b lam v) (hw : IsHighestWeightVector b lam w) : Nonempty (M ≃ₗ⁅K,L⁆ N)

Two irreducible Lie modules carrying highest weight vectors of the same weight are isomorphic. Both are isomorphic to the submodule of their product generated by the diagonal vector, which is the graph of the isomorphism between them.

theorem TauCeti.nonempty_lieModuleEquiv_iff_eq_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] [LieModule.IsTriangularizable K (↥H) L] {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam mu : Module.Dual K ↥H} {v : M} {w : N} [LieModule.IsIrreducible K L M] [LieModule.IsIrreducible K L N] (hv : IsHighestWeightVector b lam v) (hw : IsHighestWeightVector b mu w) : Nonempty (M ≃ₗ⁅K,L⁆ N) ↔ lam = mu

The classification of the irreducible highest weight modules. Two irreducible modules carrying highest weight vectors of weights lam and mu are isomorphic exactly when lam = mu; neither module is assumed finite-dimensional.