English
The universal enveloping algebra of the free Lie algebra is isomorphic to the free unital associative algebra.
Русский
Обобщающая алгебра универсального охватывающего свободной Lie-алгебры изоморфна свободной унитальной ассоциативной алгебре.
LaTeX
$$$\mathrm{UniversalEnvelopingAlgebra}_R\bigl(\mathrm{FreeLieAlgebra}_R X\bigr) \cong_{\mathrm{alg},R} \mathrm{FreeAlgebra}_R X.$$$
Lean4
/-- The universal enveloping algebra of the free Lie algebra is just the free unital associative
algebra. -/
@[simps!]
def universalEnvelopingEquivFreeAlgebra : UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) ≃ₐ[R] FreeAlgebra R X :=
AlgEquiv.ofAlgHom (UniversalEnvelopingAlgebra.lift R <| FreeLieAlgebra.lift R <| FreeAlgebra.ι R)
(FreeAlgebra.lift R <| UniversalEnvelopingAlgebra.ι R ∘ FreeLieAlgebra.of R) (by ext; simp) (by ext; simp)
