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 F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)
is a morphism of abelian groups.
the addition of two morphisms is mapped to the sum of their images
A functor F
is additive provided F.map
is an additive homomorphism.
Instances
F.mapAddHom
is an additive homomorphism whose underlying function is F.map
.
Instances For
Bundled additive functors.
Instances For
the category of additive functors is denoted C ⥤+ D
Instances For
An additive functor is in particular a functor.
Instances For
Turn an additive functor into an object of the category AdditiveFunctor C D
.
Instances For
Turn a left exact functor into an additive functor.
Instances For
Turn a right exact functor into an additive functor.
Instances For
Turn an exact functor into an additive functor.