Lie algebras #
This file defines Lie rings and Lie algebras over a commutative ring together with their modules, morphisms and equivalences, as well as various lemmas to make these definitions usable.
Main definitions #
Notation #
Working over a fixed commutative ring R
, we introduce the notations:
L →ₗ⁅R⁆ L'
for a morphism of Lie algebras,L ≃ₗ⁅R⁆ L'
for an equivalence of Lie algebras,M →ₗ⁅R,L⁆ N
for a morphism of Lie algebra modulesM
,N
over a Lie algebraL
,M ≃ₗ⁅R,L⁆ N
for an equivalence of Lie algebra modulesM
,N
over a Lie algebraL
.
Implementation notes #
Lie algebras are defined as modules with a compatible Lie ring structure and thus, like modules, are partially unbundled.
References #
Tags #
lie bracket, jacobi identity, lie ring, lie algebra, lie module
- to_add_comm_group : add_comm_group L
- to_has_bracket : has_bracket L L
- add_lie : ∀ (x y z : L), ⁅x + y,z⁆ = ⁅x,z⁆ + ⁅y,z⁆
- lie_add : ∀ (x y z : L), ⁅x,y + z⁆ = ⁅x,y⁆ + ⁅x,z⁆
- lie_self : ∀ (x : L), ⁅x,x⁆ = 0
- leibniz_lie : ∀ (x y z : L), ⁅x,⁅y,z⁆⁆ = ⁅⁅x,y⁆,z⁆ + ⁅y,⁅x,z⁆⁆
A Lie ring is an additive group with compatible product, known as the bracket, satisfying the Jacobi identity. The bracket is not associative unless it is identically zero.
A Lie algebra is a module with compatible product, known as the bracket, satisfying the Jacobi identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring.
- to_has_bracket : has_bracket L M
- add_lie : ∀ (x y : L) (m : M), ⁅x + y,m⁆ = ⁅x,m⁆ + ⁅y,m⁆
- lie_add : ∀ (x : L) (m n : M), ⁅x,m + n⁆ = ⁅x,m⁆ + ⁅x,n⁆
- leibniz_lie : ∀ (x y : L) (m : M), ⁅x,⁅y,m⁆⁆ = ⁅⁅x,y⁆,m⁆ + ⁅y,⁅x,m⁆⁆
A Lie ring module is an additive group, together with an additive action of a
Lie ring on this group, such that the Lie bracket acts as the commutator of endomorphisms.
(For representations of Lie algebras see lie_module
.)
- smul_lie : ∀ (t : R) (x : L) (m : M), ⁅t • x,m⁆ = t • ⁅x,m⁆
- lie_smul : ∀ (t : R) (x : L) (m : M), ⁅x,t • m⁆ = t • ⁅x,m⁆
A Lie module is a module over a commutative ring, together with a linear action of a Lie algebra on this module, such that the Lie bracket acts as the commutator of endomorphisms.
Equations
- lie_ring_self_module = {to_has_bracket := lie_ring.to_has_bracket infer_instance, add_lie := _, lie_add := _, leibniz_lie := _}
Every Lie algebra is a module over itself.
Equations
- lie_algebra_self_module = {smul_lie := _, lie_smul := _}
- to_fun : L → L'
- map_add' : ∀ (x y : L), c.to_fun (x + y) = c.to_fun x + c.to_fun y
- map_smul' : ∀ (m : R) (x : L), c.to_fun (m • x) = m • c.to_fun x
- map_lie' : ∀ {x y : L}, c.to_fun ⁅x,y⁆ = ⁅c.to_fun x,c.to_fun y⁆
A morphism of Lie algebras is a linear map respecting the bracket operations.
Equations
- lie_hom.linear_map.has_coe = {coe := lie_hom.to_linear_map _inst_6}
Equations
- lie_hom.has_coe_to_fun = {F := λ (x : L₁ →ₗ⁅R⁆ L₂), L₁ → L₂, coe := lie_hom.to_fun _inst_6}
The constant 0 map is a Lie algebra morphism.
Equations
- lie_hom.inhabited = {default := 0}
The composition of morphisms is a morphism.
The inverse of a bijective morphism is a morphism.
- to_fun : L → L'
- map_add' : ∀ (x y : L), c.to_fun (x + y) = c.to_fun x + c.to_fun y
- map_smul' : ∀ (m : R) (x : L), c.to_fun (m • x) = m • c.to_fun x
- map_lie' : ∀ {x y : L}, c.to_fun ⁅x,y⁆ = ⁅c.to_fun x,c.to_fun y⁆
- inv_fun : L' → L
- left_inv : function.left_inverse c.inv_fun c.to_fun
- right_inv : function.right_inverse c.inv_fun c.to_fun
An equivalence of Lie algebras is a morphism which is also a linear equivalence. We could
instead define an equivalence to be a morphism which is also a (plain) equivalence. However it is
more convenient to define via linear equivalence to get .to_linear_equiv
for free.
Equations
- lie_equiv.has_coe_to_lie_hom = {coe := lie_equiv.to_lie_hom _inst_6}
Equations
Equations
- lie_equiv.has_coe_to_fun = {F := λ (x : L₁ ≃ₗ⁅R⁆ L₂), L₁ → L₂, coe := lie_equiv.to_fun _inst_6}
Equations
- lie_equiv.inhabited = {default := 1}
Lie algebra equivalences are reflexive.
Equations
Lie algebra equivalences are symmetric.
Lie algebra equivalences are transitive.
Equations
- e₁.trans e₂ = {to_fun := (e₂.to_lie_hom.comp e₁.to_lie_hom).to_fun, map_add' := _, map_smul' := _, map_lie' := _, inv_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).inv_fun, left_inv := _, right_inv := _}
- to_fun : M → N
- map_add' : ∀ (x y : M), c.to_fun (x + y) = c.to_fun x + c.to_fun y
- map_smul' : ∀ (m : R) (x : M), c.to_fun (m • x) = m • c.to_fun x
- map_lie' : ∀ {x : L} {m : M}, c.to_fun ⁅x,m⁆ = ⁅x,c.to_fun m⁆
A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie algebra.
Equations
Equations
- lie_module_hom.has_coe_to_fun = {F := λ (x : M →ₗ⁅R,L⁆ N), M → N, coe := lie_module_hom.to_fun _inst_14}
The constant 0 map is a Lie module morphism.
The identity map is a Lie module morphism.
Equations
The composition of Lie module morphisms is a morphism.
The inverse of a bijective morphism of Lie modules is a morphism of Lie modules.
- to_fun : M → N
- map_add' : ∀ (x y : M), c.to_fun (x + y) = c.to_fun x + c.to_fun y
- map_smul' : ∀ (m : R) (x : M), c.to_fun (m • x) = m • c.to_fun x
- inv_fun : N → M
- left_inv : function.left_inverse c.inv_fun c.to_fun
- right_inv : function.right_inverse c.inv_fun c.to_fun
- map_lie' : ∀ {x : L} {m : M}, c.to_fun ⁅x,m⁆ = ⁅x,c.to_fun m⁆
An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of Lie algebra modules.
Equations
Equations
Equations
- lie_module_equiv.has_coe_to_fun = {F := λ (x : M ≃ₗ⁅R,L⁆ N), M → N, coe := lie_module_equiv.to_fun _inst_14}
Equations
Lie module equivalences are reflexive.
Equations
Lie module equivalences are syemmtric.
Lie module equivalences are transitive.
Equations
- e₁.trans e₂ = {to_fun := (e₂.to_lie_module_hom.comp e₁.to_lie_module_hom).to_fun, map_add' := _, map_smul' := _, inv_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).inv_fun, left_inv := _, right_inv := _, map_lie' := _}