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
instance
LieSubmodule.hasBracket
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
:
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 {m : M | ∃ (x : ↥I) (n : ↥N), ⁅↑x, ↑n⁆ = m} }
theorem
LieSubmodule.lieIdeal_oper_eq_span
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
(I : LieIdeal R L)
:
theorem
LieSubmodule.lieIdeal_oper_eq_linear_span
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
(I : LieIdeal R L)
:
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]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
(N : LieSubmodule R L M)
(I : LieIdeal R L)
:
theorem
LieSubmodule.lie_le_iff
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
(N' : LieSubmodule R L M)
(I : LieIdeal R L)
:
theorem
LieSubmodule.lie_coe_mem_lie
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
(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]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
(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]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
(I : LieIdeal R L)
:
@[simp]
theorem
LieSubmodule.lie_bot
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(I : LieIdeal R L)
:
@[simp]
theorem
LieSubmodule.bot_lie
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
:
theorem
LieSubmodule.lie_eq_bot_iff
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
(I : LieIdeal R L)
:
theorem
LieSubmodule.mono_lie
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L 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}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L 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}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L 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}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
(N' : LieSubmodule R L M)
(I : LieIdeal R L)
:
theorem
LieSubmodule.lie_inf
{R : Type u}
{L : Type v}
{M : Type w}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
(N : LieSubmodule R L M)
(N' : LieSubmodule R L M)
(I : LieIdeal R L)
:
theorem
LieSubmodule.map_bracket_eq
{R : Type u}
{L : Type v}
{M : Type w}
{M₂ : Type w₁}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
[LieModule R L M₂]
(N : LieSubmodule R L M)
(I : LieIdeal R L)
(f : M →ₗ⁅R,L⁆ M₂)
:
LieSubmodule.map f ⁅I, N⁆ = ⁅I, LieSubmodule.map f N⁆
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₂)
:
LieSubmodule.map f (LieSubmodule.comap f N₂) ≤ N₂
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₂ ≤ LieModuleHom.range f)
:
LieSubmodule.map f (LieSubmodule.comap f N₂) = N₂
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₂)
:
N ≤ LieSubmodule.comap f (LieSubmodule.map f N)
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 : LieModuleHom.ker f = ⊥)
:
LieSubmodule.comap f (LieSubmodule.map f N) = N
theorem
LieSubmodule.comap_bracket_eq
{R : Type u}
{L : Type v}
{M : Type w}
{M₂ : Type w₁}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[AddCommGroup M₂]
[Module R M₂]
[LieRingModule L M₂]
[LieModule R L M₂]
(I : LieIdeal R L)
(N₂ : LieSubmodule R L M₂)
(f : M →ₗ⁅R,L⁆ M₂)
(hf₁ : LieModuleHom.ker f = ⊥)
(hf₂ : N₂ ≤ LieModuleHom.range f)
:
LieSubmodule.comap f ⁅I, N₂⁆ = ⁅I, LieSubmodule.comap f N₂⁆
@[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 : LieSubmodule R L M)
(N' : LieSubmodule R L M)
:
LieSubmodule.map (LieSubmodule.incl N) (LieSubmodule.comap (LieSubmodule.incl N) N') = N ⊓ N'
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₁ : LieIdeal R L}
{I₂ : LieIdeal R L}
:
LieIdeal.map f ⁅I₁, I₂⁆ ≤ ⁅LieIdeal.map f I₁, LieIdeal.map f I₂⁆
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₂}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
[LieRing L']
[LieAlgebra R L']
(f : L →ₗ⁅R⁆ L')
{I₁ : LieIdeal R L}
{I₂ : LieIdeal R L}
(h : Function.Surjective ⇑f)
:
LieIdeal.map f ⁅I₁, I₂⁆ = ⁅LieIdeal.map f I₁, LieIdeal.map f I₂⁆
theorem
LieIdeal.comap_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')
{J₁ : LieIdeal R L'}
{J₂ : LieIdeal R L'}
:
⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ ≤ LieIdeal.comap f ⁅J₁, J₂⁆
theorem
LieIdeal.map_comap_incl
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{I₁ : LieIdeal R L}
{I₂ : LieIdeal R L}
:
LieIdeal.map (LieIdeal.incl I₁) (LieIdeal.comap (LieIdeal.incl I₁) I₂) = I₁ ⊓ I₂
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₁ : LieIdeal R L'}
{J₂ : LieIdeal R L'}
(h : LieHom.IsIdealMorphism f)
:
LieIdeal.comap f ⁅LieHom.idealRange f ⊓ J₁, LieHom.idealRange f ⊓ J₂⁆ = ⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ ⊔ LieHom.ker f
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₁ : LieIdeal R L'}
{J₂ : LieIdeal R L'}
(h : LieHom.IsIdealMorphism f)
:
LieIdeal.map f ⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ = ⁅LieHom.idealRange f ⊓ J₁, LieHom.idealRange f ⊓ J₂⁆
theorem
LieIdeal.comap_bracket_incl
{R : Type u}
{L : Type v}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(I : LieIdeal R L)
{I₁ : LieIdeal R L}
{I₂ : LieIdeal R L}
:
⁅LieIdeal.comap (LieIdeal.incl I) I₁, LieIdeal.comap (LieIdeal.incl I) I₂⁆ = LieIdeal.comap (LieIdeal.incl I) ⁅I ⊓ I₁, I ⊓ I₂⁆
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₁ : LieIdeal R L}
{I₂ : LieIdeal R L}
(h₁ : I₁ ≤ I)
(h₂ : I₂ ≤ I)
:
⁅LieIdeal.comap (LieIdeal.incl I) I₁, LieIdeal.comap (LieIdeal.incl I) I₂⁆ = LieIdeal.comap (LieIdeal.incl 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.