feat(category_theory/opposites): Adds equivalences for functor catego…

…ries. (#7505)

This PR adds the following equivalences for categories `C` and `D`:
1. `(C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ` induced by `op` and `unop`.
2.  `(Cᵒᵖ ⥤ D)ᵒᵖ ≌ (C ⥤ Dᵒᵖ)` induced by `left_op` and `right_op`.

src/category_theory/opposites.lean

@@ -113,11 +113,11 @@ protected def unop (F : Cᵒᵖ ⥤ Dᵒᵖ) : C ⥤ D :=
   map := λ X Y f, (F.map f.op).unop }
 
 /-- The isomorphism between `F.op.unop` and `F`. -/
-def op_unop_iso (F : C ⥤ D) : F.op.unop ≅ F :=
+@[simps] def op_unop_iso (F : C ⥤ D) : F.op.unop ≅ F :=
 nat_iso.of_components (λ X, iso.refl _) (by tidy)
 
 /-- The isomorphism between `F.unop.op` and `F`. -/
-def unop_op_iso (F : Cᵒᵖ ⥤ Dᵒᵖ) : F.unop.op ≅ F :=
+@[simps] def unop_op_iso (F : Cᵒᵖ ⥤ Dᵒᵖ) : F.unop.op ≅ F :=
 nat_iso.of_components (λ X, iso.refl _) (by tidy)
 
 variables (C D)
@@ -142,8 +142,6 @@ def op_inv : (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ :=
   { app := λ X, (α.app (op X)).unop,
     naturality' := λ X Y f, quiver.hom.op_inj $ (α.naturality f.op).symm } }
 
--- TODO show these form an equivalence
-
 variables {C D}
 
 /--
@@ -164,8 +162,6 @@ protected def right_op (F : Cᵒᵖ ⥤ D) : C ⥤ Dᵒᵖ :=
 { obj := λ X, op (F.obj (op X)),
   map := λ X Y f, (F.map f.op).op }
 
--- TODO show these form an equivalence
-
 instance {F : C ⥤ D} [full F] : full F.op :=
 { preimage := λ X Y f, (F.preimage f.unop).op }
 
@@ -181,6 +177,16 @@ instance right_op_faithful {F : Cᵒᵖ ⥤ D} [faithful F] : faithful F.right_o
 instance left_op_faithful {F : C ⥤ Dᵒᵖ} [faithful F] : faithful F.left_op :=
 { map_injective' := λ X Y f g h, quiver.hom.unop_inj (map_injective F (quiver.hom.unop_inj h)) }
 
+/-- The isomorphism between `F.left_op.right_op` and `F`. -/
+@[simps]
+def left_op_right_op_iso (F : C ⥤ Dᵒᵖ) : F.left_op.right_op ≅ F :=
+nat_iso.of_components (λ X, iso.refl _) (by tidy)
+
+/-- The isomorphism between `F.right_op.left_op` and `F`. -/
+@[simps]
+def right_op_left_op_iso (F : Cᵒᵖ ⥤ D) : F.right_op.left_op ≅ F :=
+nat_iso.of_components (λ X, iso.refl _) (by tidy)
+
 end
 
 end functor
@@ -238,7 +244,12 @@ taking `unop` of each component gives a natural transformation `G.left_op ⟶ F.
 -/
 @[simps] protected def left_op (α : F ⟶ G) : G.left_op ⟶ F.left_op :=
 { app         := λ X, (α.app (unop X)).unop,
-  naturality' := begin tidy, erw α.naturality, refl, end }
+  naturality' := begin
+    intros X Y f,
+    dsimp,
+    erw α.naturality,
+    refl,
+  end }
 
 /--
 Given a natural transformation `α : F.left_op ⟶ G.left_op`, for `F G : C ⥤ Dᵒᵖ`,
@@ -254,6 +265,39 @@ taking `op` of each component gives a natural transformation `G ⟶ F`.
     erw this
   end }
 
+end
+
+section
+variables {F G : Cᵒᵖ ⥤ D}
+
+local attribute [semireducible] quiver.opposite
+
+/--
+Given a natural transformation `α : F ⟶ G`, for `F G : Cᵒᵖ ⥤ D`,
+taking `op` of each component gives a natural transformation `G.right_op ⟶ F.right_op`.
+-/
+@[simps] protected def right_op (α : F ⟶ G) : G.right_op ⟶ F.right_op :=
+{ app := λ X, (α.app _).op,
+  naturality' := begin
+    intros X Y f,
+    dsimp,
+    erw α.naturality,
+    refl,
+  end }
+
+/--
+Given a natural transformation `α : F.right_op ⟶ G.right_op`, for `F G : Cᵒᵖ ⥤ D`,
+taking `unop` of each component gives a natural transformation `G ⟶ F`.
+-/
+@[simps] protected def remove_right_op (α : F.right_op ⟶ G.right_op) : G ⟶ F :=
+{ app := λ X, (α.app X.unop).unop,
+  naturality' := begin
+    intros X Y f,
+    have := congr_arg quiver.hom.unop (α.naturality f.unop),
+    dsimp at this,
+    erw this,
+  end }
+
 end
 end nat_trans
 
@@ -381,4 +425,47 @@ quiver.hom.op (hom_of_le h)
 lemma le_of_op_hom {U V : αᵒᵖ} (h : U ⟶ V) : unop V ≤ unop U :=
 le_of_hom (h.unop)
 
+namespace functor
+
+variables (C)
+variables (D : Type u₂) [category.{v₂} D]
+
+/-- 
+The equivalence of functor categories induced by `op` and `unop`.
+-/
+@[simps]
+def op_unop_equiv : (C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ :=
+{ functor := op_hom _ _,
+  inverse := op_inv _ _,
+  unit_iso := nat_iso.of_components (λ F, F.unop.op_unop_iso.op) begin
+    intros F G f,
+    dsimp [op_unop_iso],
+    rw [(show f = f.unop.op, by simp), ← op_comp, ← op_comp],
+    congr' 1,
+    tidy,
+  end,
+  counit_iso := nat_iso.of_components (λ F, F.unop_op_iso) (by tidy) }.
+
+/--
+The equivalence of functor categories induced by `left_op` and `right_op`.
+-/
+@[simps]
+def left_op_right_op_equiv : (Cᵒᵖ ⥤ D)ᵒᵖ ≌ (C ⥤ Dᵒᵖ) :=
+{ functor :=
+  { obj := λ F, F.unop.right_op,
+    map := λ F G η, η.unop.right_op },
+  inverse :=
+  { obj := λ F, op F.left_op,
+    map := λ F G η, η.left_op.op },
+  unit_iso := nat_iso.of_components (λ F, F.unop.right_op_left_op_iso.op) begin
+    intros F G η,
+    dsimp,
+    rw [(show η = η.unop.op, by simp), ← op_comp, ← op_comp],
+    congr' 1,
+    tidy,
+  end,
+  counit_iso := nat_iso.of_components (λ F, F.left_op_right_op_iso) (by tidy) }
+
+end functor
+
 end category_theory