# Documentation

Mathlib.Algebra.Lie.Abelian

# 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] :
• trivial : ∀ (x : L) (m : M), x, m = 0

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

Instances
@[simp]
theorem trivial_lie_zero (L : Type v) (M : Type w) [Bracket L M] [Zero M] [] (x : L) (m : M) :
x, m = 0
@[inline, reducible]
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.

Instances For
instance LieIdeal.isLieAbelian_of_trivial (R : Type u) (L : Type v) [] [] [] (I : LieIdeal R L) [h : LieModule.IsTrivial L { x // x I }] :
IsLieAbelian { x // x I }
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] :
(IsCommutative A fun x x_1 => x * x_1)
theorem LieAlgebra.isLieAbelian_bot (R : Type u) (L : Type v) [] [] [] :
IsLieAbelian { x // x }
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.

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.

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
@[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) :
LieModule.IsTrivial L { x // x N } 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) :
{ x // x ↑() } →ₗ⁅R,L { x // x ↑() }

maxTrivSubmodule is functorial.

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 : { x // x }) :
↑(↑() 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) :
{ x // x ↑() } ≃ₗ⁅R,L { x // x ↑() }

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

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 : { x // x }) :
↑(↑() 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.

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 : { x // x 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) :
↑(↑(LinearEquiv.symm LieModule.maxTrivLinearMapEquivLieModuleHom) 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 : { x // x 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) :
↑(↑(LinearEquiv.symm LieModule.maxTrivLinearMapEquivLieModuleHom) f) = f
@[inline, reducible]
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.

Instances For
@[simp]
theorem LieAlgebra.ad_ker_eq_self_module_ker (R : Type u) (L : Type v) [] [] [] :
@[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 { x // x I }
theorem LieAlgebra.isLieAbelian_iff_center_eq_top (R : Type u) (L : Type v) [] [] [] :
@[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) :
IsLieAbelian { x // x I } I, I =