Lie algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
Instances of this typeclass
- lie_ring.of_associative_ring
- lie_subalgebra.lie_ring
- lie_ideal.lie_ring
- derivation.lie_ring
- left_invariant_derivation.lie_ring
- lie_submodule.quotient.lie_quotient_lie_ring
- lie_algebra.commutator_ring.lie_ring
- free_lie_algebra.lie_ring
- matrix.to_lie_algebra.lie_ring
- direct_sum.lie_ring
- direct_sum.lie_ring_of_ideals
- lie_algebra.extend_scalars.tensor_product.lie_ring
- lie_algebra.restrict_scalars.restrict_scalars.lie_ring
Instances of other typeclasses for lie_ring
- lie_ring.has_sizeof_inst
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.
Instances of this typeclass
- lie_algebra.of_associative_algebra
- lie_ring.int_lie_algebra
- lie_subalgebra.lie_algebra
- lie_ideal.lie_algebra
- derivation.lie_algebra
- left_invariant_derivation.lie_algebra
- lie_submodule.quotient.lie_quotient_lie_algebra
- lie_algebra.commutator_ring.lie_algebra
- free_lie_algebra.lie_algebra
- matrix.to_lie_algebra.lie_algebra
- direct_sum.lie_algebra
- direct_sum.lie_algebra_of_ideals
- lie_algebra.extend_scalars.lie_algebra
- lie_algebra.restrict_scalars.lie_algebra
Instances of other typeclasses for lie_algebra
- lie_algebra.has_sizeof_inst
- 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
.)
Instances of this typeclass
Instances of other typeclasses for lie_ring_module
- lie_ring_module.has_sizeof_inst
- 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.
Instances of this typeclass
Instances of other typeclasses for lie_module
- lie_module.has_sizeof_inst
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 := _}
Equations
Equations
- linear_map.lie_module = {smul_lie := _, lie_smul := _}
- to_linear_map : L →ₗ[R] L'
- map_lie' : ∀ {x y : L}, self.to_linear_map.to_fun ⁅x, y⁆ = ⁅self.to_linear_map.to_fun x, self.to_linear_map.to_fun y⁆
A morphism of Lie algebras is a linear map respecting the bracket operations.
Instances for lie_hom
Equations
- lie_hom.linear_map.has_coe = {coe := lie_hom.to_linear_map _inst_5}
Equations
- lie_hom.has_coe_to_fun = {coe := λ (f : L₁ →ₗ⁅R⁆ L₂), f.to_linear_map.to_fun}
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
The identity map is a morphism of Lie algebras.
Equations
- lie_hom.id = {to_linear_map := {to_fun := linear_map.id.to_fun, map_add' := _, map_smul' := _}, map_lie' := _}
The constant 0 map is a Lie algebra morphism.
The identity map is a Lie algebra morphism.
Equations
- lie_hom.has_one = {one := lie_hom.id _inst_3}
Equations
- lie_hom.inhabited = {default := 0}
The composition of morphisms is a morphism.
Equations
- f.comp g = {to_linear_map := {to_fun := (f.to_linear_map.comp g.to_linear_map).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}
The inverse of a bijective morphism is a morphism.
A Lie ring module may be pulled back along a morphism of Lie algebras.
See note [reducible non-instances].
Equations
- lie_ring_module.comp_lie_hom M f = {to_has_bracket := {bracket := λ (x : L₁) (m : M), ⁅⇑f x, m⁆}, add_lie := _, lie_add := _, leibniz_lie := _}
A Lie module may be pulled back along a morphism of Lie algebras.
See note [reducible non-instances].
Equations
- lie_module.comp_lie_hom M f = {smul_lie := _, lie_smul := _}
- to_lie_hom : L →ₗ⁅R⁆ L'
- inv_fun : L' → L
- left_inv : function.left_inverse self.inv_fun self.to_lie_hom.to_linear_map.to_fun
- right_inv : function.right_inverse self.inv_fun self.to_lie_hom.to_linear_map.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.
Instances for lie_equiv
Consider an equivalence of Lie algebras as a linear equivalence.
Equations
- f.to_linear_equiv = {to_fun := f.to_lie_hom.to_linear_map.to_fun, map_add' := _, map_smul' := _, inv_fun := f.inv_fun, left_inv := _, right_inv := _}
Equations
- lie_equiv.has_coe_to_lie_hom = {coe := lie_equiv.to_lie_hom _inst_6}
Equations
Equations
- lie_equiv.has_coe_to_fun = {coe := λ (e : L₁ ≃ₗ⁅R⁆ L₂), e.to_lie_hom.to_linear_map.to_fun}
Equations
- lie_equiv.inhabited = {default := 1}
Lie algebra equivalences are reflexive.
Equations
Lie algebra equivalences are symmetric.
Equations
- e.symm = {to_lie_hom := {to_linear_map := (e.to_lie_hom.inverse e.inv_fun _ _).to_linear_map, map_lie' := _}, inv_fun := e.to_linear_equiv.symm.inv_fun, left_inv := _, right_inv := _}
Lie algebra equivalences are transitive.
Equations
- e₁.trans e₂ = {to_lie_hom := {to_linear_map := (e₂.to_lie_hom.comp e₁.to_lie_hom).to_linear_map, map_lie' := _}, inv_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).inv_fun, left_inv := _, right_inv := _}
A bijective morphism of Lie algebras yields an equivalence of Lie algebras.
Equations
- lie_equiv.of_bijective f h = {to_lie_hom := {to_linear_map := {to_fun := ⇑f, map_add' := _, map_smul' := _}, map_lie' := _}, inv_fun := (linear_equiv.of_bijective ↑f h).inv_fun, left_inv := _, right_inv := _}
- to_linear_map : M →ₗ[R] N
- map_lie' : ∀ {x : L} {m : M}, self.to_linear_map.to_fun ⁅x, m⁆ = ⁅x, self.to_linear_map.to_fun m⁆
A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie algebra.
Instances for lie_module_hom
- lie_module_hom.has_sizeof_inst
- lie_module_hom.linear_map.has_coe
- lie_module_hom.has_coe_to_fun
- lie_module_hom.has_zero
- lie_module_hom.has_one
- lie_module_hom.inhabited
- lie_module_hom.has_add
- lie_module_hom.has_sub
- lie_module_hom.has_neg
- lie_module_hom.has_nsmul
- lie_module_hom.has_zsmul
- lie_module_hom.add_comm_group
- lie_module_hom.has_smul
- lie_module_hom.module
- lie_module_equiv.has_coe_to_lie_module_hom
Equations
Equations
- lie_module_hom.has_coe_to_fun = {coe := λ (f : M →ₗ⁅R,L⁆ N), f.to_linear_map.to_fun}
The identity map is a morphism of Lie modules.
Equations
- lie_module_hom.id = {to_linear_map := {to_fun := linear_map.id.to_fun, map_add' := _, map_smul' := _}, map_lie' := _}
The constant 0 map is a Lie module morphism.
The identity map is a Lie module morphism.
Equations
- lie_module_hom.has_one = {one := lie_module_hom.id _inst_13}
Equations
The composition of Lie module morphisms is a morphism.
Equations
- f.comp g = {to_linear_map := {to_fun := (f.to_linear_map.comp g.to_linear_map).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}
The inverse of a bijective morphism of Lie modules is a morphism of Lie modules.
Equations
- lie_module_hom.add_comm_group = function.injective.add_comm_group coe_fn lie_module_hom.coe_injective lie_module_hom.coe_zero lie_module_hom.coe_add lie_module_hom.coe_neg lie_module_hom.coe_sub lie_module_hom.add_comm_group._proof_1 lie_module_hom.add_comm_group._proof_2
Equations
- lie_module_hom.module = function.injective.module R {to_fun := λ (f : M →ₗ⁅R,L⁆ N), f.to_linear_map.to_fun, map_zero' := _, map_add' := _} lie_module_hom.coe_injective lie_module_hom.coe_smul
- to_lie_module_hom : M →ₗ⁅R,L⁆ N
- inv_fun : N → M
- left_inv : function.left_inverse self.inv_fun self.to_lie_module_hom.to_linear_map.to_fun
- right_inv : function.right_inverse self.inv_fun self.to_lie_module_hom.to_linear_map.to_fun
An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of Lie algebra modules.
Instances for lie_module_equiv
View an equivalence of Lie modules as a linear equivalence.
Equations
- e.to_linear_equiv = {to_fun := e.to_lie_module_hom.to_linear_map.to_fun, map_add' := _, map_smul' := _, inv_fun := e.inv_fun, left_inv := _, right_inv := _}
View an equivalence of Lie modules as a type level equivalence.
Equations
- lie_module_equiv.has_coe_to_equiv = {coe := lie_module_equiv.to_equiv _inst_14}
Equations
Equations
Equations
- lie_module_equiv.has_coe_to_fun = {coe := λ (e : M ≃ₗ⁅R,L⁆ N), e.to_lie_module_hom.to_linear_map.to_fun}
Equations
Lie module equivalences are reflexive.
Equations
Lie module equivalences are syemmtric.
Equations
- e.symm = {to_lie_module_hom := {to_linear_map := (e.to_lie_module_hom.inverse e.inv_fun _ _).to_linear_map, map_lie' := _}, inv_fun := ↑e.symm.inv_fun, left_inv := _, right_inv := _}
Lie module equivalences are transitive.
Equations
- e₁.trans e₂ = {to_lie_module_hom := {to_linear_map := (e₂.to_lie_module_hom.comp e₁.to_lie_module_hom).to_linear_map, map_lie' := _}, inv_fun := (e₁.to_linear_equiv.trans e₂.to_linear_equiv).inv_fun, left_inv := _, right_inv := _}