mathlib documentation

category_theory.preadditive.functor_category

Preadditive structure on functor categories #

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

@[protected, instance]
Equations
def category_theory.nat_trans.app_hom {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive D] {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]
@[simp]
theorem category_theory.nat_trans.app_zero {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive D] {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} [category_theory.category C] [category_theory.category D] [category_theory.preadditive D] {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} [category_theory.category C] [category_theory.category D] [category_theory.preadditive D] {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} [category_theory.category C] [category_theory.category D] [category_theory.preadditive D] {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} [category_theory.category C] [category_theory.category D] [category_theory.preadditive D] {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} [category_theory.category C] [category_theory.category D] [category_theory.preadditive D] {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} [category_theory.category C] [category_theory.category D] [category_theory.preadditive D] {F G : C D} {ι : Type u_5} (s : finset ι) (X : C) (α : ι → (F G)) :
(∑ (i : ι) in s, α i).app X = ∑ (i : ι) in s, (α i).app X