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₂) [CommRing R] [LieRing L] [LieAlgebra R L] : TensorAlgebra R L → TensorAlgebra R 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.

• lie_compat: ∀ {R : Type u₁} {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x y : L), UniversalEnvelopingAlgebra.Rel R L ((TensorAlgebra.ι R) ⁅x, y⁆ + (TensorAlgebra.ι R) y * (TensorAlgebra.ι R) x) ((TensorAlgebra.ι R) x * (TensorAlgebra.ι R) y)

def UniversalEnvelopingAlgebra (R : Type u₁) (L : Type u₂) [CommRing R] [LieRing L] [LieAlgebra R L] : Type (max u₁ u₂)

The universal enveloping algebra of a Lie algebra.

Equations

• UniversalEnvelopingAlgebra R L = RingQuot (UniversalEnvelopingAlgebra.Rel R L)

instance UniversalEnvelopingAlgebra.instInhabited (R : Type u₁) (L : Type u₂) [CommRing R] [LieRing L] [LieAlgebra R L] : Inhabited (UniversalEnvelopingAlgebra R L)

Equations

• UniversalEnvelopingAlgebra.instInhabited R L = inferInstanceAs (Inhabited (RingQuot (UniversalEnvelopingAlgebra.Rel R L)))

instance UniversalEnvelopingAlgebra.instRing (R : Type u₁) (L : Type u₂) [CommRing R] [LieRing L] [LieAlgebra R L] : Ring (UniversalEnvelopingAlgebra R L)

Equations

• UniversalEnvelopingAlgebra.instRing R L = inferInstanceAs (Ring (RingQuot (UniversalEnvelopingAlgebra.Rel R L)))

instance UniversalEnvelopingAlgebra.instAlgebra (R : Type u₁) (L : Type u₂) [CommRing R] [LieRing L] [LieAlgebra R L] : Algebra R (UniversalEnvelopingAlgebra R L)

Equations

• UniversalEnvelopingAlgebra.instAlgebra R L = inferInstanceAs (Algebra R (RingQuot (UniversalEnvelopingAlgebra.Rel R L)))

def UniversalEnvelopingAlgebra.mkAlgHom (R : Type u₁) (L : Type u₂) [CommRing R] [LieRing L] [LieAlgebra R L] : TensorAlgebra R L →ₐ[R] UniversalEnvelopingAlgebra R L

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

Equations

• UniversalEnvelopingAlgebra.mkAlgHom R L = RingQuot.mkAlgHom R (UniversalEnvelopingAlgebra.Rel R L)

@[simp]

theorem UniversalEnvelopingAlgebra.ι_apply (R : Type u₁) {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] : ∀ (a : L), (UniversalEnvelopingAlgebra.ι R) a = (UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) a)

def UniversalEnvelopingAlgebra.ι (R : Type u₁) {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] : L →ₗ⁅R⁆ UniversalEnvelopingAlgebra R L

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

Equations

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem UniversalEnvelopingAlgebra.lift_symm_apply (R : Type u₁) {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u₃} [Ring A] [Algebra R A] (F : UniversalEnvelopingAlgebra R L →ₐ[R] A) : (UniversalEnvelopingAlgebra.lift R).symm F = LieHom.comp (AlgHom.toLieHom F) (UniversalEnvelopingAlgebra.ι R)

@[simp]

theorem UniversalEnvelopingAlgebra.ι_comp_lift (R : Type u₁) {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u₃} [Ring A] [Algebra R A] (f : L →ₗ⁅R⁆ A) : ⇑((UniversalEnvelopingAlgebra.lift R) f) ∘ ⇑(UniversalEnvelopingAlgebra.ι R) = ⇑f

theorem UniversalEnvelopingAlgebra.lift_ι_apply (R : Type u₁) {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u₃} [Ring A] [Algebra R A] (f : L →ₗ⁅R⁆ A) (x : L) : ((UniversalEnvelopingAlgebra.lift R) f) ((UniversalEnvelopingAlgebra.ι R) x) = f x

@[simp]

theorem UniversalEnvelopingAlgebra.lift_ι_apply' (R : Type u₁) {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u₃} [Ring A] [Algebra R A] (f : L →ₗ⁅R⁆ A) (x : L) : ((UniversalEnvelopingAlgebra.lift R) f) ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = f x

theorem UniversalEnvelopingAlgebra.lift_unique (R : Type u₁) {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u₃} [Ring A] [Algebra R A] (f : L →ₗ⁅R⁆ A) (g : UniversalEnvelopingAlgebra R L →ₐ[R] A) : ⇑g ∘ ⇑(UniversalEnvelopingAlgebra.ι R) = ⇑f ↔ g = (UniversalEnvelopingAlgebra.lift R) f

theorem UniversalEnvelopingAlgebra.hom_ext (R : Type u₁) {L : Type u₂} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u₃} [Ring A] [Algebra R A] {g₁ : UniversalEnvelopingAlgebra R L →ₐ[R] A} {g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A} (h : LieHom.comp (AlgHom.toLieHom g₁) (UniversalEnvelopingAlgebra.ι R) = LieHom.comp (AlgHom.toLieHom g₂) (UniversalEnvelopingAlgebra.ι R)) : g₁ = g₂

See note [partially-applied ext lemmas].