# Documentation

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.

class CategoryTheory.Functor.Additive {C : Type u_1} {D : Type u_2} [] [] (F : ) :

A functor F is additive provided F.map is an additive homomorphism.

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

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

Instances
theorem CategoryTheory.Functor.Additive.map_add {C : Type u_1} {D : Type u_2} [] [] {F : } [self : F.Additive] {X : C} {Y : C} {f : X Y} {g : X Y} :
F.map (f + g) = F.map f + F.map g

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

@[simp]
theorem CategoryTheory.Functor.map_add {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] {X : C} {Y : C} {f : X Y} {g : X Y} :
F.map (f + g) = F.map f + F.map g
@[simp]
theorem CategoryTheory.Functor.mapAddHom_apply {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] {X : C} {Y : C} (f : X Y) :
def CategoryTheory.Functor.mapAddHom {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] {X : C} {Y : C} :
(X Y) →+ (F.obj X F.obj Y)

F.mapAddHom is an additive homomorphism whose underlying function is F.map.

Equations
Instances For
theorem CategoryTheory.Functor.coe_mapAddHom {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] {X : C} {Y : C} :
@[instance 100]
instance CategoryTheory.Functor.preservesZeroMorphisms_of_additive {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] :
F.PreservesZeroMorphisms
Equations
• =
instance CategoryTheory.Functor.instAdditiveId {C : Type u_1} [] :
Equations
• =
instance CategoryTheory.Functor.instAdditiveComp {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] {E : Type u_4} [] (G : ) [G.Additive] :
Equations
• =
@[simp]
theorem CategoryTheory.Functor.map_neg {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] {X : C} {Y : C} {f : X Y} :
F.map (-f) = -F.map f
@[simp]
theorem CategoryTheory.Functor.map_sub {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] {X : C} {Y : C} {f : X Y} {g : X Y} :
F.map (f - g) = F.map f - F.map g
theorem CategoryTheory.Functor.map_nsmul {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] {X : C} {Y : C} {f : X Y} {n : } :
F.map (n f) = n F.map f
theorem CategoryTheory.Functor.map_zsmul {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] {X : C} {Y : C} {f : X Y} {r : } :
F.map (r f) = r F.map f
@[simp]
theorem CategoryTheory.Functor.map_sum {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] {X : C} {Y : C} {α : Type u_4} (f : α(X Y)) (s : ) :
F.map (as, f a) = as, F.map (f a)
theorem CategoryTheory.Functor.additive_of_iso {C : Type u_1} {D : Type u_2} [] [] {F : } [F.Additive] {G : } (e : F G) :
theorem CategoryTheory.Functor.additive_of_full_essSurj_comp {C : Type u_1} {D : Type u_2} {E : Type u_3} [] [] [] (F : ) [F.Additive] [F.Full] [F.EssSurj] (G : ) [(F.comp G).Additive] :
theorem CategoryTheory.Functor.additive_of_comp_faithful {C : Type u_1} {D : Type u_2} {E : Type u_3} [] [] [] (F : ) (G : ) [G.Additive] [(F.comp G).Additive] [G.Faithful] :
theorem CategoryTheory.Functor.hasZeroObject_of_additive {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] :
instance CategoryTheory.Functor.inducedFunctor_additive {C : Type u_1} {D : Type u_2} [] (F : CD) :
Equations
• =
instance CategoryTheory.Functor.fullSubcategoryInclusion_additive {C : Type u_1} [] (Z : CProp) :
Equations
• =
@[instance 100]
instance CategoryTheory.Functor.preservesFiniteBiproductsOfAdditive {C : Type u₁} {D : Type u₂} [] [] (F : ) [F.Additive] :
Equations
• One or more equations did not get rendered due to their size.
theorem CategoryTheory.Functor.additive_of_preservesBinaryBiproducts {C : Type u₁} {D : Type u₂} [] [] (F : ) [F.PreservesZeroMorphisms] :
theorem CategoryTheory.Functor.additive_of_preserves_binary_products {C : Type u₁} {D : Type u₂} [] [] (F : ) [F.PreservesZeroMorphisms] :
instance CategoryTheory.Equivalence.inverse_additive {C : Type u_1} {D : Type u_2} [] [] (e : C D) [e.functor.Additive] :
Equations
• =
def CategoryTheory.AdditiveFunctor (C : Type u_1) (D : Type u_2) [] [] :
Type (max (max (max u_1 u_2) u_3) u_4)

Equations
Instances For
instance CategoryTheory.instCategoryAdditiveFunctor (C : Type u_1) (D : Type u_2) [] [] :
Equations

the category of additive functors is denoted C ⥤+ D

Equations
Instances For
instance CategoryTheory.instPreadditiveAdditiveFunctor (C : Type u_1) (D : Type u_2) [] [] :
Equations

An additive functor is in particular a functor.

Equations
Instances For
instance CategoryTheory.instFullAdditiveFunctorFunctorForget (C : Type u_1) (D : Type u_2) [] [] :
.Full
Equations
• =
def CategoryTheory.AdditiveFunctor.of {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] :
C ⥤+ D

Turn an additive functor into an object of the category AdditiveFunctor C D.

Equations
• = { obj := F, property := }
Instances For
@[simp]
theorem CategoryTheory.AdditiveFunctor.of_fst {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] :
= F
@[simp]
theorem CategoryTheory.AdditiveFunctor.forget_obj {C : Type u_1} {D : Type u_2} [] [] (F : C ⥤+ D) :
.obj F = F.obj
theorem CategoryTheory.AdditiveFunctor.forget_obj_of {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Additive] :
@[simp]
theorem CategoryTheory.AdditiveFunctor.forget_map {C : Type u_1} {D : Type u_2} [] [] (F : C ⥤+ D) (G : C ⥤+ D) (α : F G) :
.map α = α
instance CategoryTheory.instAdditiveAdditiveFunctorFunctorForget {C : Type u_1} {D : Type u_2} [] [] :
Equations
• =
instance CategoryTheory.instAdditiveObjFunctor {C : Type u_1} {D : Type u_2} [] [] (F : C ⥤+ D) :
Equations
• =

Turn a left exact functor into an additive functor.

Equations
Instances For
Equations
• =
Equations
• =

Turn a right exact functor into an additive functor.

Equations
Instances For
Equations
• =
Equations
• =

Turn an exact functor into an additive functor.

Equations
Instances For
Equations
• =
Equations
• =
@[simp]
theorem CategoryTheory.AdditiveFunctor.ofLeftExact_obj_fst {C : Type u₁} {D : Type u₂} [] [] (F : C ⥤ₗ D) :
( F).obj = F.obj
@[simp]
theorem CategoryTheory.AdditiveFunctor.ofRightExact_obj_fst {C : Type u₁} {D : Type u₂} [] [] (F : C ⥤ᵣ D) :
( F).obj = F.obj
@[simp]
theorem CategoryTheory.AdditiveFunctor.ofExact_obj_fst {C : Type u₁} {D : Type u₂} [] [] (F : C ⥤ₑ D) :
(.obj F).obj = F.obj
@[simp]
theorem CategoryTheory.AdditiveFunctor.ofLeftExact_map {C : Type u₁} {D : Type u₂} [] [] {F : C ⥤ₗ D} {G : C ⥤ₗ D} (α : F G) :
α = α
@[simp]
theorem CategoryTheory.AdditiveFunctor.ofRightExact_map {C : Type u₁} {D : Type u₂} [] [] {F : C ⥤ᵣ D} {G : C ⥤ᵣ D} (α : F G) :
α = α
@[simp]
theorem CategoryTheory.AdditiveFunctor.ofExact_map {C : Type u₁} {D : Type u₂} [] [] {F : C ⥤ₑ D} {G : C ⥤ₑ D} (α : F G) :
.map α = α