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₂} [CommRing R] [LieRing L] [LieAlgebra R L] (x y : L) : Rel R L ((TensorAlgebra.ι R) ⁅x, y⁆ + (TensorAlgebra.ι R) y * (TensorAlgebra.ι R) x) ((TensorAlgebra.ι R) x * (TensorAlgebra.ι R) y)

def UniversalEnvelopingAlgebra.ringCon (R : Type u₁) (L : Type u₂) [CommRing R] [LieRing L] [LieAlgebra R L] : RingCon (TensorAlgebra R L)

Rel as a ring congruence, used to build the quotient.

Equations

• UniversalEnvelopingAlgebra.ringCon R L = ringConGen (UniversalEnvelopingAlgebra.Rel R L)

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 = (UniversalEnvelopingAlgebra.ringCon R L).Quotient

@[implicit_reducible]

instance instInhabitedUniversalEnvelopingAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : Inhabited (UniversalEnvelopingAlgebra R L)

Equations

• instInhabitedUniversalEnvelopingAlgebra R L = { default := instInhabitedUniversalEnvelopingAlgebra._aux_1 R L }

@[implicit_reducible]

instance instRingUniversalEnvelopingAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : Ring (UniversalEnvelopingAlgebra R L)

Equations

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

@[implicit_reducible]

instance instAlgebraUniversalEnvelopingAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : Algebra R (UniversalEnvelopingAlgebra R L)

Equations

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

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 = RingCon.mkₐ R (UniversalEnvelopingAlgebra.ringCon R L)

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

• UniversalEnvelopingAlgebra.ι R = { toLinearMap := (UniversalEnvelopingAlgebra.mkAlgHom R L).toLinearMap ∘ₗ TensorAlgebra.ι R, map_lie' := ⋯ }

@[simp]

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

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) : (lift R).symm F = F.toLieHom.comp (ι 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) : ⇑((lift R) f) ∘ ⇑(ι 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) : ((lift R) f) ((ι 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) : ((lift R) f) ((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 ∘ ⇑(ι R) = ⇑f ↔ g = (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₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A} (h : g₁.toLieHom.comp (ι R) = g₂.toLieHom.comp (ι R)) : g₁ = g₂

See note [partially-applied ext lemmas].

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