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 #
Tagsc #
lie bracket, jacobi identity, lie ring, lie algebra, lie module
- add : L → L → L
- zero : L
- nsmul : ℕ → L → L
- nsmul_zero : ∀ (x : L), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : L), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
- neg : L → L
- sub : L → L → L
- zsmul : ℤ → L → L
- zsmul_zero' : ∀ (a : L), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : L), SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
- zsmul_neg' : ∀ (n : ℕ) (a : L), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
- bracket : L → L → L
A Lie ring bracket is additive in its first component.
A Lie ring bracket is additive in its second component.
A Lie ring bracket vanishes on the diagonal in L × L.
A Lie ring bracket satisfies a Leibniz / Jacobi identity.
A Lie ring is an additive group with compatible product, known as the bracket, satisfying the Jacobi identity.
Instances
- smul : R → L → L
A Lie algebra bracket is compatible with scalar multiplication in its second argument.
The compatibility in the first argument is not a class property, but follows since every Lie algebra has a natural Lie module action on itself, see
LieModule
.
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
- bracket : L → M → M
A Lie ring module bracket is additive in its first component.
A Lie ring module bracket is additive in its second component.
A Lie ring module bracket satisfies a Leibniz / Jacobi identity.
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 LieModule
.)
Instances
A Lie module bracket is compatible with scalar multiplication in its first argument.
A Lie module bracket is compatible with scalar multiplication in its second argument.
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
Every Lie algebra is a module over itself.
- toFun : L → L'
- map_add' : ∀ (x y : L), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
- map_smul' : ∀ (r : R) (x : L), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
- map_lie' : ∀ {x y : L}, AddHom.toFun s.toAddHom ⁅x, y⁆ = ⁅AddHom.toFun s.toAddHom x, AddHom.toFun s.toAddHom y⁆
A morphism of Lie algebras is compatible with brackets.
A morphism of Lie algebras is a linear map respecting the bracket operations.
Instances For
A morphism of Lie algebras is a linear map respecting the bracket operations.
Instances For
The constant 0 map is a Lie algebra morphism.
The identity map is a Lie algebra morphism.
The composition of morphisms is a morphism.
Instances For
The inverse of a bijective morphism is a morphism.
Instances For
A Lie ring module may be pulled back along a morphism of Lie algebras.
See note [reducible non-instances].
Instances For
A Lie module may be pulled back along a morphism of Lie algebras.
- toFun : L → L'
- map_add' : ∀ (x y : L), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
- map_smul' : ∀ (r : R) (x : L), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
- map_lie' : ∀ {x y : L}, AddHom.toFun s.toAddHom ⁅x, y⁆ = ⁅AddHom.toFun s.toAddHom x, AddHom.toFun s.toAddHom y⁆
- invFun : L' → L
The inverse function of an equivalence of Lie algebras
- left_inv : Function.LeftInverse s.invFun s.toFun
The inverse function of an equivalence of Lie algebras is a left inverse of the underlying function.
- right_inv : Function.RightInverse s.invFun s.toFun
The inverse function of an equivalence of Lie algebras is a right inverse of the underlying function.
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 .toLinearEquiv
for free.
Instances For
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 .toLinearEquiv
for free.
Instances For
Consider an equivalence of Lie algebras as a linear equivalence.
Instances For
Lie algebra equivalences are reflexive.
Instances For
Lie algebra equivalences are symmetric.
Instances For
Lie algebra equivalences are transitive.
Instances For
A bijective morphism of Lie algebras yields an equivalence of Lie algebras.
Instances For
- toFun : M → N
- map_add' : ∀ (x y : M), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
- map_smul' : ∀ (r : R) (x : M), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
- map_lie' : ∀ {x : L} {m : M}, AddHom.toFun s.toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun s.toAddHom m⁆
A module of Lie algebra modules is compatible with the action of the Lie algebra on the modules.
A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie algebra.
Instances For
A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie algebra.
Instances For
The identity map is a morphism of Lie modules.
Instances For
The constant 0 map is a Lie module morphism.
The identity map is a Lie module morphism.
The composition of Lie module morphisms is a morphism.
Instances For
The inverse of a bijective morphism of Lie modules is a morphism of Lie modules.
Instances For
- toFun : M → N
- map_add' : ∀ (x y : M), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
- map_smul' : ∀ (r : R) (x : M), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
- map_lie' : ∀ {x : L} {m : M}, AddHom.toFun s.toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun s.toAddHom m⁆
- invFun : N → M
The inverse function of an equivalence of Lie modules
- left_inv : Function.LeftInverse s.invFun s.toFun
The inverse function of an equivalence of Lie modules is a left inverse of the underlying function.
- right_inv : Function.RightInverse s.invFun s.toFun
The inverse function of an equivalence of Lie modules is a right inverse of the underlying function.
An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of Lie algebra modules.
Instances For
An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of Lie algebra modules.
Instances For
View an equivalence of Lie modules as a linear equivalence.
Instances For
View an equivalence of Lie modules as a type level equivalence.
Instances For
Lie module equivalences are reflexive.
Instances For
Lie module equivalences are symmetric.
Instances For
Lie module equivalences are transitive.