mathlib documentation

algebra.lie.weights

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 #

References #

Tags #

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

def lie_module.pre_weight_space {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type w) [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (χ : L → R) :

Given a Lie module M over a Lie algebra L, the pre-weight space of M with respect to a map χ : L → R is the simultaneous generalized eigenspace of the action of all x : L on M, with eigenvalues χ x.

See also lie_module.weight_space.

Equations
theorem lie_module.mem_pre_weight_space {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type w) [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (χ : L → R) (m : M) :
m lie_module.pre_weight_space M χ ∀ (x : L), ∃ (k : ), (((lie_module.to_endomorphism R L M) x - χ x 1) ^ k) m = 0
@[protected]
theorem lie_module.weight_vector_multiplication {R : Type u} (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (M₁ : Type w₁) (M₂ : Type w₂) (M₃ : Type w₃) [add_comm_group M₁] [module R M₁] [lie_ring_module L M₁] [lie_module R L M₁] [add_comm_group M₂] [module R M₂] [lie_ring_module L M₂] [lie_module R L M₂] [add_comm_group M₃] [module R M₃] [lie_ring_module L M₃] [lie_module R L M₃] (g : M₁ M₂ →ₗ⁅R,L M₃) (χ₁ χ₂ : L → R) :

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

theorem lie_module.lie_mem_pre_weight_space_of_mem_pre_weight_space {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {M : Type w} [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {χ₁ χ₂ : L → R} {x : L} {m : M} (hx : x lie_module.pre_weight_space L χ₁) (hm : m lie_module.pre_weight_space M χ₂) :
def lie_module.weight_space {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type w) [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [lie_algebra.is_nilpotent R L] (χ : L → R) :

If a Lie algebra is nilpotent, then pre-weight spaces are Lie submodules.

Equations
theorem lie_module.mem_weight_space {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type w) [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [lie_algebra.is_nilpotent R L] (χ : L → R) (m : M) :
theorem lie_module.coe_weight_space_of_top {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (M : Type w) [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [lie_algebra.is_nilpotent R L] (χ : L → R) :
def lie_module.is_weight {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [lie_algebra.is_nilpotent R H] (M : Type w) [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (χ : lie_algebra.lie_character R 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.

Equations

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

def lie_algebra.root_space {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [lie_algebra.is_nilpotent R H] (χ : H → R) :

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.

def lie_algebra.is_root {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [lie_algebra.is_nilpotent R H] (χ : lie_algebra.lie_character R 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.

theorem lie_algebra.lie_mem_weight_space_of_mem_weight_space {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {H : lie_subalgebra R L} [lie_algebra.is_nilpotent R H] {M : Type w} [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {χ₁ χ₂ : H → R} {x : L} {m : M} (hx : x lie_algebra.root_space H χ₁) (hm : m lie_module.weight_space M χ₂) :
def lie_algebra.root_space_weight_space_product_aux (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [lie_algebra.is_nilpotent R H] (M : Type w) [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] {χ₁ χ₂ χ₃ : H → R} (hχ : χ₁ + χ₂ = χ₃) :

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

Equations
def lie_algebra.root_space_weight_space_product (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [lie_algebra.is_nilpotent R H] (M : Type w) [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) :

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.

Equations
@[simp]
theorem lie_algebra.coe_root_space_weight_space_product_tmul (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [lie_algebra.is_nilpotent R H] (M : Type w) [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) (x : (lie_algebra.root_space H χ₁)) (m : (lie_module.weight_space M χ₂)) :
def lie_algebra.root_space_product (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [lie_algebra.is_nilpotent R H] (χ₁ χ₂ χ₃ : H → R) (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.

Equations
theorem lie_algebra.root_space_product_tmul (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [lie_algebra.is_nilpotent R H] (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) (x : (lie_algebra.root_space H χ₁)) (y : (lie_algebra.root_space H χ₂)) :
((lie_algebra.root_space_product R L H χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] y)) = x,y

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

Equations
theorem lie_algebra.mem_zero_root_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) [lie_algebra.is_nilpotent R H] (x : L) :
x lie_algebra.zero_root_subalgebra R L H ∀ (y : H), ∃ (k : ), ((lie_module.to_endomorphism R H L) y ^ k) x = 0

In finite dimensions over a field (and possibly more generally) Engel's theorem shows that the converse of this is also true, i.e., zero_root_subalgebra R L H = H ↔ lie_subalgebra.is_cartan_subalgebra H.

def lie_module.weight_space' {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {H : lie_subalgebra R L} [lie_algebra.is_nilpotent R H] (M : Type w) [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (χ : H → R) :

A priori, weight spaces are Lie submodules over the Lie subalgebra H used to define them. However they are naturally Lie submodules over the (in general larger) Lie subalgebra zero_root_subalgebra R L H. Even though it is often the case that zero_root_subalgebra R L H = H, it is likely to be useful to have the flexibility not to have to invoke this equality (as well as to work more generally).

Equations
@[simp]
theorem lie_module.coe_weight_space' {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] {H : lie_subalgebra R L} [lie_algebra.is_nilpotent R H] (M : Type w) [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (χ : H → R) :