Commit 2021-05-07 04:59 6d25f3ae

View on Github →

feat(category_theory/opposites): Adds equivalences for functor categories. (#7505) This PR adds the following equivalences for categories C and D:

(C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ induced by op and unop.
(Cᵒᵖ ⥤ D)ᵒᵖ ≌ (C ⥤ Dᵒᵖ) induced by left_op and right_op.

Estimated changes

Modified src/category_theory/opposites.lean

added def category_theory.functor.left_op_right_op_equiv

added def category_theory.functor.left_op_right_op_iso

added def category_theory.functor.op_unop_equiv

modified def category_theory.functor.op_unop_iso

added def category_theory.functor.right_op_left_op_iso

modified def category_theory.functor.unop_op_iso