mathlib documentation

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 #

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

@[protected, instance]
def lie_submodule.has_bracket {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (I : lie_ideal R L) :
I,N = lie_submodule.lie_span R L {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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (I : lie_ideal R L) :
I,N = submodule.span R {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.

theorem lie_submodule.lie_ideal_oper_eq_linear_span' {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (I : lie_ideal R L) :
I,N = submodule.span R {m : M | ∃ (x : L) (H : x I) (n : M) (H : n N), x,n = m}
theorem lie_submodule.lie_le_iff {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) (I : lie_ideal R L) :
I,N N' ∀ (x : L), x I∀ (m : M), m Nx,m N'
theorem lie_submodule.lie_coe_mem_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (I : lie_ideal R 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (I : lie_ideal R 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] [lie_algebra R L] (I J : lie_ideal R L) :
theorem lie_submodule.lie_le_right {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (I : lie_ideal R L) :
theorem lie_submodule.lie_le_left {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I J : lie_ideal R L) :
theorem lie_submodule.lie_le_inf {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L] (I J : lie_ideal R L) :
@[simp]
theorem lie_submodule.lie_bot {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (I : lie_ideal R L) :
@[simp]
theorem lie_submodule.bot_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) :
theorem lie_submodule.lie_eq_bot_iff {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (I : lie_ideal R L) :
I,N = ∀ (x : L), x I∀ (m : M), m Nx,m = 0
theorem lie_submodule.mono_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) (I J : lie_ideal R 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (I J : lie_ideal R 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) (I : lie_ideal R 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] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) (I : lie_ideal R L) :
@[simp]
theorem lie_submodule.sup_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (I J : lie_ideal R L) :
@[simp]
theorem lie_submodule.lie_inf {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) (I : lie_ideal R L) :
@[simp]
theorem lie_submodule.inf_lie {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N : lie_submodule R L M) (I J : lie_ideal R L) :
theorem lie_submodule.map_bracket_eq {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M₂] [module R M₂] [lie_ring_module L M₂] [lie_module R L M₂] (N : lie_submodule R L M) (I : lie_ideal R L) (f : M →ₗ⁅R,L M₂) :
theorem lie_submodule.map_comap_le {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M₂] [module R M₂] [lie_ring_module L M₂] [lie_module R L M₂] (N₂ : lie_submodule R L M₂) (f : M →ₗ⁅R,L M₂) :
theorem lie_submodule.map_comap_eq {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M₂] [module R M₂] [lie_ring_module L M₂] [lie_module R L M₂] (N₂ : lie_submodule R L M₂) (f : M →ₗ⁅R,L M₂) (hf : N₂ f.range) :
theorem lie_submodule.le_comap_map {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M₂] [module R M₂] [lie_ring_module L M₂] [lie_module R L M₂] (N : lie_submodule R L M) (f : M →ₗ⁅R,L M₂) :
theorem lie_submodule.comap_map_eq {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M₂] [module R M₂] [lie_ring_module L M₂] [lie_module R L M₂] (N : lie_submodule R L M) (f : M →ₗ⁅R,L M₂) (hf : f.ker = ) :
theorem lie_submodule.comap_bracket_eq {R : Type u} {L : Type v} {M : Type w} {M₂ : Type w₁} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] [add_comm_group M₂] [module R M₂] [lie_ring_module L M₂] [lie_module R L M₂] (I : lie_ideal R L) (N₂ : lie_submodule R L M₂) (f : M →ₗ⁅R,L M₂) (hf₁ : f.ker = ) (hf₂ : N₂ f.range) :
@[simp]
theorem lie_submodule.map_comap_incl {R : Type u} {L : Type v} {M : Type w} [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M] (N N' : lie_submodule R L M) :
theorem lie_ideal.map_bracket_le {R : Type u} {L : Type v} {L' : Type w₂} [comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L'] (f : L →ₗ⁅R L') {I₁ I₂ : lie_ideal R L} :

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