mathlib3 documentation

category_theory.preadditive.functor_category

Preadditive structure on functor categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
Equations

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

Equations
@[simp]
@[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)) :
(s.sum (λ (i : ι), α i)).app X = s.sum (λ (i : ι), (α i).app X)