Documentation

Mathlib.CategoryTheory.Preadditive.Opposite

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

@[simp]
theorem CategoryTheory.unop_add (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {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) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (k : ) (f : X Y) :
(k f).unop = k f.unop
@[simp]
theorem CategoryTheory.unop_neg (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
(-f).unop = -f.unop
@[simp]
theorem CategoryTheory.op_add (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {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) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} (k : ) (f : X Y) :
(k f).op = k f.op
@[simp]
theorem CategoryTheory.op_neg (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} (f : X Y) :
(-f).op = -f.op

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

Equations
Instances For
    @[simp]
    theorem CategoryTheory.unop_sum {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : Cᵒᵖ) (Y : Cᵒᵖ) {ι : Type u_2} (s : Finset ι) (f : ι(X Y)) :
    (Finset.sum s f).unop = Finset.sum s fun (i : ι) => (f i).unop
    @[simp]

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

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.op_sum {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : C) (Y : C) {ι : Type u_2} (s : Finset ι) (f : ι(X Y)) :
      (Finset.sum s f).op = Finset.sum s fun (i : ι) => (f i).op