# If C is preadditive, Cᵒᵖ has a natural preadditive structure. #

Equations
• = { homGroup := fun (X Y : Cᵒᵖ) => ().addCommGroup, add_comp := , comp_add := }
instance CategoryTheory.moduleEndLeft (C : Type u_1) [] {X : Cᵒᵖ} {Y : C} :
Module (X.unop Y)
Equations
@[simp]
theorem CategoryTheory.unop_add (C : Type u_1) [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (g : X Y) :
(f + g).unop = f.unop + g.unop
@[simp]
theorem CategoryTheory.unop_zsmul (C : Type u_1) [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (k : ) (f : X Y) :
(k f).unop = k f.unop
@[simp]
theorem CategoryTheory.unop_neg (C : Type u_1) [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
(-f).unop = -f.unop
@[simp]
theorem CategoryTheory.op_add (C : Type u_1) [] {X : C} {Y : C} (f : X Y) (g : X Y) :
(f + g).op = f.op + g.op
@[simp]
theorem CategoryTheory.op_zsmul (C : Type u_1) [] {X : C} {Y : C} (k : ) (f : X Y) :
(k f).op = k f.op
@[simp]
theorem CategoryTheory.op_neg (C : Type u_1) [] {X : C} {Y : C} (f : X Y) :
(-f).op = -f.op
@[simp]
theorem CategoryTheory.unopHom_apply {C : Type u_1} [] (X : Cᵒᵖ) (Y : Cᵒᵖ) (f : X Y) :
() f = f.unop
def CategoryTheory.unopHom {C : Type u_1} [] (X : Cᵒᵖ) (Y : Cᵒᵖ) :
(X Y) →+ (Y.unop X.unop)

unop induces morphisms of monoids on hom groups of a preadditive category

Equations
Instances For
@[simp]
theorem CategoryTheory.unop_sum {C : Type u_1} [] (X : Cᵒᵖ) (Y : Cᵒᵖ) {ι : Type u_2} (s : ) (f : ι(X Y)) :
(s.sum f).unop = is, (f i).unop
@[simp]
theorem CategoryTheory.opHom_apply {C : Type u_1} [] (X : C) (Y : C) (f : X Y) :
() f = f.op
def CategoryTheory.opHom {C : Type u_1} [] (X : C) (Y : C) :
(X Y) →+ ({ unop := Y } { unop := X })

op induces morphisms of monoids on hom groups of a preadditive category

Equations
Instances For
@[simp]
theorem CategoryTheory.op_sum {C : Type u_1} [] (X : C) (Y : C) {ι : Type u_2} (s : ) (f : ι(X Y)) :
(s.sum f).op = is, (f i).op
instance CategoryTheory.Functor.op_additive {C : Type u_1} [] {D : Type u_2} [] (F : ) [F.Additive] :
Equations
• =
instance CategoryTheory.Functor.rightOp_additive {C : Type u_1} [] {D : Type u_2} [] (F : ) [F.Additive] :