feat(category_theory/opposites): iso.unop (#7400)

src/category_theory/opposites.lean

@@ -271,6 +271,19 @@ protected def op (α : X ≅ Y) : op Y ≅ op X :=
   hom_inv_id' := quiver.hom.unop_inj α.inv_hom_id,
   inv_hom_id' := quiver.hom.unop_inj α.hom_inv_id }
 
+/-- The isomorphism obtained from an isomorphism in the opposite category. -/
+@[simps] def unop {X Y : Cᵒᵖ} (f : X ≅ Y) : Y.unop ≅ X.unop :=
+{ hom := f.hom.unop,
+  inv := f.inv.unop,
+  hom_inv_id' := by simp only [← unop_comp, f.inv_hom_id, unop_id],
+  inv_hom_id' := by simp only [← unop_comp, f.hom_inv_id, unop_id] }
+
+@[simp] lemma unop_op {X Y : Cᵒᵖ} (f : X ≅ Y) : f.unop.op = f :=
+by ext; refl
+
+@[simp] lemma op_unop {X Y : C} (f : X ≅ Y) : f.op.unop = f :=
+by ext; refl
+
 end iso
 
 namespace nat_iso