Ideal operations for Lie algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_bracketlie_submodule.lie_ideal_oper_eq_linear_spanlie_ideal.map_bracket_lelie_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
@[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] :
has_bracket (lie_ideal R L) (lie_submodule 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.
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) :
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) :
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) :
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) :
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_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) :
@[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) :
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₂) :
lie_submodule.map f ⁅I, N⁆ = ⁅I, lie_submodule.map f N⁆
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₂) :
lie_submodule.map f (lie_submodule.comap f N₂) ≤ N₂
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) :
lie_submodule.map f (lie_submodule.comap f N₂) = N₂
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₂) :
N ≤ lie_submodule.comap f (lie_submodule.map f N)
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 = ⊥) :
lie_submodule.comap f (lie_submodule.map f N) = N
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) :
lie_submodule.comap f ⁅I, N₂⁆ = ⁅I, lie_submodule.comap f N₂⁆
@[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) :
lie_submodule.map N.incl (lie_submodule.comap N.incl N') = N ⊓ N'
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} :
lie_ideal.map f ⁅I₁, I₂⁆ ≤ ⁅lie_ideal.map f I₁, lie_ideal.map f 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]
[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) :
lie_ideal.map f ⁅I₁, I₂⁆ = ⁅lie_ideal.map f I₁, lie_ideal.map f I₂⁆
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'} :
⁅lie_ideal.comap f J₁, lie_ideal.comap f J₂⁆ ≤ lie_ideal.comap f ⁅J₁, J₂⁆
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) :
lie_ideal.comap f ⁅f.ideal_range ⊓ J₁, f.ideal_range ⊓ J₂⁆ = ⁅lie_ideal.comap f J₁, lie_ideal.comap f 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]
[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) :
lie_ideal.map f ⁅lie_ideal.comap f J₁, lie_ideal.comap f 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]
[lie_algebra R L]
(I : lie_ideal R L)
{I₁ I₂ : lie_ideal R L} :
⁅lie_ideal.comap I.incl I₁, lie_ideal.comap I.incl I₂⁆ = lie_ideal.comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆
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) :
⁅lie_ideal.comap I.incl I₁, lie_ideal.comap I.incl I₂⁆ = lie_ideal.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.