mathlib

a6275694 - feat(category_theory/monoidal): adjunctions in rigid categories (#13707)

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>