Preadditive structure on functor categories

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

instance CategoryTheory.instZeroHomFunctor {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.instZeroHomFunctor = { zero := { app := fun (x : C) => 0, naturality := ⋯ } }

instance CategoryTheory.instAddHomFunctor {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.instAddHomFunctor = { add := fun (α β : F ⟶ G) => { app := fun (X : C) => α.app X + β.app X, naturality := ⋯ } }

instance CategoryTheory.instNegHomFunctor {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.instNegHomFunctor = { 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 = { 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) : CategoryTheory.NatTrans.app 0 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)) : (∑ i ∈ s, α i).app X = ∑ i ∈ s, (α i).app X