English
The map sending a linear map f: N → P to lTensor M f is a linear map from N ⊗ M to P ⊗ M preserving addition and scalar action.
Русский
Отображение, отправляющее линейное отображение f: N → P в lTensor M f, является линейным отображением между N ⊗ M и P ⊗ M, сохраняющим сложение и действие скаляра.
LaTeX
$$$ lTensor M : (N \\to P) \\to (M \\otimes N \\to M \\otimes P) $ is linear$$
Lean4
/-- `lTensorHom M` is the natural linear map that sends a linear map `f : N →ₗ P` to `M ⊗ f`.
See also `Module.End.lTensorAlgHom`. -/
def lTensorHom : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] M ⊗[R] P
where
toFun := lTensor M
map_add' f
g := by
ext x y
simp only [compr₂_apply, mk_apply, add_apply, lTensor_tmul, tmul_add]
map_smul' r
f := by
dsimp
ext x y
simp only [compr₂_apply, mk_apply, tmul_smul, smul_apply, lTensor_tmul]
