tensorLeftHomEquiv_whiskerLeft_comp_evaluation

English

For X, Y with HasLeftDual, the symmetric form of the right adjoint mate produces an equality relating the cooperation of right dual and coevaluation with whiskering on the right.

Русский

Для X, Y с правым двойственным, симметричная форма правого сопряженного моста даёт равенство, связывающее кооперацию правого двойственного и коэвюацию с правым переносом.

LaTeX

$$$(\\mathrm{tensorRightHomEquiv}\\, (\\_ ,\\_ ,\\_ ,\\_)).symm(η\\_ Y Y' \\;≫\\; f \\rhd Y') = (λ\\_ \\_).hom \\gg f$$$

Lean4

@[simp]
theorem tensorLeftHomEquiv_whiskerLeft_comp_evaluation {Y Z : C} [HasLeftDual Z] (f : Y ⟶ ᘁZ) :
    (tensorLeftHomEquiv _ _ _ _) (Z ◁ f ≫ ε_ _ _) = f ≫ (ρ_ _).inv :=
  calc
    _ = 𝟙 _ ⊗≫ (η_ (ᘁZ : C) Z ▷ Y ≫ ((ᘁZ) ⊗ Z) ◁ f) ⊗≫ (ᘁZ) ◁ ε_ (ᘁZ) Z := by dsimp [tensorLeftHomEquiv]; monoidal
    _ = f ⊗≫ (η_ (ᘁZ) Z ▷ (ᘁZ) ⊗≫ (ᘁZ) ◁ ε_ (ᘁZ) Z) := by rw [← whisker_exchange]; monoidal
    _ = _ := by rw [evaluation_coevaluation'']; monoidal

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