mathlib documentation

category_theory.preadditive.opposite

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

@[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
@[simp]
theorem category_theory.unop_zsmul (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {X Y : Cᵒᵖ} (k : ) (f : X Y) :
(k f).unop = k f.unop
@[simp]
@[simp]
@[simp]
theorem category_theory.op_add (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {X Y : C} (f g : X Y) :
(f + g).op = f.op + g.op
@[simp]
theorem category_theory.op_zsmul (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {X Y : C} (k : ) (f : X Y) :
(k f).op = k f.op
@[simp]
theorem category_theory.op_neg (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {X Y : C} (f : X Y) :
(-f).op = -f.op

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

Equations
@[simp]
theorem category_theory.unop_sum {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X Y : Cᵒᵖ) {ι : Type u_3} (s : finset ι) (f : ι (X Y)) :
(s.sum f).unop = s.sum (λ (i : ι), (f i).unop)

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

Equations
@[simp]
theorem category_theory.op_sum {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X Y : C) {ι : Type u_3} (s : finset ι) (f : ι (X Y)) :
(s.sum f).op = s.sum (λ (i : ι), (f i).op)