Ideal operations for Lie algebras #
Given a Lie module M
over a Lie algebra L
, there is a natural action of the Lie ideals of L
on the Lie submodules of M
. In the special case that M = L
with the adjoint action, this
provides a pairing of Lie ideals which is especially important. For example, it can be used to
define solvability / nilpotency of a Lie algebra via the derived / lower-central series.
Main definitions #
lie_submodule.has_bracket
lie_submodule.lie_ideal_oper_eq_linear_span
lie_ideal.map_bracket_le
lie_ideal.comap_bracket_le
Notation #
Given a Lie module M
over a Lie algebra L
, together with a Lie submodule N ⊆ M
and a Lie
ideal I ⊆ L
, we introduce the notation ⁅I, N⁆
for the Lie submodule of M
corresponding to
the action defined in this file.
Tags #
lie algebra, ideal operation
Given a Lie module M
over a Lie algebra L
, the set of Lie ideals of L
acts on the set
of submodules of M
.
Equations
- lie_submodule.has_bracket = {bracket := λ (I : lie_ideal R L) (N : lie_submodule R L M), lie_submodule.lie_span R L {m : M | ∃ (x : ↥I) (n : ↥N), ⁅↑x,↑n⁆ = m}}
See also lie_submodule.lie_ideal_oper_eq_linear_span'
and
lie_submodule.lie_ideal_oper_eq_tensor_map_range
.
Note that the inequality can be strict; e.g., the inclusion of an Abelian subalgebra of a simple algebra.
This is a very useful result; it allows us to use the fact that inclusion distributes over the Lie bracket operation on ideals, subject to the conditions shown.