# mathlibdocumentation

algebra.lie.ideal_operations

# 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

@[instance]
def lie_submodule.has_bracket {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] :
has_bracket L) L 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 lie_submodule.lie_ideal_oper_eq_span {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (I : L) :
I,N = {m : M | ∃ (x : I) (n : N), x,n = m}
theorem lie_submodule.lie_ideal_oper_eq_linear_span {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (I : L) :
I,N = {m : M | ∃ (x : I) (n : N), x,n = m}

See also lie_submodule.lie_ideal_oper_eq_tensor_map_range.

theorem lie_submodule.lie_coe_mem_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (I : L) (x : I) (m : N) :
theorem lie_submodule.lie_mem_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (I : L) {x : L} {m : M} (hx : x I) (hm : m N) :
theorem lie_submodule.lie_comm {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I J : L) :
theorem lie_submodule.lie_le_right {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (I : L) :
theorem lie_submodule.lie_le_left {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I J : L) :
theorem lie_submodule.lie_le_inf {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I J : L) :
@[simp]
theorem lie_submodule.lie_bot {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (I : L) :
@[simp]
theorem lie_submodule.bot_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) :
theorem lie_submodule.mono_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N N' : M) (I J : L) (h₁ : I J) (h₂ : N N') :
theorem lie_submodule.mono_lie_left {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (I J : L) (h : I J) :
theorem lie_submodule.mono_lie_right {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N N' : M) (I : L) (h : N N') :
@[simp]
theorem lie_submodule.lie_sup {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N N' : M) (I : L) :
@[simp]
theorem lie_submodule.sup_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (I J : L) :
@[simp]
theorem lie_submodule.lie_inf {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N N' : M) (I : L) :
@[simp]
theorem lie_submodule.inf_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [ L] [ M] [ M] [ L M] (N : M) (I J : L) :
theorem lie_ideal.map_bracket_le {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') {I₁ I₂ : L} :
I₁,I₂ I₁, I₂

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

theorem lie_ideal.map_bracket_eq {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') {I₁ I₂ : L} (h : function.surjective f) :
I₁,I₂ = I₁, I₂
theorem lie_ideal.comap_bracket_le {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] (f : L →ₗ⁅R L') {J₁ J₂ : L'} :
J₁, J₂ J₁,J₂
theorem lie_ideal.map_comap_incl {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] {I₁ I₂ : L} :
I₂) = I₁ I₂
theorem lie_ideal.comap_bracket_eq {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {J₁ J₂ : L'} (h : f.is_ideal_morphism) :
f.ideal_range J₁,f.ideal_range J₂ = J₁, J₂ f.ker
theorem lie_ideal.map_comap_bracket_eq {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [ L] [lie_ring L'] [ L'] {f : L →ₗ⁅R L'} {J₁ J₂ : L'} (h : f.is_ideal_morphism) :
J₁, J₂ = f.ideal_range J₁,f.ideal_range J₂
theorem lie_ideal.comap_bracket_incl {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) {I₁ I₂ : L} :
I₁, I₂ = I I₁,I I₂
theorem lie_ideal.comap_bracket_incl_of_le {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [ L] (I : L) {I₁ I₂ : L} (h₁ : I₁ I) (h₂ : I₂ I) :
I₁, I₂ = 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.