Preadditive structure on functor categories

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

instance CategoryTheory.instZeroHomFunctorToQuiverToCategoryStructCategory {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} : Zero (F ⟶ G)

Equations

• CategoryTheory.instZeroHomFunctorToQuiverToCategoryStructCategory = { zero := { app := fun (X : C) => 0, naturality := ⋯ } }

instance CategoryTheory.instAddHomFunctorToQuiverToCategoryStructCategory {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} : Add (F ⟶ G)

Equations

• CategoryTheory.instAddHomFunctorToQuiverToCategoryStructCategory = { add := fun (α β : F ⟶ G) => { app := fun (X : C) => α.app X + β.app X, naturality := ⋯ } }

instance CategoryTheory.instNegHomFunctorToQuiverToCategoryStructCategory {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} : Neg (F ⟶ G)

Equations

• CategoryTheory.instNegHomFunctorToQuiverToCategoryStructCategory = { neg := fun (α : F ⟶ G) => { app := fun (X : C) => -α.app X, naturality := ⋯ } }

instance CategoryTheory.functorCategoryPreadditive {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive D] : CategoryTheory.Preadditive (CategoryTheory.Functor C D)

Equations

• CategoryTheory.functorCategoryPreadditive = { homGroup := fun (F G : CategoryTheory.Functor C D) => AddCommGroup.mk ⋯, add_comp := ⋯, comp_add := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.appHom_apply {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) : (CategoryTheory.NatTrans.appHom X) α = α.app X

def CategoryTheory.NatTrans.appHom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor 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

• CategoryTheory.NatTrans.appHom X = { toZeroHom := { toFun := fun (α : F ⟶ G) => α.app X, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.app_zero {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (X : C) : 0.app X = 0

@[simp]

theorem CategoryTheory.NatTrans.app_add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) (β : F ⟶ G) : (α + β).app X = α.app X + β.app X

@[simp]

theorem CategoryTheory.NatTrans.app_sub {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) (β : F ⟶ G) : (α - β).app X = α.app X - β.app X

@[simp]

theorem CategoryTheory.NatTrans.app_neg {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) : (-α).app X = -α.app X

@[simp]

theorem CategoryTheory.NatTrans.app_nsmul {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) (n : ℕ) : (n • α).app X = n • α.app X

@[simp]

theorem CategoryTheory.NatTrans.app_zsmul {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) (n : ℤ) : (n • α).app X = n • α.app X

@[simp]

theorem CategoryTheory.NatTrans.app_units_zsmul {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) (n : ℤˣ) : (n • α).app X = n • α.app X

@[simp]

theorem CategoryTheory.NatTrans.app_sum {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {ι : Type u_3} (s : Finset ι) (X : C) (α : ι → (F ⟶ G)) : (Finset.sum s fun (i : ι) => α i).app X = Finset.sum s fun (i : ι) => (α i).app X