Preadditive structure on functor categories #

If C and D are categories and D is preadditive, then C ⥤ D is also preadditive.

@[protected, instance]
def category_theory.functor_category_preadditive {C : Type u_1} {D : Type u_2}  :
Equations
def category_theory.nat_trans.app_hom {C : Type u_1} {D : Type u_2} {F G : C D} (X : C) :
(F G) →+ (F.obj X G.obj X)

Application of a natural transformation at a fixed object, as group homomorphism

Equations
@[simp]
theorem category_theory.nat_trans.app_hom_apply {C : Type u_1} {D : Type u_2} {F G : C D} (X : C) (α : F G) :
= α.app X
@[simp]
theorem category_theory.nat_trans.app_zero {C : Type u_1} {D : Type u_2} {F G : C D} (X : C) :
0.app X = 0
@[simp]
theorem category_theory.nat_trans.app_add {C : Type u_1} {D : Type u_2} {F G : C D} (X : C) (α β : F G) :
+ β).app X = α.app X + β.app X
@[simp]
theorem category_theory.nat_trans.app_sub {C : Type u_1} {D : Type u_2} {F G : C D} (X : C) (α β : F G) :
- β).app X = α.app X - β.app X
@[simp]
theorem category_theory.nat_trans.app_neg {C : Type u_1} {D : Type u_2} {F G : C D} (X : C) (α : F G) :
(-α).app X = -α.app X
@[simp]
theorem category_theory.nat_trans.app_nsmul {C : Type u_1} {D : Type u_2} {F G : C D} (X : C) (α : F G) (n : ) :
(n α).app X = n α.app X
@[simp]
theorem category_theory.nat_trans.app_zsmul {C : Type u_1} {D : Type u_2} {F G : C D} (X : C) (α : F G) (n : ) :
(n α).app X = n α.app X
@[simp]
theorem category_theory.nat_trans.app_sum {C : Type u_1} {D : Type u_2} {F G : C D} {ι : Type u_5} (s : finset ι) (X : C) (α : ι → (F G)) :
(s.sum (λ (i : ι), α i)).app X = s.sum (λ (i : ι), (α i).app X)