Theorems · Definition · nonassociative algebras

UniversalEnvelopingAlgebra.mkAlgHom

(R : Type u₁) →
  (L : Type u₂) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : 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.

Defined in

Mathlib.Algebra.Lie.UniversalEnveloping

Cited by

3 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Quot.sound

Assumes

CommRingLieRingLieAlgebra