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 #

• LieSubmodule.hasBracket
• LieSubmodule.lieIdeal_oper_eq_linear_span
• LieIdeal.map_bracket_le
• LieIdeal.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

instance LieSubmodule.hasBracket {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] :

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
theorem LieSubmodule.lieIdeal_oper_eq_span {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (I : LieIdeal R L) :
I, N = LieSubmodule.lieSpan R L {m : M | ∃ (x : I) (n : N), x, n = m}
theorem LieSubmodule.lieIdeal_oper_eq_linear_span {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (I : LieIdeal R L) :
I, N = Submodule.span R {m : M | ∃ (x : I) (n : N), x, n = m}

See also LieSubmodule.lieIdeal_oper_eq_linear_span' and LieSubmodule.lieIdeal_oper_eq_tensor_map_range.

theorem LieSubmodule.lieIdeal_oper_eq_linear_span' {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) (I : LieIdeal R L) :
I, N = Submodule.span R {m : M | xI, nN, x, n = m}
theorem LieSubmodule.lie_le_iff {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) (I : LieIdeal R L) :
I, N N' xI, mN, x, m N'
theorem LieSubmodule.lie_coe_mem_lie {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (I : LieIdeal R L) (x : I) (m : N) :
x, m I, N
theorem LieSubmodule.lie_mem_lie {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (I : LieIdeal R L) {x : L} {m : M} (hx : x I) (hm : m N) :
theorem LieSubmodule.lie_comm {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (J : LieIdeal R L) :
theorem LieSubmodule.lie_le_right {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (I : LieIdeal R L) :
theorem LieSubmodule.lie_le_left {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (J : LieIdeal R L) :
theorem LieSubmodule.lie_le_inf {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) (J : LieIdeal R L) :
I, J I J
@[simp]
theorem LieSubmodule.lie_bot {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (I : LieIdeal R L) :
@[simp]
theorem LieSubmodule.bot_lie {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) :
theorem LieSubmodule.lie_eq_bot_iff {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (I : LieIdeal R L) :
I, N = xI, mN, x, m = 0
theorem LieSubmodule.mono_lie {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) (I : LieIdeal R L) (J : LieIdeal R L) (h₁ : I J) (h₂ : N N') :
theorem LieSubmodule.mono_lie_left {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (I : LieIdeal R L) (J : LieIdeal R L) (h : I J) :
theorem LieSubmodule.mono_lie_right {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) (I : LieIdeal R L) (h : N N') :
@[simp]
theorem LieSubmodule.lie_sup {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) (I : LieIdeal R L) :
@[simp]
theorem LieSubmodule.sup_lie {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (I : LieIdeal R L) (J : LieIdeal R L) :
theorem LieSubmodule.lie_inf {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) (I : LieIdeal R L) :
theorem LieSubmodule.inf_lie {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (I : LieIdeal R L) (J : LieIdeal R L) :
theorem LieSubmodule.map_bracket_eq {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R M₂] [] [LieModule R L M₂] (N : LieSubmodule R L M) (I : LieIdeal R L) (f : M →ₗ⁅R,L M₂) :
theorem LieSubmodule.map_comap_le {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [] [] [] [Module R M] [] [] [Module R M₂] [] (N₂ : LieSubmodule R L M₂) (f : M →ₗ⁅R,L M₂) :
N₂
theorem LieSubmodule.map_comap_eq {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [] [] [] [Module R M] [] [] [Module R M₂] [] (N₂ : LieSubmodule R L M₂) (f : M →ₗ⁅R,L M₂) (hf : N₂ f.range) :
= N₂
theorem LieSubmodule.le_comap_map {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [] [] [] [Module R M] [] [] [Module R M₂] [] (N : LieSubmodule R L M) (f : M →ₗ⁅R,L M₂) :
N
theorem LieSubmodule.comap_map_eq {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [] [] [] [Module R M] [] [] [Module R M₂] [] (N : LieSubmodule R L M) (f : M →ₗ⁅R,L M₂) (hf : f.ker = ) :
= N
theorem LieSubmodule.comap_bracket_eq {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R M₂] [] [LieModule R L M₂] (I : LieIdeal R L) (N₂ : LieSubmodule R L M₂) (f : M →ₗ⁅R,L M₂) (hf₁ : f.ker = ) (hf₂ : N₂ f.range) :
@[simp]
theorem LieSubmodule.map_comap_incl {R : Type u} {L : Type v} {M : Type w} [] [] [] [Module R M] [] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) :
LieSubmodule.map N.incl (LieSubmodule.comap N.incl N') = N N'
theorem LieIdeal.map_bracket_le {R : Type u} {L : Type v} {L' : Type w₂} [] [] [] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R L') {I₁ : LieIdeal R L} {I₂ : LieIdeal R L} :

Note that the inequality can be strict; e.g., the inclusion of an Abelian subalgebra of a simple algebra.

theorem LieIdeal.map_bracket_eq {R : Type u} {L : Type v} {L' : Type w₂} [] [] [] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R L') {I₁ : LieIdeal R L} {I₂ : LieIdeal R L} (h : ) :
theorem LieIdeal.comap_bracket_le {R : Type u} {L : Type v} {L' : Type w₂} [] [] [] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R L') {J₁ : LieIdeal R L'} {J₂ : LieIdeal R L'} :
theorem LieIdeal.map_comap_incl {R : Type u} {L : Type v} [] [] [] {I₁ : LieIdeal R L} {I₂ : LieIdeal R L} :
LieIdeal.map I₁.incl (LieIdeal.comap I₁.incl I₂) = I₁ I₂
theorem LieIdeal.comap_bracket_eq {R : Type u} {L : Type v} {L' : Type w₂} [] [] [] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R L'} {J₁ : LieIdeal R L'} {J₂ : LieIdeal R L'} (h : f.IsIdealMorphism) :
LieIdeal.comap f f.idealRange J₁, f.idealRange J₂ = , f.ker
theorem LieIdeal.map_comap_bracket_eq {R : Type u} {L : Type v} {L' : Type w₂} [] [] [] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R L'} {J₁ : LieIdeal R L'} {J₂ : LieIdeal R L'} (h : f.IsIdealMorphism) :
LieIdeal.map f , = f.idealRange J₁, f.idealRange J₂
theorem LieIdeal.comap_bracket_incl {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) {I₁ : LieIdeal R L} {I₂ : LieIdeal R L} :
LieIdeal.comap I.incl I₁, LieIdeal.comap I.incl I₂ = LieIdeal.comap I.incl I I₁, I I₂
theorem LieIdeal.comap_bracket_incl_of_le {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) {I₁ : LieIdeal R L} {I₂ : LieIdeal R L} (h₁ : I₁ I) (h₂ : I₂ I) :
LieIdeal.comap I.incl I₁, LieIdeal.comap I.incl I₂ = LieIdeal.comap I.incl I₁, I₂

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.