Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-29 04:24 e294500e

View on Github →

feat(category_theory/monoidal): transport rigid structure over an equivalence (#13736)

Estimated changes

Modified src/category_theory/monoidal/category.lean

added theorem category_theory.monoidal_category.hom_inv_id_tensor'

added theorem category_theory.monoidal_category.inv_hom_id_tensor'

added theorem category_theory.monoidal_category.tensor_hom_inv_id'

added theorem category_theory.monoidal_category.tensor_inv_hom_id'

Modified src/category_theory/monoidal/rigid.lean

added def category_theory.exact_pairing_congr

added def category_theory.exact_pairing_congr_left

added def category_theory.exact_pairing_congr_right

Created src/category_theory/monoidal/rigid/of_equivalence.lean

added def category_theory.exact_pairing_of_faithful

added def category_theory.exact_pairing_of_fully_faithful

added def category_theory.has_left_dual_of_equivalence

added def category_theory.has_right_dual_of_equivalence

added def category_theory.left_rigid_category_of_equivalence

added def category_theory.right_rigid_category_of_equivalence

added def category_theory.rigid_category_of_equivalence