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
.
Equations
- CategoryTheory.Functor.mapAddHom F = AddMonoidHom.mk' (fun f => F.map f) (_ : ∀ (x x_1 : X ⟶ Y), F.map (x + x_1) = F.map x + F.map x_1)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Bundled additive functors.
Equations
- (C ⥤+ D) = CategoryTheory.FullSubcategory fun F => CategoryTheory.Functor.Additive F
Instances For
the category of additive functors is denoted C ⥤+ D
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.instPreadditiveAdditiveFunctorInstCategoryAdditiveFunctor C D = CategoryTheory.Preadditive.inducedCategory CategoryTheory.FullSubcategory.obj
An additive functor is in particular a functor.
Equations
Instances For
Turn an additive functor into an object of the category AdditiveFunctor C D
.
Equations
- CategoryTheory.AdditiveFunctor.of F = { obj := F, property := (_ : CategoryTheory.Functor.Additive F) }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Turn a left exact functor into an additive functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Turn a right exact functor into an additive functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Turn an exact functor into an additive functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.