English
A weaker form of the universal property: the space of L-equivariant bilinear maps is isomorphic to the space of L-equivariant linear maps out of a tensor product.
Русский
Улучшенная форма всеобъемлющей характеристики: множество L-эквивариантных билинейных отображений эквивалентно множеству L-эквивариантных линейных отображений из тензорного произведения.
LaTeX
$$def liftLie : (M →₅⁅R,L⁆ N →ₗ[R] P) ≃ₗ⁅R,L⁆ M ⊗[R] N →ₗ⁅R,L⁆ P$$
Lean4
/-- The tensor product of two Lie modules is a Lie module. -/
instance lieModule : LieModule R L (M ⊗[R] N)
where
smul_lie c x
t := by
change hasBracketAux (c • x) _ = c • hasBracketAux _ _
simp only [hasBracketAux, smul_add, LinearMap.rTensor_smul, LinearMap.smul_apply, LinearMap.lTensor_smul,
LieHom.map_smul, LinearMap.add_apply]
lie_smul c _ := LinearMap.map_smul _ c
