English
Let R be a commutative ring, L a Lie algebra over R, and M, N, P Lie modules with compatible structures. For any Lie module morphism f: M →ₗ⁅R,L⁆ N →ₗ[R] P, there is a canonical lifted morphism liftLie R L M N P f: M ⊗R N →ₗ⁅R,L⁆ P such that its value on simple tensors is obtained by applying f to the first factor and then evaluating on the second: (liftLie R L M N P f)(m ⊗ n) = f m n for all m ∈ M, n ∈ N.
Русский
Пусть R — коммутативное кольцо, L — евклидовая алгебра Ли над R, и M, N, P — модули Ли, удовлетворяющие соответствующим условиям. Для любого гомоморфа Ли-модулей f: M →ₗ⁅R,L⁆ N →ₗ[R] P существует канонический поднесённый гомоморфизм liftLie R L M N P f: M ⊗R N →ₗ⁅R,L⁆ P так, что на простых тензорах выполняется (liftLie R L M N P f)(m ⊗ n) = f m n для всех m ∈ M, n ∈ N.
LaTeX
$$$$(\mathrm{liftLie}\,R\,L\,M\,N\,P\,f)(m \otimes n) = f\,m\,n,$$$$
Lean4
theorem liftLie_apply (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (m : M) (n : N) : liftLie R L M N P f (m ⊗ₜ n) = f m n := by
simp only [coe_liftLie_eq_lift_coe, LieModuleHom.coe_toLinearMap, lift_apply]
