English
There is a canonical linear equivalence between the tensor product of Hom-spaces and a Hom-space of tensor products.
Русский
Существует каноническое линейное эквивалентность между тензорным произведением пространств Hom и пространством Hom от тензоров.
LaTeX
$$$\\mathrm{homTensorHomEquiv}\\;R\\;M\\;N\\;P\\;Q : (M \\to_R P) \\otimes_R (N \\to_R Q) \\cong_R M \\otimes_R N \\to_R P \\otimes_R Q$$$
Lean4
/-- When `M` and `N` are free `R` modules, the map `homTensorHomMap` is an equivalence. Note that
`homTensorHomEquiv` is not defined directly in terms of `homTensorHomMap`, but the equivalence
between the two is given by `homTensorHomEquiv_toLinearMap` and `homTensorHomEquiv_apply`.
-/
noncomputable def homTensorHomEquiv : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) ≃ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q :=
rTensorHomEquivHomRTensor R M P _ ≪≫ₗ (LinearEquiv.refl R M).arrowCongr (lTensorHomEquivHomLTensor R N _ Q) ≪≫ₗ
lift.equiv R M N _
