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.

class CategoryTheory.Functor.Additive {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) : Prop

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

@[simp]

theorem CategoryTheory.Functor.map_add {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X Y : C} {f g : X ⟶ Y} : F.map (f + g) = F.map f + F.map g

def CategoryTheory.Functor.mapAddHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X Y : C} : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)

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

@[simp]

theorem CategoryTheory.Functor.mapAddHom_apply {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X Y : C} (f : X ⟶ Y) : F.mapAddHom f = F.map f

theorem CategoryTheory.Functor.coe_mapAddHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X Y : C} : ⇑F.mapAddHom = F.map

@[instance 100]

instance CategoryTheory.Functor.preservesZeroMorphisms_of_additive {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : F.PreservesZeroMorphisms

instance CategoryTheory.Functor.instAdditiveId {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] : (Functor.id C).Additive

instance CategoryTheory.Functor.instAdditiveComp {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {E : Type u_4} [Category.{v_4, u_4} E] [Preadditive E] (G : Functor D E) [G.Additive] : (F.comp G).Additive

instance CategoryTheory.Functor.instAdditiveObjEvaluation {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {J : Type u_4} [Category.{v_4, u_4} J] (j : J) : ((evaluation J C).obj j).Additive

@[simp]

theorem CategoryTheory.Functor.map_neg {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X Y : C} {f 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X 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} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X Y : C} {α : Type u_4} (f : α → (X ⟶ Y)) (s : Finset α) : F.map (∑ a ∈ s, f a) = ∑ a ∈ s, F.map (f a)

theorem CategoryTheory.Functor.additive_of_iso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] {F : Functor C D} [F.Additive] {G : Functor C D} (e : F ≅ G) : G.Additive

theorem CategoryTheory.Functor.additive_of_full_essSurj_comp {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [Preadditive C] [Preadditive D] [Preadditive E] (F : Functor C D) [F.Additive] [F.Full] [F.EssSurj] (G : Functor D E) [(F.comp G).Additive] : G.Additive

theorem CategoryTheory.Functor.additive_of_comp_faithful {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [Preadditive C] [Preadditive D] [Preadditive E] (F : Functor C D) (G : Functor D E) [G.Additive] [(F.comp G).Additive] [G.Faithful] : F.Additive

theorem CategoryTheory.Functor.hasZeroObject_of_additive {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] [Limits.HasZeroObject C] : Limits.HasZeroObject D

instance CategoryTheory.Functor.inducedFunctor_additive {C : Type u_1} {D : Type u_2} [Category.{v_1, u_2} D] [Preadditive D] (F : C → D) : (inducedFunctor F).Additive

instance CategoryTheory.Functor.fullSubcategoryInclusion_additive {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] (Z : ObjectProperty C) : Z.ι.Additive

instance CategoryTheory.Functor.instAdditiveFullSubcategoryLift {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor D C) [F.Additive] (P : ObjectProperty C) (hF : ∀ (X : D), P (F.obj X)) : (P.lift F hF).Additive

@[instance 100]

instance CategoryTheory.Functor.preservesFiniteBiproductsOfAdditive {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : Limits.PreservesFiniteBiproducts F

@[instance 100]

instance CategoryTheory.Functor.preservesFiniteCoproductsOfAdditive {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : Limits.PreservesFiniteCoproducts F

@[instance 100]

instance CategoryTheory.Functor.preservesFiniteProductsOfAdditive {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : Limits.PreservesFiniteProducts F

theorem CategoryTheory.Functor.additive_of_preservesBinaryBiproducts {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] (F : Functor C D) [Limits.HasBinaryBiproducts C] [F.PreservesZeroMorphisms] [Limits.PreservesBinaryBiproducts F] : F.Additive

theorem CategoryTheory.Functor.additive_of_preserves_binary_products {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] (F : Functor C D) [Limits.HasBinaryProducts C] [Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F] [F.PreservesZeroMorphisms] : F.Additive

instance CategoryTheory.Equivalence.inverse_additive {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (e : C ≌ D) [e.functor.Additive] : e.inverse.Additive

def CategoryTheory.additiveFunctor (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] : ObjectProperty (Functor C D)

The additiveness of a functor, as a property of objects in C ⥤ D.

theorem CategoryTheory.additiveFunctor_iff {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) : additiveFunctor C D F ↔ F.Additive

@[reducible, inline]

abbrev CategoryTheory.AdditiveFunctor (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] : Type (max (max (max u_1 u_2) v_1) v_2)

Bundled additive functors.

instance CategoryTheory.instAdditiveObjFunctorAdditiveFunctor (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : C ⥤+ D) : F.obj.Additive

def CategoryTheory.«term_⥤+_» : Lean.TrailingParserDescr

the category of additive functors is denoted C ⥤+ D

@[reducible, inline]

abbrev CategoryTheory.AdditiveFunctor.forget (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] : Functor (C ⥤+ D) (Functor C D)

An additive functor is in particular a functor.

def CategoryTheory.AdditiveFunctor.of {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : C ⥤+ D

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

@[simp]

theorem CategoryTheory.AdditiveFunctor.of_obj {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : (of F).obj = F

@[simp]

theorem CategoryTheory.AdditiveFunctor.of_fst {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : (of F).obj = F

@[simp]

theorem CategoryTheory.AdditiveFunctor.forget_obj {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : C ⥤+ D) : (forget C D).obj F = F.obj

theorem CategoryTheory.AdditiveFunctor.forget_obj_of {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : (forget C D).obj (of F) = F

@[simp]

theorem CategoryTheory.AdditiveFunctor.forget_map {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F G : C ⥤+ D) (α : F ⟶ G) : (forget C D).map α = α.hom

instance CategoryTheory.instAdditiveAdditiveFunctorFunctorForget {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] : (AdditiveFunctor.forget C D).Additive

instance CategoryTheory.instAdditiveObjFunctorAdditiveFunctor_1 {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : C ⥤+ D) : F.obj.Additive

theorem CategoryTheory.leftExactFunctor_le_additiveFunctor (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] : leftExactFunctor C D ≤ additiveFunctor C D

theorem CategoryTheory.rightExactFunctor_le_additiveFunctor (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] : rightExactFunctor C D ≤ additiveFunctor C D

theorem CategoryTheory.exactFunctor_le_additiveFunctor (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] : exactFunctor C D ≤ additiveFunctor C D

@[reducible, inline]

abbrev CategoryTheory.AdditiveFunctor.ofLeftExact (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] : Functor (C ⥤ₗ D) (C ⥤+ D)

Turn a left exact functor into an additive functor.

@[reducible, inline]

abbrev CategoryTheory.AdditiveFunctor.ofRightExact (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] : Functor (C ⥤ᵣ D) (C ⥤+ D)

Turn a right exact functor into an additive functor.

@[reducible, inline]

abbrev CategoryTheory.AdditiveFunctor.ofExact (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] : Functor (C ⥤ₑ D) (C ⥤+ D)

Turn an exact functor into an additive functor.

@[simp]

theorem CategoryTheory.AdditiveFunctor.ofLeftExact_obj_fst {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] (F : C ⥤ₗ D) : ((ofLeftExact C D).obj F).obj = F.obj

@[simp]

theorem CategoryTheory.AdditiveFunctor.ofRightExact_obj_fst {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] (F : C ⥤ᵣ D) : ((ofRightExact C D).obj F).obj = F.obj

@[simp]

theorem CategoryTheory.AdditiveFunctor.ofExact_obj_fst {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] (F : C ⥤ₑ D) : ((ofExact C D).obj F).obj = F.obj

@[simp]

theorem CategoryTheory.AdditiveFunctor.ofLeftExact_map_hom {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] {F G : C ⥤ₗ D} (α : F ⟶ G) : ((ofLeftExact C D).map α).hom = α.hom

@[simp]

theorem CategoryTheory.AdditiveFunctor.ofRightExact_map_hom {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] {F G : C ⥤ᵣ D} (α : F ⟶ G) : ((ofRightExact C D).map α).hom = α.hom

@[simp]

theorem CategoryTheory.AdditiveFunctor.ofExact_map_hom {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] {F G : C ⥤ₑ D} (α : F ⟶ G) : ((ofExact C D).map α).hom = α.hom

@[deprecated CategoryTheory.AdditiveFunctor.ofLeftExact_map_hom (since := "2025-12-18")]

theorem CategoryTheory.AdditiveFunctor.ofLeftExact_map {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] {F G : C ⥤ₗ D} (α : F ⟶ G) : ((ofLeftExact C D).map α).hom = α.hom

Alias of CategoryTheory.AdditiveFunctor.ofLeftExact_map_hom.

@[deprecated CategoryTheory.AdditiveFunctor.ofRightExact_map_hom (since := "2025-12-18")]

theorem CategoryTheory.AdditiveFunctor.ofRightExact_map {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] {F G : C ⥤ᵣ D} (α : F ⟶ G) : ((ofRightExact C D).map α).hom = α.hom

Alias of CategoryTheory.AdditiveFunctor.ofRightExact_map_hom.

@[deprecated CategoryTheory.AdditiveFunctor.ofExact_map_hom (since := "2025-12-18")]

theorem CategoryTheory.AdditiveFunctor.ofExact_map {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [Limits.HasBinaryBiproducts C] {F G : C ⥤ₑ D} (α : F ⟶ G) : ((ofExact C D).map α).hom = α.hom

Alias of CategoryTheory.AdditiveFunctor.ofExact_map_hom.