English
The construction homTensorHomEquiv gives a canonical equivalence between two tensor-Hom levels and the lift.equiv construction together with lift.equiv yields the same result as the standard lift.
Русский
Конструкция homTensorHomEquiv задаёт каноническое эквивалентность между двумя уровнями тензор-Гом и объединение с lift.equiv даёт тот же результат, что и стандартный lift.
LaTeX
$$$\\mathrm{homTensorHomEquiv}\\;R\\;M\\;N\\;P\\;Q : (M \\to_R P) \\otimes_R (N \\to_R Q) \\to_R (M \\otimes_R N) \\to_R (P \\otimes_R Q)$$$
Lean4
@[simp]
theorem homTensorHomEquiv_apply (x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) :
homTensorHomEquiv R M N P Q x = homTensorHomMap R M N P Q x := by
rw [← LinearEquiv.coe_toLinearMap, homTensorHomEquiv_toLinearMap]
