Universal enveloping algebra #
Given a commutative ring
R and a Lie algebra
R, we construct the universal
enveloping algebra of
L, together with its universal property.
Main definitions #
universal_enveloping_algebra: the universal enveloping algebra, endowed with an
universal_enveloping_algebra.ι: the Lie algebra morphism from
Lto its universal enveloping algebra.
universal_enveloping_algebra.lift: given an associative algebra
A, together with a Lie algebra morphism
f : L →ₗ⁅R⁆ A,
lift R L f : universal_enveloping_algebra R L →ₐ[R] Ais the unique morphism of algebras through which
universal_enveloping_algebra.ι_comp_lift: states that the lift of a morphism is indeed part of a factorisation.
universal_enveloping_algebra.lift_unique: states that lifts of morphisms are indeed unique.
universal_enveloping_algebra.hom_ext: a restatement of
lift_uniqueas an extensionality lemma.
lie algebra, universal enveloping algebra, tensor algebra
- lie_compat : ∀ (R : Type u₁) (L : Type u₂) [_inst_1 : comm_ring R] [_inst_2 : lie_ring L] [_inst_3 : lie_algebra R L] (x y : L), universal_enveloping_algebra.rel R L (⇑(tensor_algebra.ι R) ⁅x,y⁆ + (⇑(tensor_algebra.ι R) y) * ⇑(tensor_algebra.ι R) x) ((⇑(tensor_algebra.ι R) x) * ⇑(tensor_algebra.ι R) y)
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.
The quotient map from the tensor algebra to the universal enveloping algebra as a morphism of associative algebras.
The natural Lie algebra morphism from a Lie algebra to its universal enveloping algebra.
The universal property of the universal enveloping algebra: Lie algebra morphisms into associative algebras lift to associative algebra morphisms from the universal enveloping algebra.