English
The tensor-hom adjunction for modules with a Lie algebra action is compatible with the Lie action, giving a LieModule equivalence lifting a bilinear map to a map on the tensor product.
Русский
Сопоставление тензорного гомоморфа и билинейного отображения сохраняет действие Ли и образует эквивалентность на тензорном произведении.
LaTeX
$$def lift : (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 ring module. -/
instance lieRingModule : LieRingModule L (M ⊗[R] N)
where
bracket x := hasBracketAux x
add_lie x y
t :=
by
simp only [hasBracketAux, LinearMap.lTensor_add, LinearMap.rTensor_add, LieHom.map_add, LinearMap.add_apply]
abel
lie_add _ := LinearMap.map_add _
leibniz_lie x y
t :=
by
suffices (hasBracketAux x).comp (hasBracketAux y) = hasBracketAux ⁅x, y⁆ + (hasBracketAux y).comp (hasBracketAux x)
by rw [← LinearMap.comp_apply, this]; rfl
ext m n
simp only [hasBracketAux, AlgebraTensorModule.curry_apply, curry_apply, sub_tmul, tmul_sub,
LinearMap.coe_restrictScalars, Function.comp_apply, LinearMap.coe_comp, LinearMap.rTensor_tmul, LieHom.map_lie,
toEnd_apply_apply, LinearMap.add_apply, LinearMap.map_add, LieHom.lie_apply, Module.End.lie_apply,
LinearMap.lTensor_tmul]
abel
