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.

Main definitions #

universal_enveloping_algebra: the universal enveloping algebra, endowed with an R-algebra structure.
universal_enveloping_algebra.ι: the Lie algebra morphism from L to 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] A is the unique morphism of algebras through which f factors.
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_unique as an extensionality lemma.

Tags #

lie algebra, universal enveloping algebra, tensor algebra

source

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

tensor_algebra R L → tensor_algebra R L → Prop

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.

source

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

Type (max u₁ u₂)

The universal enveloping algebra of a Lie algebra.

Equations

universal_enveloping_algebra R L = ring_quot (universal_enveloping_algebra.rel R L)

Instances for universal_enveloping_algebra

source

@[protected, instance]

def universal_enveloping_algebra.algebra (R : Type u₁) (L : Type u₂) [comm_ring R] [lie_ring L] [lie_algebra R L] :

algebra R (universal_enveloping_algebra R L)

source

@[protected, instance]

def universal_enveloping_algebra.ring (R : Type u₁) (L : Type u₂) [comm_ring R] [lie_ring L] [lie_algebra R L] :

ring (universal_enveloping_algebra R L)

source

@[protected, instance]

def universal_enveloping_algebra.inhabited (R : Type u₁) (L : Type u₂) [comm_ring R] [lie_ring L] [lie_algebra R L] :

inhabited (universal_enveloping_algebra R L)

source

def universal_enveloping_algebra.mk_alg_hom (R : Type u₁) (L : Type u₂) [comm_ring R] [lie_ring L] [lie_algebra R L] :

tensor_algebra R L →ₐ[R] universal_enveloping_algebra R L

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

Equations

universal_enveloping_algebra.mk_alg_hom R L = ring_quot.mk_alg_hom R (universal_enveloping_algebra.rel R L)

source

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

L →ₗ⁅R⁆ universal_enveloping_algebra R L

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

Equations

universal_enveloping_algebra.ι R = {to_linear_map := {to_fun := ((universal_enveloping_algebra.mk_alg_hom R L).to_linear_map.comp (tensor_algebra.ι R)).to_fun, map_add' := _, map_smul' := _}, map_lie' := _}

source

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

(L →ₗ⁅R⁆ A) ≃ (universal_enveloping_algebra R 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.

Equations

universal_enveloping_algebra.lift R = {to_fun := λ (f : L →ₗ⁅R⁆ A), ⇑(ring_quot.lift_alg_hom R) ⟨⇑(tensor_algebra.lift R) ↑f, _⟩, inv_fun := λ (F : universal_enveloping_algebra R L →ₐ[R] A), ↑F.comp (universal_enveloping_algebra.ι R), left_inv := _, right_inv := _}

source

@[simp]

theorem universal_enveloping_algebra.lift_symm_apply (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [lie_algebra R L] {A : Type u₃} [ring A] [algebra R A] (F : universal_enveloping_algebra R L →ₐ[R] A) :

⇑((universal_enveloping_algebra.lift R).symm) F = ↑F.comp (universal_enveloping_algebra.ι R)

source

@[simp]

theorem universal_enveloping_algebra.ι_comp_lift (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [lie_algebra R L] {A : Type u₃} [ring A] [algebra R A] (f : L →ₗ⁅R⁆ A) :

⇑(⇑(universal_enveloping_algebra.lift R) f) ∘ ⇑(universal_enveloping_algebra.ι R) = ⇑f

source

@[simp]

theorem universal_enveloping_algebra.lift_ι_apply (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [lie_algebra R L] {A : Type u₃} [ring A] [algebra R A] (f : L →ₗ⁅R⁆ A) (x : L) :

⇑(⇑(universal_enveloping_algebra.lift R) f) (⇑(universal_enveloping_algebra.ι R) x) = ⇑f x

source

theorem universal_enveloping_algebra.lift_unique (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [lie_algebra R L] {A : Type u₃} [ring A] [algebra R A] (f : L →ₗ⁅R⁆ A) (g : universal_enveloping_algebra R L →ₐ[R] A) :

⇑g ∘ ⇑(universal_enveloping_algebra.ι R) = ⇑f ↔ g = ⇑(universal_enveloping_algebra.lift R) f

source

@[ext]

theorem universal_enveloping_algebra.hom_ext (R : Type u₁) {L : Type u₂} [comm_ring R] [lie_ring L] [lie_algebra R L] {A : Type u₃} [ring A] [algebra R A] {g₁ g₂ : universal_enveloping_algebra R L →ₐ[R] A} (h : ↑g₁.comp (universal_enveloping_algebra.ι R) = ↑g₂.comp (universal_enveloping_algebra.ι R)) :

g₁ = g₂

See note [partially-applied ext lemmas].