# mathlibdocumentation

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 #

• lie_module.weight_space
• lie_module.is_weight
• lie_algebra.root_space
• lie_algebra.is_root
• lie_algebra.root_space_weight_space_product
• lie_algebra.root_space_product

## 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] [ L] (M : Type w) [ M] [ M] [ L M] (χ : L → R) :
M

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
• = ⨅ (x : L), (χ x)
theorem lie_module.mem_pre_weight_space {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (M : Type w) [ M] [ M] [ L M] (χ : L → R) (m : M) :
∀ (x : L), ∃ (k : ), (( M) x - χ x 1) ^ k) m = 0
theorem lie_module.weight_vector_multiplication {R : Type u} (L : Type v) [comm_ring R] [lie_ring L] [ L] (M₁ : Type w₁) (M₂ : Type w₂) (M₃ : Type w₃) [add_comm_group M₁] [ M₁] [ M₁] [ L M₁] [add_comm_group M₂] [ M₂] [ M₂] [ L M₂] [add_comm_group M₃] [ M₃] [ M₃] [ L M₃] (g : M₁ M₂ →ₗ⁅R,L M₃) (χ₁ χ₂ : L → R) :
(g ∘ₗ .range (χ₁ + χ₂)

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] [ L] {M : Type w} [ M] [ M] [ L M] {χ₁ χ₂ : L → R} {x : L} {m : M} (hx : x ) (hm : m ) :
x,m (χ₁ + χ₂)
def lie_module.weight_space {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (M : Type w) [ M] [ M] [ L M] (χ : L → R) :
M

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] [ L] (M : Type w) [ M] [ M] [ L M] (χ : L → R) (m : M) :
@[simp]
theorem lie_module.zero_weight_space_eq_top_of_nilpotent' {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (M : Type w) [ M] [ M] [ L M] [ M] :

See also the more useful form lie_module.zero_weight_space_eq_top_of_nilpotent.

theorem lie_module.coe_weight_space_of_top {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (M : Type w) [ M] [ M] [ L M] (χ : L → R) :
@[simp]
theorem lie_module.zero_weight_space_eq_top_of_nilpotent {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (M : Type w) [ M] [ M] [ L M] [ M] :
def lie_module.is_weight {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (H : L) (M : Type w) [ M] [ M] [ L M] (χ : 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
• χ =
theorem lie_module.is_weight_zero_of_nilpotent {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (M : Type w) [ M] [ M] [ L M] [nontrivial M] [ M] :

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] [ L] (H : L) (χ : H → R) :
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.

@[simp]
theorem lie_algebra.zero_root_space_eq_top_of_nilpotent {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] [h : L] :
def lie_algebra.is_root {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (H : L) (χ : 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 lie_algebra.root_space_comap_eq_weight_space {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (H : L) (χ : H → R) :
theorem lie_algebra.lie_mem_weight_space_of_mem_weight_space {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {H : L} {M : Type w} [ M] [ M] [ L M] {χ₁ χ₂ : H → R} {x : L} {m : M} (hx : x ) (hm : m ) :
x,m (χ₁ + χ₂)
def lie_algebra.root_space_weight_space_product (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (H : L) (M : Type w) [ M] [ M] [ L M] (χ₁ χ₂ χ₃ : H → R) (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] [ L] (H : L) (M : Type w) [ M] [ M] [ L M] (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) (x : χ₁)) (m : χ₂)) :
( χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] m)) = x,m
def lie_algebra.root_space_product (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (H : L) (χ₁ χ₂ χ₃ : H → R) (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
• χ₁ χ₂ χ₃ = χ₂ χ₃
@[simp]
theorem lie_algebra.root_space_product_def (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (H : L)  :
theorem lie_algebra.root_space_product_tmul (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (H : L) (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) (x : χ₁)) (y : χ₂)) :
( χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] y)) = x,y
def lie_algebra.zero_root_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (H : L)  :

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

Equations
@[simp]
theorem lie_algebra.coe_zero_root_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (H : L)  :
theorem lie_algebra.mem_zero_root_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (H : L) (x : L) :
∀ (y : H), ∃ (k : ), ( L) y ^ k) x = 0
theorem lie_algebra.to_lie_submodule_le_root_space_zero (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (H : L)  :
theorem lie_algebra.le_zero_root_subalgebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (H : L)  :
@[simp]
theorem lie_algebra.zero_root_subalgebra_normalizer_eq_self (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (H : L)  :
theorem lie_algebra.zero_root_subalgebra_is_cartan_of_eq (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [ L] (H : L) (h : = H) :

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] [ L] {H : L} (M : Type w) [ M] [ M] [ L M] (χ : H → R) :
M

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] [ L] {H : L} (M : Type w) [ M] [ M] [ L M] (χ : H → R) :