English
Let R be a commutative ring, L a Lie algebra over R, A a ring with an R-algebra structure, and f: L →ₗ⁅R⁆ A a Lie algebra hom. Then the universal enveloping algebra U_R(L) admits a canonical algebra hom lift R f: U_R(L) → A extending f, and for every x ∈ L one has (lift R f)(ι_R(x)) = f(x). In particular, the restriction of lift R f to the Lie algebra L equals f.
Русский
Пусть R — коммутативное кольцо, L — Lie-алгебра над R, A — кольцо с структурой R-алгебры, f: L →ₗ⁅R⁆ A — гомоморфия Lie. Тогда существует каноническое расширение lift R f: U_R(L) → A такое, что при ограничении на L через вложение ι_R мы получаем f; то есть (lift R f)(ι_R(x)) = f(x) для всех x ∈ L. Следовательно, ограничение lift R f на L равно f.
LaTeX
$$$ (\\mathrm{lift}\\;R\\;f) \\circ (\\iota\\;R) = f $$$
Lean4
@[simp]
theorem lift_ι_apply' (x : L) : lift R f ((UniversalEnvelopingAlgebra.mkAlgHom R L) (ιₜ x)) = f x := by
simpa using lift_ι_apply R f x
