# Documentation

Mathlib.Algebra.Lie.UniversalEnveloping

# Universal enveloping algebra #

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.

## Main definitions #

• UniversalEnvelopingAlgebra: the universal enveloping algebra, endowed with an R-algebra structure.
• UniversalEnvelopingAlgebra.ι: the Lie algebra morphism from L to its universal enveloping algebra.
• UniversalEnvelopingAlgebra.lift: given an associative algebra A, together with a Lie algebra morphism f : L →ₗ⁅R⁆ A, lift R L f : UniversalEnvelopingAlgebra R L →ₐ[R] A is the unique morphism of algebras through which f factors.
• UniversalEnvelopingAlgebra.ι_comp_lift: states that the lift of a morphism is indeed part of a factorisation.
• UniversalEnvelopingAlgebra.lift_unique: states that lifts of morphisms are indeed unique.
• UniversalEnvelopingAlgebra.hom_ext: a restatement of lift_unique as an extensionality lemma.

## Tags #

lie algebra, universal enveloping algebra, tensor algebra

inductive UniversalEnvelopingAlgebra.Rel (R : Type u₁) (L : Type u₂) [] [] [] :
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.

Instances For
def UniversalEnvelopingAlgebra (R : Type u₁) (L : Type u₂) [] [] [] :
Type (max u₁ u₂)

The universal enveloping algebra of a Lie algebra.

Instances For
instance UniversalEnvelopingAlgebra.instInhabited (R : Type u₁) (L : Type u₂) [] [] [] :
instance UniversalEnvelopingAlgebra.instRing (R : Type u₁) (L : Type u₂) [] [] [] :
instance UniversalEnvelopingAlgebra.instAlgebra (R : Type u₁) (L : Type u₂) [] [] [] :
def UniversalEnvelopingAlgebra.mkAlgHom (R : Type u₁) (L : Type u₂) [] [] [] :

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

Instances For
@[simp]
theorem UniversalEnvelopingAlgebra.ι_apply (R : Type u₁) {L : Type u₂} [] [] [] :
∀ (a : L), = ↑() (↑() a)
def UniversalEnvelopingAlgebra.ι (R : Type u₁) {L : Type u₂} [] [] [] :

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

Instances For
def UniversalEnvelopingAlgebra.lift (R : Type u₁) {L : Type u₂} [] [] [] {A : Type u₃} [Ring A] [Algebra R A] :
(L →ₗ⁅R 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.

Instances For
@[simp]
theorem UniversalEnvelopingAlgebra.lift_symm_apply (R : Type u₁) {L : Type u₂} [] [] [] {A : Type u₃} [Ring A] [Algebra R A] (F : ) :
().symm F =
@[simp]
theorem UniversalEnvelopingAlgebra.ι_comp_lift (R : Type u₁) {L : Type u₂} [] [] [] {A : Type u₃} [Ring A] [Algebra R A] (f : L →ₗ⁅R A) :
↑() = f
theorem UniversalEnvelopingAlgebra.lift_ι_apply (R : Type u₁) {L : Type u₂} [] [] [] {A : Type u₃} [Ring A] [Algebra R A] (f : L →ₗ⁅R A) (x : L) :
↑() () = f x
@[simp]
theorem UniversalEnvelopingAlgebra.lift_ι_apply' (R : Type u₁) {L : Type u₂} [] [] [] {A : Type u₃} [Ring A] [Algebra R A] (f : L →ₗ⁅R A) (x : L) :
↑() (↑() (↑() x)) = f x
theorem UniversalEnvelopingAlgebra.lift_unique (R : Type u₁) {L : Type u₂} [] [] [] {A : Type u₃} [Ring A] [Algebra R A] (f : L →ₗ⁅R A) (g : ) :
= f g =
theorem UniversalEnvelopingAlgebra.hom_ext (R : Type u₁) {L : Type u₂} [] [] [] {A : Type u₃} [Ring A] [Algebra R A] {g₁ : } {g₂ : } (h : ) :
g₁ = g₂

See note [partially-applied ext lemmas].