Weights and roots of Lie modules and Lie algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_spacelie_module.is_weightlie_algebra.root_spacelie_algebra.is_rootlie_algebra.root_space_weight_space_productlie_algebra.root_space_productlie_algebra.zero_root_subalgebra_eq_iff_is_cartan
References #
Tags #
lie character, eigenvalue, eigenspace, weight, weight vector, root, root vector
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
- lie_module.pre_weight_space M χ = ⨅ (x : L), (⇑(lie_module.to_endomorphism R L M) x).maximal_generalized_eigenspace (χ x)
See also bourbaki1975b Chapter VII §1.1, Proposition 2 (ii).
If a Lie algebra is nilpotent, then pre-weight spaces are Lie submodules.
Equations
- lie_module.weight_space M χ = {carrier := (lie_module.pre_weight_space M χ).carrier, add_mem' := _, zero_mem' := _, smul_mem' := _, lie_mem := _}
Instances for ↥lie_module.weight_space
See also the more useful form lie_module.zero_weight_space_eq_top_of_nilpotent.
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
- lie_module.is_weight H M χ = (lie_module.weight_space 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.
A (nilpotent) Lie algebra acts nilpotently on the zero weight space of a Noetherian Lie module.
By Engel's theorem, when the Lie algebra is Noetherian, the zero weight space of a Noetherian Lie module is nilpotent.
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.
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.
Auxiliary definition for root_space_weight_space_product,
which is close to the deterministic timeout limit.
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
- lie_algebra.root_space_weight_space_product R L H M χ₁ χ₂ χ₃ hχ = ⇑(tensor_product.lie_module.lift_lie R ↥H ↥(lie_algebra.root_space H χ₁) ↥(lie_module.weight_space M χ₂) ↥(lie_module.weight_space M χ₃)) {to_linear_map := lie_algebra.root_space_weight_space_product_aux R L H M hχ, map_lie' := _}
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
- lie_algebra.root_space_product R L H χ₁ χ₂ χ₃ hχ = lie_algebra.root_space_weight_space_product R L H L χ₁ χ₂ χ₃ hχ
Given a nilpotent Lie subalgebra H ⊆ L, the root space of the zero map 0 : H → R is a Lie
subalgebra of L.
Equations
- lie_algebra.zero_root_subalgebra R L H = {to_submodule := {carrier := ↑(lie_algebra.root_space H 0).carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}, lie_mem' := _}
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
lie_algebra.zero_root_subalgebra_eq_iff_is_cartan
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).