mathlib documentation

category_theory.preadditive.opposite

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

source
@[protected, instance]
def category_theory.opposite.preadditive (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] :
category_theory.preadditive Cᵒᵖ
Equations
source
@[protected, instance]
def category_theory.module_End_left (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {X : Cᵒᵖ} {Y : C} :
module (category_theory.End X) (opposite.unop X ⟶ Y)
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
source
@[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
source
@[simp]
theorem category_theory.unop_neg (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {X Y : Cᵒᵖ} (f : X ⟶ Y) :
(-f).unop = -f.unop
source
@[simp]
theorem category_theory.op_zero (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (X Y : C) :
0.op = 0
source
@[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
source
@[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
source
@[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
source
def category_theory.unop_hom {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X Y : Cᵒᵖ) :
(X ⟶ Y) →+ (opposite.unop Y ⟶ opposite.unop X)

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

Equations
source
@[simp]
theorem category_theory.unop_hom_apply {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X Y : Cᵒᵖ) (f : X ⟶ Y) :
⇑(category_theory.unop_hom X Y) f = f.unop
source
@[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)
source
def category_theory.op_hom {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X Y : C) :
(X ⟶ Y) →+ (opposite.op Y ⟶ opposite.op X)

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

Equations
source
@[simp]
theorem category_theory.op_hom_apply {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (X Y : C) (f : X ⟶ Y) :
⇑(category_theory.op_hom X Y) f = f.op
source
@[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)
source
@[protected, instance]
def category_theory.functor.op_additive {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {D : Type u_3} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.additive] :
F.op.additive
source
@[protected, instance]
def category_theory.functor.right_op_additive {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {D : Type u_3} [category_theory.category D] [category_theory.preadditive D] (F : Cᵒᵖ ⥤ D) [F.additive] :
F.right_op.additive
source
@[protected, instance]
def category_theory.functor.left_op_additive {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {D : Type u_3} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ Dᵒᵖ) [F.additive] :
F.left_op.additive
source
@[protected, instance]
def category_theory.functor.unop_additive {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {D : Type u_3} [category_theory.category D] [category_theory.preadditive D] (F : Cᵒᵖ ⥤ Dᵒᵖ) [F.additive] :
F.unop.additive