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 #

Tags #

lie algebra, universal enveloping algebra, tensor algebra

inductive UniversalEnvelopingAlgebra.Rel (R : Type u₁) (L : Type u₂) [CommRing R] [LieRing L] [LieAlgebra R L] :

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₂) [CommRing R] [LieRing L] [LieAlgebra R L] :
    Type (max u₁ u₂)

    The universal enveloping algebra of a Lie algebra.

    Instances For

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

      Instances For
        @[simp]

        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₂} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u₃} [Ring A] [Algebra 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.ι_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) :
            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) :
            @[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) :

            See note [partially-applied ext lemmas].