mathlib3documentation

algebra.lie.universal_enveloping

Universal enveloping algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given a commutative ring R and a Lie algebra L over R, we construct the universal enveloping algebra of L, together with its universal property.

Tags #

lie algebra, universal enveloping algebra, tensor algebra

inductive universal_enveloping_algebra.rel (R : Type u₁) (L : Type u₂) [comm_ring R] [lie_ring L] [ L] :
Prop

The quotient by the ideal generated by this relation is the universal enveloping algebra.

Note that we have avoided using the more natural expression: | lie_compat (x y : L) : rel (ιₜ ⁅x, y⁆) ⁅ιₜ x, ιₜ y⁆ so that our construction needs only the semiring structure of the tensor algebra.

def universal_enveloping_algebra (R : Type u₁) (L : Type u₂) [comm_ring R] [lie_ring L] [ L] :
Type (max u₁ u₂)

The universal enveloping algebra of a Lie algebra.

Equations
Instances for universal_enveloping_algebra
@[protected, instance]
def universal_enveloping_algebra.algebra (R : Type u₁) (L : Type u₂) [comm_ring R] [lie_ring L] [ L] :
@[protected, instance]
def universal_enveloping_algebra.ring (R : Type u₁) (L : Type u₂) [comm_ring R] [lie_ring L] [ L] :
@[protected, instance]
def universal_enveloping_algebra.inhabited (R : Type u₁) (L : Type u₂) [comm_ring R] [lie_ring L] [ L] :
def universal_enveloping_algebra.mk_alg_hom (R : Type u₁) (L : Type u₂) [comm_ring R] [lie_ring L] [ L] :

The quotient map from the tensor algebra to the universal enveloping algebra as a morphism of associative algebras.

Equations
def universal_enveloping_algebra.ι (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [ L] :

The natural Lie algebra morphism from a Lie algebra to its universal enveloping algebra.

Equations
def universal_enveloping_algebra.lift (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [ L] {A : Type u₃} [ring A] [ A] :

The universal property of the universal enveloping algebra: Lie algebra morphisms into associative algebras lift to associative algebra morphisms from the universal enveloping algebra.

Equations
@[simp]
theorem universal_enveloping_algebra.lift_symm_apply (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [ L] {A : Type u₃} [ring A] [ A] (F : →ₐ[R] A) :
@[simp]
theorem universal_enveloping_algebra.ι_comp_lift (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [ L] {A : Type u₃} [ring A] [ A] (f : L →ₗ⁅R A) :
@[simp]
theorem universal_enveloping_algebra.lift_ι_apply (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [ L] {A : Type u₃} [ring A] [ A] (f : L →ₗ⁅R A) (x : L) :
= f x
theorem universal_enveloping_algebra.lift_unique (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [ L] {A : Type u₃} [ring A] [ A] (f : L →ₗ⁅R A) (g : →ₐ[R] A) :
@[ext]
theorem universal_enveloping_algebra.hom_ext (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [ L] {A : Type u₃} [ring A] [ A] {g₁ g₂ : →ₐ[R] A} (h : = ) :
g₁ = g₂