Commit 2022-05-02 11:44 a6275694
View on Github →feat(category_theory/monoidal): adjunctions in rigid categories (#13707)
We construct the bijection on hom-sets (Yᘁ ⊗ X ⟶ Z) ≃ (X ⟶ Y ⊗ Z)
given by "pulling the string on the left" down or up, using right duals in a right rigid category.
As consequences, we show that a left rigid category is monoidal closed (it seems our lefts and rights have got mixed up!!), and that functors from a groupoid to a rigid category is again a rigid category.