tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight

English

In a rigid monoidal category with HasRightDual Y and left dual X, the simp lemma equates the image of a coevaluation followed by whiskering with the identity on the unit.

Русский

В ридидной моноидальной категории с HasRightDual Y и HasLeftDual X, упрощение согласования коэвюации после перетасовки с единицей даёт равенство изображения коэвюации затем перетащивания с единицей.

LaTeX

$$$(\\mathrm{tensorLeftHomEquiv}\\,(\\,\\_\\_,\\_\\_,\\_)).symm(η\\_\\_ \\gg\\; f) = (ρ\\_\\_).hom \\gg f$$$

Lean4

@[simp]
theorem tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight {Y Y' Z : C} [ExactPairing Y Y'] (f : Y ⟶ Z) :
    (tensorRightHomEquiv _ Y _ _).symm (η_ Y Y' ≫ f ▷ Y') = (λ_ _).hom ≫ f :=
  calc
    _ = η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 _ := by dsimp [tensorRightHomEquiv]; monoidal
    _ = (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f := by rw [← whisker_exchange]; monoidal
    _ = _ := by rw [evaluation_coevaluation'']; monoidal

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