tensorLeftHomEquiv_whiskerRight_comp_evaluation

English

A variant of right naturality for tensorRightHomEquiv with an optional dual pair structure; expresses the same compatibility under adapted duals and associators.

Русский

Вариант естественности справа для tensorRightHomEquiv с опциональной структурой двойственных пар; выражает ту же совместимость при адаптированных двойственных и ассоциаторных структурах.

LaTeX

$$$\\bigl(\\mathrm{tensorRightHomEquiv}\\, (X' \\otimes X) \\; Y \\; Y' \\; Z\\bigr)^{\\!-1}\\bigl((g \\otimes f) \\circ (\\alpha^{-1})\\bigr) = (\\alpha) \\circ (\\mathrm{tensorRightHomEquiv}\\, X Y Y' Z)^{\\!-1} g$$$$

Lean4

@[simp]
theorem tensorLeftHomEquiv_whiskerRight_comp_evaluation {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) :
    (tensorLeftHomEquiv _ _ _ _) (f ▷ _ ≫ ε_ _ _) = (ᘁf) ≫ (ρ_ _).inv :=
  by
  dsimp [tensorLeftHomEquiv, leftAdjointMate]
  simp

Похожие утверждения