If C
is preadditive, Cᵒᵖ
has a natural preadditive structure. #
@[protected, instance]
def
category_theory.opposite.preadditive
(C : Type u_1)
[category_theory.category C]
[category_theory.preadditive C] :
Equations
- category_theory.opposite.preadditive C = {hom_group := λ (X Y : Cᵒᵖ), (category_theory.op_equiv X Y).add_comm_group, add_comp' := _, comp_add' := _}
@[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
- category_theory.module_End_left C = {to_distrib_mul_action := {to_mul_action := category_theory.End.mul_action_left Y, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[simp]
theorem
category_theory.unop_zero
(C : Type u_1)
[category_theory.category C]
[category_theory.preadditive C]
(X Y : Cᵒᵖ) :
@[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) :
@[simp]
theorem
category_theory.op_zero
(C : Type u_1)
[category_theory.category C]
[category_theory.preadditive C]
(X Y : C) :
@[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) :
@[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] :
@[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] :
@[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] :
@[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] :