mathlib documentation

category_theory.preadditive.opposite

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

source
@[instance]
def category_theory.opposite.preadditive (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] :
category_theory.preadditive Cᵒᵖ
Equations
source
@[simp]
theorem category_theory.unop_zero (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (X Y : Cᵒᵖ) :
0.unop = 0
source
@[simp]
theorem category_theory.unop_add (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {X Y : Cᵒᵖ} (f g : X ⟶ Y) :
(f + g).unop = f.unop + g.unop