# Trivial Lie modules and Abelian Lie algebras #

The action of a Lie algebra L on a module M is trivial if ⁅x, m⁆ = 0 for all x ∈ L and m ∈ M. In the special case that M = L with the adjoint action, triviality corresponds to the concept of an Abelian Lie algebra.

In this file we define these concepts and provide some related definitions and results.

## Main definitions #

• LieModule.IsTrivial
• IsLieAbelian
• commutative_ring_iff_abelian_lie_ring
• LieModule.ker
• LieModule.maxTrivSubmodule
• LieAlgebra.center

## Tags #

lie algebra, abelian, commutative, center

class LieModule.IsTrivial (L : Type v) (M : Type w) [Bracket L M] [Zero M] :

A Lie (ring) module is trivial iff all brackets vanish.

• trivial : ∀ (x : L) (m : M), x, m = 0
Instances
theorem LieModule.IsTrivial.trivial {L : Type v} {M : Type w} [Bracket L M] [Zero M] [self : ] (x : L) (m : M) :
x, m = 0
@[simp]
theorem trivial_lie_zero (L : Type v) (M : Type w) [Bracket L M] [Zero M] [] (x : L) (m : M) :
x, m = 0
instance LieModule.instIsTrivialOfSubsingleton {L : Type u_1} {M : Type u_2} [] [] [] [] :
Equations
• =
instance LieModule.instIsTrivialOfSubsingleton' {L : Type u_1} {M : Type u_2} [] [] [] [] :
Equations
• =
@[reducible, inline]
abbrev IsLieAbelian (L : Type v) [Bracket L L] [Zero L] :

A Lie algebra is Abelian iff it is trivial as a Lie module over itself.

Equations
Instances For
instance LieIdeal.isLieAbelian_of_trivial (R : Type u) (L : Type v) [] [] [] (I : LieIdeal R L) [h : ] :
IsLieAbelian I
Equations
• =
theorem Function.Injective.isLieAbelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R L₂} (h₁ : ) :
theorem Function.Surjective.isLieAbelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R L₂} (h₁ : ) (h₂ : ) :
theorem lie_abelian_iff_equiv_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R L₂) :
theorem commutative_ring_iff_abelian_lie_ring {A : Type v} [Ring A] :
(Std.Commutative fun (x x_1 : A) => x * x_1)
def LieModule.ker (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] :

The kernel of the action of a Lie algebra L on a Lie module M as a Lie ideal in L.

Equations
• = ().ker
Instances For
@[simp]
theorem LieModule.mem_ker (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) :
x ∀ (m : M), x, m = 0
def LieModule.maxTrivSubmodule (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] :

The largest submodule of a Lie module M on which the Lie algebra L acts trivially.

Equations
• = { carrier := {m : M | ∀ (x : L), x, m = 0}, add_mem' := , zero_mem' := , smul_mem' := , lie_mem := }
Instances For
@[simp]
theorem LieModule.mem_maxTrivSubmodule (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (m : M) :
m ∀ (x : L), x, m = 0
instance LieModule.instIsTrivialSubtypeMemSubmoduleMaxTrivSubmodule (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] :
Equations
• =
@[simp]
theorem LieModule.ideal_oper_maxTrivSubmodule_eq_bot (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (I : LieIdeal R L) :
theorem LieModule.le_max_triv_iff_bracket_eq_bot (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] {N : LieSubmodule R L M} :
theorem LieModule.trivial_iff_le_maximal_trivial (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] (N : LieSubmodule R L M) :
N
theorem LieModule.isTrivial_iff_max_triv_eq_top (R : Type u) (L : Type v) (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] :
def LieModule.maxTrivHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (f : M →ₗ⁅R,L N) :
() →ₗ⁅R,L ()

maxTrivSubmodule is functorial.

Equations
• = { toFun := fun (m : ()) => f m, , map_add' := , map_smul' := , map_lie' := }
Instances For
@[simp]
theorem LieModule.coe_maxTrivHom_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (f : M →ₗ⁅R,L N) (m : ()) :
( m) = f m
def LieModule.maxTrivEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (e : M ≃ₗ⁅R,L N) :
() ≃ₗ⁅R,L ()

The maximal trivial submodules of Lie-equivalent Lie modules are Lie-equivalent.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LieModule.coe_maxTrivEquiv_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (e : M ≃ₗ⁅R,L N) (m : ()) :
() = e m
@[simp]
theorem LieModule.maxTrivEquiv_of_refl_eq_refl {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] [LieModule R L M] :
LieModule.maxTrivEquiv LieModuleEquiv.refl = LieModuleEquiv.refl
@[simp]
theorem LieModule.maxTrivEquiv_of_equiv_symm_eq_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (e : M ≃ₗ⁅R,L N) :
def LieModule.maxTrivLinearMapEquivLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] :

A linear map between two Lie modules is a morphism of Lie modules iff the Lie algebra action on it is trivial.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LieModule.coe_maxTrivLinearMapEquivLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (f : (LieModule.maxTrivSubmodule R L (M →ₗ[R] N))) :
(LieModule.maxTrivLinearMapEquivLieModuleHom f) = f
@[simp]
theorem LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (f : M →ₗ⁅R,L N) :
(LieModule.maxTrivLinearMapEquivLieModuleHom.symm f) = f
@[simp]
theorem LieModule.coe_linearMap_maxTrivLinearMapEquivLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (f : (LieModule.maxTrivSubmodule R L (M →ₗ[R] N))) :
(LieModule.maxTrivLinearMapEquivLieModuleHom f) = f
@[simp]
theorem LieModule.coe_linearMap_maxTrivLinearMapEquivLieModuleHom_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [] [] [] [] [Module R M] [] [LieModule R L M] [] [Module R N] [] [LieModule R L N] (f : M →ₗ⁅R,L N) :
(LieModule.maxTrivLinearMapEquivLieModuleHom.symm f) = f
@[reducible, inline]
abbrev LieAlgebra.center (R : Type u) (L : Type v) [] [] [] :

The center of a Lie algebra is the set of elements that commute with everything. It can be viewed as the maximal trivial submodule of the Lie algebra as a Lie module over itself via the adjoint representation.

Equations
Instances For
Equations
• =
@[simp]
theorem LieAlgebra.ad_ker_eq_self_module_ker (R : Type u) (L : Type v) [] [] [] :
().ker =
@[simp]
theorem LieAlgebra.self_module_ker_eq_center (R : Type u) (L : Type v) [] [] [] :
=
theorem LieAlgebra.abelian_of_le_center (R : Type u) (L : Type v) [] [] [] (I : LieIdeal R L) (h : I ) :
IsLieAbelian I
theorem LieAlgebra.isLieAbelian_iff_center_eq_top (R : Type u) (L : Type v) [] [] [] :
theorem LieModule.commute_toEndomorphism_of_mem_center_left {R : Type u} {L : Type v} (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] {x : L} (hx : x ) (y : L) :
Commute (() x) (() y)
theorem LieModule.commute_toEndomorphism_of_mem_center_right {R : Type u} {L : Type v} (M : Type w) [] [] [] [] [Module R M] [] [LieModule R L M] {x : L} (hx : x ) (y : L) :
Commute (() y) (() x)
@[simp]
theorem LieSubmodule.trivial_lie_oper_zero {R : Type u} {L : Type v} {M : Type w} [] [] [] [] [Module R M] [] (N : LieSubmodule R L M) (I : LieIdeal R L) [] :
theorem LieSubmodule.lie_abelian_iff_lie_self_eq_bot {R : Type u} {L : Type v} [] [] [] (I : LieIdeal R L) :