# Documentation

Mathlib.Algebra.Lie.IdealOperations

# 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.

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 | x 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 | x 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 | x, x I n, n N 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' ∀ (x : L), x I∀ (m : M), m Nx, 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 : { x // x I }) (m : { x // x 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 = ∀ (x : L), x I∀ (m : M), m Nx, 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₂
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 : ) :
= 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₁ : ) (hf₂ : ) :
@[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) :
= 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 () (LieIdeal.comap () 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 : ) :
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 : ) :
theorem LieIdeal.comap_bracket_incl {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) {I₁ : LieIdeal R L} {I₂ : LieIdeal R L} :
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) :

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.