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.hasBracketLieSubmodule.lieIdeal_oper_eq_linear_spanLieIdeal.map_bracket_leLieIdeal.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
theorem
LieSubmodule.map_comap_le
{R : Type u}
{L : Type v}
{M : Type w}
{M₂ : Type w₁}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
(N₂ : LieSubmodule R L M₂)
(f : M →ₗ⁅R,L⁆ M₂)
:
theorem
LieSubmodule.map_comap_eq
{R : Type u}
{L : Type v}
{M : Type w}
{M₂ : Type w₁}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
(N₂ : LieSubmodule R L M₂)
(f : M →ₗ⁅R,L⁆ M₂)
(hf : N₂ ≤ f.range)
:
theorem
LieSubmodule.le_comap_map
{R : Type u}
{L : Type v}
{M : Type w}
{M₂ : Type w₁}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
(N : LieSubmodule R L M)
(f : M →ₗ⁅R,L⁆ M₂)
:
theorem
LieSubmodule.comap_map_eq
{R : Type u}
{L : Type v}
{M : Type w}
{M₂ : Type w₁}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
(N : LieSubmodule R L M)
(f : M →ₗ⁅R,L⁆ M₂)
(hf : f.ker = ⊥)
:
@[simp]
theorem
LieSubmodule.map_comap_incl
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N N' : LieSubmodule R L M)
:
@[instance_reducible]
instance
LieSubmodule.hasBracket
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieAlgebra R L]
:
Bracket (LieIdeal R L) (LieSubmodule 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
- LieSubmodule.hasBracket = { bracket := fun (I : LieIdeal R L) (N : LieSubmodule R L M) => LieSubmodule.lieSpan R L {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅↑x_1, ↑n⁆ = x} }
theorem
LieSubmodule.lieIdeal_oper_eq_linear_span
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
[LieAlgebra R L]
(I : LieIdeal R L)
[LieModule R L 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}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
[LieAlgebra R L]
(I : LieIdeal R L)
[LieModule R L M]
:
theorem
LieSubmodule.lie_le_iff
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N N' : LieSubmodule R L M)
[LieAlgebra R L]
(I : LieIdeal R L)
:
theorem
LieSubmodule.lie_coe_mem_lie
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N : LieSubmodule R L M}
[LieAlgebra R L]
{I : LieIdeal R L}
(x : ↥I)
(m : ↥N)
:
theorem
LieSubmodule.lie_mem_lie
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N : LieSubmodule R L M}
[LieAlgebra R L]
{I : LieIdeal R L}
{x : L}
{m : M}
(hx : x ∈ I)
(hm : m ∈ N)
:
theorem
LieSubmodule.lie_le_right
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
[LieAlgebra R L]
(I : LieIdeal R L)
:
@[simp]
theorem
LieSubmodule.lie_bot
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieAlgebra R L]
(I : LieIdeal R L)
:
@[simp]
theorem
LieSubmodule.bot_lie
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
[LieAlgebra R L]
:
theorem
LieSubmodule.lie_eq_bot_iff
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
[LieAlgebra R L]
(I : LieIdeal R L)
:
theorem
LieSubmodule.mono_lie
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N N' : LieSubmodule R L M}
[LieAlgebra R L]
{I J : LieIdeal R L}
(h₁ : I ≤ J)
(h₂ : N ≤ N')
:
theorem
LieSubmodule.mono_lie_left
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
[LieAlgebra R L]
{I J : LieIdeal R L}
(h : I ≤ J)
:
theorem
LieSubmodule.mono_lie_right
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
{N N' : LieSubmodule R L M}
[LieAlgebra R L]
(I : LieIdeal R L)
(h : N ≤ N')
:
@[simp]
theorem
LieSubmodule.lie_sup
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N N' : LieSubmodule R L M)
[LieAlgebra R L]
(I : LieIdeal R L)
:
@[simp]
theorem
LieSubmodule.sup_lie
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
[LieAlgebra R L]
(I J : LieIdeal R L)
:
theorem
LieSubmodule.lie_inf
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N N' : LieSubmodule R L M)
[LieAlgebra R L]
(I : LieIdeal R L)
:
theorem
LieSubmodule.inf_lie
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
[LieAlgebra R L]
(I J : LieIdeal R L)
:
theorem
LieSubmodule.map_bracket_eq
{R : Type u}
{L : Type v}
{M : Type w}
{M₂ : Type w₁}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
(N : LieSubmodule R L M)
(f : M →ₗ⁅R,L⁆ M₂)
[LieAlgebra R L]
[LieModule R L M₂]
(I : LieIdeal R L)
[LieModule R L M]
:
theorem
LieSubmodule.comap_bracket_eq
{R : Type u}
{L : Type v}
{M : Type w}
{M₂ : Type w₁}
[CommRing R]
[LieRing L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
(N₂ : LieSubmodule R L M₂)
(f : M →ₗ⁅R,L⁆ M₂)
[LieAlgebra R L]
[LieModule R L M₂]
(I : LieIdeal R L)
[LieModule R L M]
(hf₁ : f.ker = ⊥)
(hf₂ : N₂ ≤ f.range)
:
theorem
LieIdeal.map_bracket_le
{R : Type u}
{L : Type v}
{L' : Type w₂}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieRing L']
[LieAlgebra R L']
(f : L →ₗ⁅R⁆ L')
{I₁ 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.comap_bracket_eq
{R : Type u}
{L : Type v}
{L' : Type w₂}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieRing L']
[LieAlgebra R L']
{f : L →ₗ⁅R⁆ L'}
{J₁ J₂ : LieIdeal R L'}
(h : f.IsIdealMorphism)
:
theorem
LieIdeal.map_comap_bracket_eq
{R : Type u}
{L : Type v}
{L' : Type w₂}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieRing L']
[LieAlgebra R L']
{f : L →ₗ⁅R⁆ L'}
{J₁ J₂ : LieIdeal R L'}
(h : f.IsIdealMorphism)
:
theorem
LieIdeal.comap_bracket_incl_of_le
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(I : LieIdeal R L)
{I₁ 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.