tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft

English

For X, Y with HasLeftDual, the left adjoint mate interacts with the coevaluation to equate two natural ways of passing f through the coevaluation and whiskering on the left.

Русский

Для X, Y с левым двойственным, левая сопряженная пара взаимодействует с коэвюацией, приводя к равенству двух естественных способов пропускать f через коэвюацию и левый перенос.

LaTeX

$$$\\eta_{(Y' ) Y} \\; \\rhd\\; Y \\otimes (Y' \\otimes Y) \\rightarrow f \\; = \\; (\\cdot) \\circ f$$$

Lean4

@[simp]
theorem tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) :
    (tensorRightHomEquiv _ (ᘁY) _ _).symm (η_ (ᘁX : C) X ≫ (ᘁX : C) ◁ f) = (λ_ _).hom ≫ ᘁf :=
  by
  dsimp [tensorRightHomEquiv, leftAdjointMate]
  simp

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