Weights and roots of Lie modules and Lie algebras

Just as a key tool when studying the behaviour of a linear operator is to decompose the space on which it acts into a sum of (generalised) eigenspaces, a key tool when studying a representation M of Lie algebra L is to decompose M into a sum of simultaneous eigenspaces of x as x ranges over L. These simultaneous generalised eigenspaces are known as the weight spaces of M.

When L is nilpotent, it follows from the binomial theorem that weight spaces are Lie submodules. Even when L is not nilpotent, it may be useful to study its representations by restricting them to a nilpotent subalgebra (e.g., a Cartan subalgebra). In the particular case when we view L as a module over itself via the adjoint action, the weight spaces of L restricted to a nilpotent subalgebra are known as root spaces.

Basic definitions and properties of the above ideas are provided in this file.

Main definitions

• LieModule.weightSpaceOf
• LieModule.weightSpace
• LieModule.IsWeight
• LieAlgebra.rootSpace
• LieAlgebra.IsRoot
• LieAlgebra.rootSpaceWeightSpaceProduct
• LieAlgebra.rootSpaceProduct
• LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 7--9

Tags

lie character, eigenvalue, eigenspace, weight, weight vector, root, root vector

theorem LieModule.weight_vector_multiplication {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M₁ : Type w₁) (M₂ : Type w₂) (M₃ : Type w₃) [AddCommGroup M₁] [Module R M₁] [LieRingModule L M₁] [LieModule R L M₁] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] [AddCommGroup M₃] [Module R M₃] [LieRingModule L M₃] [LieModule R L M₃] (g : TensorProduct R M₁ M₂ →ₗ⁅R,L⁆ M₃) (χ₁ : R) (χ₂ : R) (x : L) : LinearMap.range (LinearMap.comp (↑g) (TensorProduct.mapIncl (Module.End.maximalGeneralizedEigenspace (↑(LieModule.toEndomorphism R L M₁) x) χ₁) (Module.End.maximalGeneralizedEigenspace (↑(LieModule.toEndomorphism R L M₂) x) χ₂))) ≤ Module.End.maximalGeneralizedEigenspace (↑(LieModule.toEndomorphism R L M₃) x) (χ₁ + χ₂)

See also bourbaki1975b Chapter VII §1.1, Proposition 2 (ii).

theorem LieModule.lie_mem_maxGenEigenspace_toEndomorphism {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type w} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ : R} {χ₂ : R} {x : L} {y : L} {m : M} (hy : y ∈ Module.End.maximalGeneralizedEigenspace (↑(LieModule.toEndomorphism R L L) x) χ₁) (hm : m ∈ Module.End.maximalGeneralizedEigenspace (↑(LieModule.toEndomorphism R L M) x) χ₂) : ⁅y, m⁆ ∈ Module.End.maximalGeneralizedEigenspace (↑(LieModule.toEndomorphism R L M) x) (χ₁ + χ₂)

def LieModule.weightSpaceOf {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ : R) (x : L) : LieSubmodule R L M

If M is a representation of a nilpotent Lie algebra L, χ is a scalar, and x : L, then weightSpaceOf M χ x is the maximal generalized χ-eigenspace of the action of x on M.

It is a Lie submodule because L is nilpotent.

theorem LieModule.mem_weightSpaceOf {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ : R) (x : L) (m : M) : m ∈ LieModule.weightSpaceOf M χ x ↔ ∃ k, ↑((↑(LieModule.toEndomorphism R L M) x - χ • 1) ^ k) m = 0

def LieModule.weightSpace {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ : L → R) : LieSubmodule R L M

If M is a representation of a nilpotent Lie algebra L and χ : L → R is a family of scalars, then weightSpace M χ is the intersection of the maximal generalized χ x-eigenspaces of the action of x on M as x ranges over L.

It is a Lie submodule because L is nilpotent.

theorem LieModule.mem_weightSpace {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ : L → R) (m : M) : m ∈ LieModule.weightSpace M χ ↔ ∀ (x : L), ∃ k, ↑((↑(LieModule.toEndomorphism R L M) x - χ x • 1) ^ k) m = 0

@[simp]

theorem LieModule.zero_weightSpace_eq_top_of_nilpotent' {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.IsNilpotent R L M] : LieModule.weightSpace M 0 = ⊤

See also the more useful form LieModule.zero_weightSpace_eq_top_of_nilpotent.

theorem LieModule.coe_weightSpace_of_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ : L → R) : ↑(LieModule.weightSpace M (χ ∘ ↑(LieSubalgebra.incl ⊤))) = ↑(LieModule.weightSpace M χ)

@[simp]

theorem LieModule.zero_weightSpace_eq_top_of_nilpotent {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [LieModule.IsNilpotent R L M] : LieModule.weightSpace M 0 = ⊤

def LieModule.IsWeight {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ : LieAlgebra.LieCharacter R { x // x ∈ H }) : Prop

Given a Lie module M of a Lie algebra L, a weight of M with respect to a nilpotent subalgebra H ⊆ L is a Lie character whose corresponding weight space is non-empty.

theorem LieModule.isWeight_zero_of_nilpotent {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Nontrivial M] [LieAlgebra.IsNilpotent R L] [LieModule.IsNilpotent R L M] : LieModule.IsWeight ⊤ M 0

For a non-trivial nilpotent Lie module over a nilpotent Lie algebra, the zero character is a weight with respect to the ⊤ Lie subalgebra.

theorem LieModule.exists_weightSpace_zero_le_ker_of_isNoetherian (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] (x : L) : ∃ k, ↑(LieModule.weightSpace M 0) ≤ LinearMap.ker (↑(LieModule.toEndomorphism R L M) x ^ k)

theorem LieModule.isNilpotent_toEndomorphism_weightSpace_zero {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] (x : L) : IsNilpotent (↑(LieModule.toEndomorphism R L { x // x ∈ ↑(LieModule.weightSpace M 0) }) x)

A (nilpotent) Lie algebra acts nilpotently on the zero weight space of a Noetherian Lie module.

instance LieModule.instIsNilpotentSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleWeightSpaceOfNatForAllToOfNat0InstZeroToZeroToCommMonoidWithZeroAddCommGroupToRingInstModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommMonoidInstLieRingModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommGroupToRing {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] : LieModule.IsNilpotent R L { x // x ∈ ↑(LieModule.weightSpace M 0) }

By Engel's theorem, the zero weight space of a Noetherian Lie module is nilpotent.

@[inline, reducible]

abbrev LieAlgebra.rootSpace {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] (χ : { x // x ∈ H } → R) : LieSubmodule R { x // x ∈ H } L

Given a nilpotent Lie subalgebra H ⊆ L, the root space of a map χ : H → R is the weight space of L regarded as a module of H via the adjoint action.

theorem LieAlgebra.zero_rootSpace_eq_top_of_nilpotent {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] : LieAlgebra.rootSpace ⊤ 0 = ⊤

@[inline, reducible]

abbrev LieAlgebra.IsRoot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] (χ : LieAlgebra.LieCharacter R { x // x ∈ H }) : Prop

A root of a Lie algebra L with respect to a nilpotent subalgebra H ⊆ L is a weight of L, regarded as a module of H via the adjoint action.

@[simp]

theorem LieAlgebra.rootSpace_comap_eq_weightSpace {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] (χ : { x // x ∈ H } → R) : LieSubmodule.comap (LieSubalgebra.incl' H) (LieAlgebra.rootSpace H χ) = LieModule.weightSpace { x // x ∈ H } χ

theorem LieAlgebra.lie_mem_weightSpace_of_mem_weightSpace {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieAlgebra.IsNilpotent R { x // x ∈ H }] {M : Type w} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ : { x // x ∈ H } → R} {χ₂ : { x // x ∈ H } → R} {x : L} {m : M} (hx : x ∈ LieAlgebra.rootSpace H χ₁) (hm : m ∈ LieModule.weightSpace M χ₂) : ⁅x, m⁆ ∈ LieModule.weightSpace M (χ₁ + χ₂)

def LieAlgebra.rootSpaceWeightSpaceProductAux (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ : { x // x ∈ H } → R} {χ₂ : { x // x ∈ H } → R} {χ₃ : { x // x ∈ H } → R} (hχ : χ₁ + χ₂ = χ₃) : { x // x ∈ ↑(LieAlgebra.rootSpace H χ₁) } →ₗ[R] { x // x ∈ ↑(LieModule.weightSpace M χ₂) } →ₗ[R] { x // x ∈ ↑(LieModule.weightSpace M χ₃) }

Auxiliary definition for rootSpaceWeightSpaceProduct, which is close to the deterministic timeout limit.

def LieAlgebra.rootSpaceWeightSpaceProduct (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ₁ : { x // x ∈ H } → R) (χ₂ : { x // x ∈ H } → R) (χ₃ : { x // x ∈ H } → R) (hχ : χ₁ + χ₂ = χ₃) : TensorProduct R { x // x ∈ ↑(LieAlgebra.rootSpace H χ₁) } { x // x ∈ ↑(LieModule.weightSpace M χ₂) } →ₗ⁅R,{ x // x ∈ H }⁆ { x // x ∈ ↑(LieModule.weightSpace M χ₃) }

Given a nilpotent Lie subalgebra H ⊆ L together with χ₁ χ₂ : H → R, there is a natural R-bilinear product of root vectors and weight vectors, compatible with the actions of H.

@[simp]

theorem LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ₁ : { x // x ∈ H } → R) (χ₂ : { x // x ∈ H } → R) (χ₃ : { x // x ∈ H } → R) (hχ : χ₁ + χ₂ = χ₃) (x : { x // x ∈ LieAlgebra.rootSpace H χ₁ }) (m : { x // x ∈ LieModule.weightSpace M χ₂ }) : ↑(↑(LieAlgebra.rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] m)) = ⁅↑x, ↑m⁆

def LieAlgebra.rootSpaceProduct (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] (χ₁ : { x // x ∈ H } → R) (χ₂ : { x // x ∈ H } → R) (χ₃ : { x // x ∈ H } → R) (hχ : χ₁ + χ₂ = χ₃) : TensorProduct R { x // x ∈ ↑(LieAlgebra.rootSpace H χ₁) } { x // x ∈ ↑(LieAlgebra.rootSpace H χ₂) } →ₗ⁅R,{ x // x ∈ H }⁆ { x // x ∈ ↑(LieAlgebra.rootSpace H χ₃) }

Given a nilpotent Lie subalgebra H ⊆ L together with χ₁ χ₂ : H → R, there is a natural R-bilinear product of root vectors, compatible with the actions of H.

@[simp]

theorem LieAlgebra.rootSpaceProduct_def (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] : LieAlgebra.rootSpaceProduct R L H = LieAlgebra.rootSpaceWeightSpaceProduct R L H L

theorem LieAlgebra.rootSpaceProduct_tmul (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] (χ₁ : { x // x ∈ H } → R) (χ₂ : { x // x ∈ H } → R) (χ₃ : { x // x ∈ H } → R) (hχ : χ₁ + χ₂ = χ₃) (x : { x // x ∈ LieAlgebra.rootSpace H χ₁ }) (y : { x // x ∈ LieAlgebra.rootSpace H χ₂ }) : ↑(↑(LieAlgebra.rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] y)) = ⁅↑x, ↑y⁆

def LieAlgebra.zeroRootSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] : LieSubalgebra R L

Given a nilpotent Lie subalgebra H ⊆ L, the root space of the zero map 0 : H → R is a Lie subalgebra of L.

@[simp]

theorem LieAlgebra.coe_zeroRootSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] : (LieAlgebra.zeroRootSubalgebra R L H).toSubmodule = ↑(LieAlgebra.rootSpace H 0)

theorem LieAlgebra.mem_zeroRootSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] (x : L) : x ∈ LieAlgebra.zeroRootSubalgebra R L H ↔ ∀ (y : { x // x ∈ H }), ∃ k, ↑(↑(LieModule.toEndomorphism R { x // x ∈ H } L) y ^ k) x = 0

theorem LieAlgebra.toLieSubmodule_le_rootSpace_zero (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] : LieSubalgebra.toLieSubmodule H ≤ LieAlgebra.rootSpace H 0

theorem LieAlgebra.le_zeroRootSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] : H ≤ LieAlgebra.zeroRootSubalgebra R L H

@[simp]

theorem LieAlgebra.zeroRootSubalgebra_normalizer_eq_self (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] : LieSubalgebra.normalizer (LieAlgebra.zeroRootSubalgebra R L H) = LieAlgebra.zeroRootSubalgebra R L H

theorem LieAlgebra.is_cartan_of_zeroRootSubalgebra_eq (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] (h : LieAlgebra.zeroRootSubalgebra R L H = H) : LieSubalgebra.IsCartanSubalgebra H

If the zero root subalgebra of a nilpotent Lie subalgebra H is just H then H is a Cartan subalgebra.

When L is Noetherian, it follows from Engel's theorem that the converse holds. See LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan

@[simp]

theorem LieAlgebra.zeroRootSubalgebra_eq_of_is_cartan (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieSubalgebra.IsCartanSubalgebra H] [IsNoetherian R L] : LieAlgebra.zeroRootSubalgebra R L H = H

theorem LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R { x // x ∈ H }] [IsNoetherian R L] : LieAlgebra.zeroRootSubalgebra R L H = H ↔ LieSubalgebra.IsCartanSubalgebra H