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.instZeroHomFunctor {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive D] {F G : Functor C D} :
Zero (F ⟶ G)
Equations
    source
    instance CategoryTheory.instAddHomFunctor {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive D] {F G : Functor C D} :
    Add (F ⟶ G)
    Equations
      source
      instance CategoryTheory.instNegHomFunctor {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive D] {F G : Functor C D} :
      Neg (F ⟶ G)
      Equations
        source
        instance CategoryTheory.functorCategoryPreadditive {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive D] :
        Preadditive (Functor C D)
        Equations
          source
          def CategoryTheory.NatTrans.appHom {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive D] {F G : 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
            Instances For
              source
              @[simp]
              theorem CategoryTheory.NatTrans.appHom_apply {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive D] {F G : Functor C D} (X : C) (α : F ⟶ G) :
              (appHom X) α = α.app X
              source
              @[simp]
              theorem CategoryTheory.NatTrans.app_zero {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive D] {F G : Functor C D} (X : C) :
              app 0 X = 0
              source
              @[simp]
              theorem CategoryTheory.NatTrans.app_add {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive D] {F G : Functor C D} (X : C) (α β : F ⟶ G) :
              (α + β).app X = α.app X + β.app X
              source
              @[simp]
              theorem CategoryTheory.NatTrans.app_sub {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive D] {F G : Functor C D} (X : C) (α β : F ⟶ G) :
              (α - β).app X = α.app X - β.app X
              source
              @[simp]
              theorem CategoryTheory.NatTrans.app_neg {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive D] {F G : 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} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive D] {F G : 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} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive D] {F G : Functor C D} (X : C) (α : F ⟶ G) (n : ℤ) :
              (n • α).app X = n • α.app X
              source
              @[simp]
              theorem CategoryTheory.NatTrans.app_units_zsmul {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [Preadditive D] {F G : 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} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] [Preadditive D] {F G : Functor C D} {ι : Type u_3} (s : Finset ι) (X : C) (α : ι → (F ⟶ G)) :
              (∑ i ∈ s, α i).app X = ∑ i ∈ s, (α i).app X