Additive Functors #

A functor between two preadditive categories is called additive provided that the induced map on hom types is a morphism of abelian groups.

An additive functor between preadditive categories creates and preserves biproducts. Conversely, if F : C ⥤ D is a functor between preadditive categories, where C has binary biproducts, and if F preserves binary biproducts, then F is additive.

We also define the category of bundled additive functors.

Implementation details #

Functor.Additive is a Prop-valued class, defined by saying that for every two objects X and Y, the map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y) is a morphism of abelian groups.

  • map_add : ∀ {X Y : C} {f g : X Y}, (f + g) = f + g

    the addition of two morphisms is mapped to the sum of their images

A functor F is additive provided is an additive homomorphism.


    F.mapAddHom is an additive homomorphism whose underlying function is

    Instances For
      theorem CategoryTheory.Functor.map_sum {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {X : C} {Y : C} {α : Type u_3} (f : α → (X Y)) (s : Finset α) : (Finset.sum s fun a => f a) = Finset.sum s fun a => (f a)

      Bundled additive functors.

      Instances For

        the category of additive functors is denoted C ⥤+ D

        Instances For