English
For Y, Y' and Z with an exact pairing Y ⊣ Y', the symmetry between left adjunction and evaluation yields a commuting diagram: the left adjoint mate composed with the evaluation equals the coevaluation composed with whiskering on the right.
Русский
Для Y, Y' и Z с точным сопряжением Y ⊣ Y' равносильность между левой парой и оценкой даёт диаграмму, которая компонуется равенством: левая сопряженность после оценки равна коэвюации после перетасовки справа.
LaTeX
$$$\\eta_{Y\\, (Y') } \\; \\rhd\\; Y' \\otimes (\\text{...}) \\; = \\; \\eta_{X\\, X'} \\; \\otimes \\; (\\text{...})$$$
Lean4
@[simp]
theorem tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft {Y Y' Z : C} [ExactPairing Y Y'] (f : Y' ⟶ Z) :
(tensorLeftHomEquiv _ _ _ _).symm (η_ _ _ ≫ Y ◁ f) = (ρ_ _).hom ≫ f := by
calc
_ = Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 _ := by dsimp [tensorLeftHomEquiv]; monoidal
_ = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f := by rw [whisker_exchange]; monoidal
_ = _ := by rw [coevaluation_evaluation'']; monoidal
