English
The map sending r: R to an endomorphism on the N-part to the P-part respects rTensor in a canonical way, i.e., rTensorHom behaves as expected with TensorProduct.
Русский
Отображение, отправляющее r на соответствующее отображение на N и P, сохраняет структуру rTensor согласно каноническим правилам TensorProduct.
LaTeX
$$$ rTensorHom : (N \\to P) \\to (N \\otimes M \\to P \\otimes M) $ is linear$$
Lean4
/-- `rTensorHom M` is the natural linear map that sends a linear map `f : N →ₗ P` to `f ⊗ M`.
See also `Module.End.rTensorAlgHom`. -/
def rTensorHom : (N →ₗ[R] P) →ₗ[R] N ⊗[R] M →ₗ[R] P ⊗[R] M
where
toFun f := f.rTensor M
map_add' f
g := by
ext x y
simp only [compr₂_apply, mk_apply, add_apply, rTensor_tmul, add_tmul]
map_smul' r
f := by
dsimp
ext x y
simp only [compr₂_apply, mk_apply, smul_tmul, tmul_smul, smul_apply, rTensor_tmul]
