From f2edc5a3529d95699b43514d6feb7eb11608723f Mon Sep 17 00:00:00 2001
From: Adam Topaz <github@adamtopaz.com>
Date: Mon, 5 Jul 2021 14:57:50 +0000
Subject: [PATCH] feat(category_theory/preadditive/opposite): Adds some
 instances and lemmas (#8202)

This PR adds some instances and lemmas related to opposites and additivity of functors.
---
 src/category_theory/opposites.lean            | 14 ++++++++++++--
 src/category_theory/preadditive/opposite.lean | 15 ++++++++++++++-
 2 files changed, 26 insertions(+), 3 deletions(-)

diff --git a/src/category_theory/opposites.lean b/src/category_theory/opposites.lean
index b24883da7675c..69d308c5b7984 100644
--- a/src/category_theory/opposites.lean
+++ b/src/category_theory/opposites.lean
@@ -231,7 +231,7 @@ we can take the "unopposite" of each component obtaining a natural transformatio
 end
 
 section
-variables {F G : C ⥤ Dᵒᵖ}
+variables {F G H : C ⥤ Dᵒᵖ}
 
 /--
 Given a natural transformation `α : F ⟶ G`, for `F G : C ⥤ Dᵒᵖ`,
@@ -245,6 +245,11 @@ taking `unop` of each component gives a natural transformation `G.left_op ⟶ F.
     simp_rw [← unop_comp, α.naturality]
   end }
 
+@[simp] lemma left_op_id : (𝟙 F : F ⟶ F).left_op = 𝟙 F.left_op := rfl
+
+@[simp] lemma left_op_comp (α : F ⟶ G) (β : G ⟶ H) :
+  (α ≫ β).left_op = β.left_op ≫ α.left_op := rfl
+
 /--
 Given a natural transformation `α : F.left_op ⟶ G.left_op`, for `F G : C ⥤ Dᵒᵖ`,
 taking `op` of each component gives a natural transformation `G ⟶ F`.
@@ -262,7 +267,7 @@ taking `op` of each component gives a natural transformation `G ⟶ F`.
 end
 
 section
-variables {F G : Cᵒᵖ ⥤ D}
+variables {F G H : Cᵒᵖ ⥤ D}
 
 /--
 Given a natural transformation `α : F ⟶ G`, for `F G : Cᵒᵖ ⥤ D`,
@@ -276,6 +281,11 @@ taking `op` of each component gives a natural transformation `G.right_op ⟶ F.r
     simp_rw [← op_comp, α.naturality]
   end }
 
+@[simp] lemma right_op_id : (𝟙 F : F ⟶ F).right_op = 𝟙 F.right_op := rfl
+
+@[simp] lemma right_op_comp (α : F ⟶ G) (β : G ⟶ H) :
+  (α ≫ β).right_op = β.right_op ≫ α.right_op := rfl
+
 /--
 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`.
diff --git a/src/category_theory/preadditive/opposite.lean b/src/category_theory/preadditive/opposite.lean
index 0be0768deac16..fec4539a5f879 100644
--- a/src/category_theory/preadditive/opposite.lean
+++ b/src/category_theory/preadditive/opposite.lean
@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Adam Topaz
 -/
 import category_theory.preadditive
+import category_theory.preadditive.additive_functor
 import data.equiv.transfer_instance
 
 /-!
@@ -26,5 +27,17 @@ instance : preadditive Cᵒᵖ :=
 
 @[simp] lemma unop_zero (X Y : Cᵒᵖ) : (0 : X ⟶ Y).unop = 0 := rfl
 @[simp] lemma unop_add {X Y : Cᵒᵖ} (f g : X ⟶ Y) : (f + g).unop = f.unop + g.unop := rfl
+@[simp] lemma op_zero (X Y : C) : (0 : X ⟶ Y).op = 0 := rfl
+@[simp] lemma op_add {X Y : C} (f g : X ⟶ Y) : (f + g).op = f.op + g.op := rfl
+
+variables {C} {D : Type*} [category D] [preadditive D]
+
+instance functor.op_additive (F : C ⥤ D) [F.additive] : F.op.additive := {}
+
+instance functor.right_op_additive (F : Cᵒᵖ ⥤ D) [F.additive] : F.right_op.additive := {}
+
+instance functor.left_op_additive (F : C ⥤ Dᵒᵖ) [F.additive] : F.left_op.additive := {}
+
+instance functor.unop_additive (F : Cᵒᵖ ⥤ Dᵒᵖ) [F.additive] : F.unop.additive := {}
 
 end category_theory