Documentation

Mathlib.CategoryTheory.Preadditive.FunctorCategory

Preadditive structure on functor categories #

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

source
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 = CategoryTheory.Preadditive.mk
source
@[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
source
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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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