English
Let Y, Y', Z be objects with an exact pairing Y ⊣ Y'. For morphisms f: X ⟶ Z ⊗ Y' and g: X' ⟶ Z', the left tensor–hom equivalence commutes with tensoring on the left, i.e., the inverse of tensorLeftHomEquiv applied to a composed tensor is equal to the composition of the inverse on f and g with the associator, up to the appropriate isomorphism.
Русский
Пусть Y, Y' и Z имеют точное сопряжение. Для морфизмов f: X ⟶ Y ⊗ Z и g: X' ⟶ Z' тензорная лево-эквиваленция совместима с тензорированием слева: применение противообразной left-эквивалентности к композиции равняется композиции обратной к f и g с ассоциатором.
LaTeX
$$$\\bigl(\\mathrm{tensorLeftHomEquiv}\\,(X \\otimes X')\\,Y\,Y'\\,(Z \\otimes Z')\\bigr)^{\\!-1}\\bigl((f \\otimes_{\\mathrm{m}} g) \\;\\gg\\; (\\alpha_{\\_\\_\\_}.\\mathrm{hom})\\bigr) = (\\alpha_{\\_\\_\\_}.\\mathrm{inv}) \\circ \\bigl(\\mathrm{tensorLeftHomEquiv}\\,X Y Y' Z\\bigr)^{\\!-1} f \\otimes_{\\mathrm{m}} g$$
Lean4
/-- `tensorLeftHomEquiv` commutes with tensoring on the right -/
theorem tensorLeftHomEquiv_tensor {X X' Y Y' Z Z' : C} [ExactPairing Y Y'] (f : X ⟶ Y ⊗ Z) (g : X' ⟶ Z') :
(tensorLeftHomEquiv (X ⊗ X') Y Y' (Z ⊗ Z')).symm ((f ⊗ₘ g) ≫ (α_ _ _ _).hom) =
(α_ _ _ _).inv ≫ ((tensorLeftHomEquiv X Y Y' Z).symm f ⊗ₘ g) :=
by simp [tensorLeftHomEquiv, tensorHom_def']
