Documentation

TauCeti.Algebra.Lie.HighestWeight.Dual

Self-duality of a finite-dimensional irreducible highest weight module #

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically closed field of characteristic zero, let H be a Cartan subalgebra and b a base of its root system, and let M be a finite-dimensional irreducible L-module with a highest weight vector of weight lam. This file identifies the highest weight of the dual module M* and reads off the self-duality criterion:

M carries a nonzero invariant bilinear form ↔ M ≃ M* ↔ -(w₀ • lam) = lam,

with w₀ the longest element of the Weyl group.

The highest weight of the dual #

TauCeti/Algebra/Lie/HighestWeight/LowestWeight.lean identifies w₀ • lam as the lowest weight of M: nothing lies below it, so subtracting a positive root from it leaves the weight support (TauCeti.genWeightSpace_longestElement_smul_sub_root_eq_bot).

A functional that vanishes on every weight space except the lowest one is then a highest weight vector of M* of weight -(w₀ • lam). Its weight is read off the decomposition of M into weight spaces, and a positive root space kills it because raising a weight into w₀ • lam would have to start below w₀ • lam, where M is zero.

The criterion #

M* is irreducible (TauCeti.LieModule.isIrreducible_dual), so the classification of irreducible highest weight modules by their weight turns the existence of an equivalence M ≃ M* into the equation -(w₀ • lam) = lam; and a nonzero invariant bilinear form on M is exactly a nonzero morphism M → M*, which by Schur's lemma is an equivalence.

The criterion at L(lam) #

At the named carrier L(lam) the criterion needs only dominance of lam: L(lam) is irreducible with a highest weight vector of weight lam, because the Verma module M(lam) is nonzero (TauCeti.vermaGenerator_ne_zero), and dominance makes it finite-dimensional.

Main results #

References #

The highest weight vector of the dual #

source
theorem TauCeti.exists_isHighestWeightVector_dual {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} [IsAlgClosed K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {v : M} [LieModule.IsIrreducible K L M] [FiniteDimensional K M] (hv : IsHighestWeightVector b lam v) :
∃ (f : Module.Dual K M), IsHighestWeightVector b (-(longestElement (LieAlgebra.IsKilling.rootSystem H) b • lam)) f

The dual of an irreducible highest weight module has a highest weight vector of weight -(w₀ • lam). A functional vanishing on every weight space but the lowest one has weight -(w₀ • lam) because the weight spaces are honest eigenspaces, and a positive root space kills it because it raises the lowest weight space out of the weight support.

The self-duality criterion #

source
theorem TauCeti.nonempty_lieModuleEquiv_dual_iff {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} [IsAlgClosed K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {v : M} [LieModule.IsIrreducible K L M] [FiniteDimensional K M] (hv : IsHighestWeightVector b lam v) :
Nonempty (M ≃ₗ⁅K,L⁆ Module.Dual K M) ↔ -(longestElement (LieAlgebra.IsKilling.rootSystem H) b • lam) = lam

A finite-dimensional irreducible module is self-dual exactly when -(w₀ • lam) = lam. The dual is irreducible with highest weight -(w₀ • lam), and irreducible highest weight modules are classified by their weight.

source
theorem TauCeti.exists_ne_zero_lieInvariant_iff_neg_longestElement_smul_eq {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} [IsAlgClosed K] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {v : M} [LieModule.IsIrreducible K L M] [FiniteDimensional K M] (hv : IsHighestWeightVector b lam v) :
(∃ (Φ : LinearMap.BilinForm K M), Φ ≠ 0 ∧ LinearMap.BilinForm.lieInvariant L Φ) ↔ -(longestElement (LieAlgebra.IsKilling.rootSystem H) b • lam) = lam

The self-duality criterion in its invariant-form shape. A finite-dimensional irreducible module with highest weight lam carries a nonzero invariant bilinear form exactly when -(w₀ • lam) = lam.

TauCeti.IsDominantIntegral.neg_longestElement_smul records the pointwise reading of w₀ behind this: whenever lam is dominant integral, so is -(w₀ • lam), that is, w₀ • lam lands in the negative of the dominant integral weights.

source
theorem TauCeti.exists_ne_zero_lieInvariant_irreducibleQuotient_iff {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] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} [IsAlgClosed K] (hlam : IsDominantIntegral b lam) :
(∃ (Φ : LinearMap.BilinForm K (irreducibleQuotient b lam)), Φ ≠ 0 ∧ LinearMap.BilinForm.lieInvariant L Φ) ↔ -(longestElement (LieAlgebra.IsKilling.rootSystem H) b • lam) = lam

The self-duality criterion at the named carrier L(lam). For dominant integral lam, the module L(lam) carries a nonzero invariant bilinear form exactly when -(w₀ • lam) = lam.

Dominance makes L(lam) finite-dimensional (TauCeti.finiteDimensional_of_isHighestWeightVector_of_isDominantIntegral), so no finite-dimensionality hypothesis is needed.