English
A weaker universal property for tensor products of Lie modules: the bilinear L-equivariant maps correspond to Lie-module homs from the tensor product.
Русский
Усложненная вариация всеобщего свойства тензорного произведения Ли-модулей: билинейные L-эквивариантные отображения трежутся к гомоморфизмам Ли-модулей из тензорного произведения.
LaTeX
$$def liftLie : (M →ₗ⁅R,L⁆ N →ₗ[R] P) ≃ₗ⁅R,L⁆ M ⊗[R] N →ₗ⁅R,L⁆ P$$
Lean4
/-- The universal property for tensor product of modules of a Lie algebra: the `R`-linear
tensor-hom adjunction is equivariant with respect to the `L` action. -/
def lift : (M →ₗ[R] N →ₗ[R] P) ≃ₗ⁅R,L⁆ M ⊗[R] N →ₗ[R] P :=
{ TensorProduct.lift.equiv R M N P with
map_lie' := fun {x f} => by
ext m n
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe, AlgebraTensorModule.curry_apply,
curry_apply, LinearMap.coe_restrictScalars, lift.equiv_apply, LieHom.lie_apply, LinearMap.sub_apply,
lie_tmul_right, map_add]
abel }
