English
Let X, X' be objects and Y, Y' Z be objects with an exact pairing Y ⊣ Y'. The tensorRightHomEquiv morphism respects left tensoring, i.e., the inverse of tensorRightHomEquiv applied to a tensor composition equals the composition of the left associator with the whiskering on the left and the inverse on f.
Русский
Пусть X, X'—объекты, Y, Y' и Z—объекты с точным сопряжением Y ⊣ Y'. Эквиваленция правого гомоморфизма сохраняет левое тензорирование: обратная к tensorRightHomEquiv применённая к композиции тензора равна композиции левого ассоциатора с левым перетаскиванием и обратной к f.
LaTeX
$$$\\bigl(\\mathrm{tensorRightHomEquiv}\\,(X' \\otimes X)\\,Y\\,Y'\\,Z\\bigr)^{\\!-1}\\bigl((g \\otimes_{\\mathrm{m}} f) \\;\\gg\\; (\\alpha_{\\_\\_\\_}.\\mathrm{inv})\\bigr) = (\\alpha_{\\_\\_\\_}.\\mathrm{hom}) \\circ \\bigl(g \\otimes_{\\mathrm{m}} (\\mathrm{tensorRightHomEquiv}\\,X Y Y' Z)^{\\!-1} f\\bigr)$$
Lean4
/-- `tensorRightHomEquiv` commutes with tensoring on the left -/
theorem tensorRightHomEquiv_tensor {X X' Y Y' Z Z' : C} [ExactPairing Y Y'] (f : X ⟶ Z ⊗ Y') (g : X' ⟶ Z') :
(tensorRightHomEquiv (X' ⊗ X) Y Y' (Z' ⊗ Z)).symm ((g ⊗ₘ f) ≫ (α_ _ _ _).inv) =
(α_ _ _ _).hom ≫ (g ⊗ₘ (tensorRightHomEquiv X Y Y' Z).symm f) :=
by simp [tensorRightHomEquiv, tensorHom_def]
