Documentation

Mathlib.Algebra.Lie.IdealOperations

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

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] :

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 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) :
I, N = LieSubmodule.lieSpan R L {m : M | ∃ (x : I) (n : N), x, n = m}
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) :
I, N = Submodule.span R {m : M | ∃ (x : I) (n : N), x, n = 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] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (I : LieIdeal R L) :
I, N = Submodule.span R {m : M | xI, nN, x, n = m}
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) :
I, N N' xI, mN, x, m N'
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) :
x, m I, 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_comm {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (J : LieIdeal R L) :
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) :
theorem LieSubmodule.lie_le_left {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (J : LieIdeal R L) :
theorem LieSubmodule.lie_le_inf {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (J : LieIdeal R L) :
I, J I J
@[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) :
I, N = xI, mN, x, m = 0
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) :
@[simp]
theorem LieSubmodule.sup_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) (J : 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.inf_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) (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] [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₂) :
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 = ) :
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₁ : f.ker = ) (hf₂ : N₂ f.range) :
@[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 N.incl (LieSubmodule.comap N.incl 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} :

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) :
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'} :
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 I₁.incl (LieIdeal.comap I₁.incl 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 : f.IsIdealMorphism) :
LieIdeal.comap f f.idealRange J₁, f.idealRange J₂ = LieIdeal.comap f J₁, LieIdeal.comap f J₂ f.ker
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 : f.IsIdealMorphism) :
LieIdeal.map f LieIdeal.comap f J₁, LieIdeal.comap f J₂ = f.idealRange J₁, f.idealRange 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 I.incl I₁, LieIdeal.comap I.incl I₂ = LieIdeal.comap I.incl 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 I.incl I₁, LieIdeal.comap I.incl I₂ = LieIdeal.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.