English
Let C be a monoidal category with an exact pairing Y ⊣ Y'. For objects X, X', Y, Y', Z in C and morphisms f: X → X' and g: X' → Z ⊗ Y', the naturality of the right-hand tensor–hom correspondence states that applying the inverse of the right tensor–hom equivalence to the composite f; g is the same as first whiskering f on the right by Y and then applying the inverse to g.
Русский
Пусть C — моноидальная категория с точной связью Y ⊣ Y'. Пусть X, X', Y, Y', Z — объекты в C, f: X → X', g: X' → Z ⊗ Y'. Тогда естественность правой эквиваленции тензорного гомоморфизма говорит: обратная к right-tensor–hom применённая к составному f ≫ g равна f, «приплотному» к Y, затем применённой к g.
LaTeX
$$$\\bigl(\\mathrm{tensorRightHomEquiv}\\,(X,Y,Y',Z)\\bigr).symm\\bigl(f \\;\\gg\\; g\\bigr) = (f \\rhd_Y) \\;\\gg\\; \\bigl(\\mathrm{tensorRightHomEquiv}\\,(X',Y,Y',Z)\\bigr)^{\\! -1}\\; g$$$
Lean4
theorem tensorRightHomEquiv_symm_naturality {X X' Y Y' Z : C} [ExactPairing Y Y'] (f : X ⟶ X') (g : X' ⟶ Z ⊗ Y') :
(tensorRightHomEquiv X Y Y' Z).symm (f ≫ g) = f ▷ Y ≫ (tensorRightHomEquiv X' Y Y' Z).symm g := by
simp [tensorRightHomEquiv]
