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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) : Prop

• 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

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

@[simp]

theorem CategoryTheory.Functor.map_add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {X : C} {Y : C} (f : X ⟶ Y) : ↑(CategoryTheory.Functor.mapAddHom F) f = F.map f

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

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

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

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

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

instance CategoryTheory.Functor.instAdditiveComp {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] {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] [CategoryTheory.Preadditive E] (G : CategoryTheory.Functor D E) [CategoryTheory.Functor.Additive G] : CategoryTheory.Functor.Additive (CategoryTheory.Functor.comp F G)

@[simp]

theorem CategoryTheory.Functor.map_neg {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] {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} [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 α) : F.map (Finset.sum s fun a => f a) = Finset.sum s fun a => F.map (f a)

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

instance CategoryTheory.Functor.fullSubcategoryInclusion_additive {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (Z : C → Prop) : CategoryTheory.Functor.Additive (CategoryTheory.fullSubcategoryInclusion Z)

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

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

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

def CategoryTheory.AdditiveFunctor (C : Type u_1) (D : Type u_2) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] : Type (max (max (max u_1 u_2) u_3) u_4)

Bundled additive functors.

instance CategoryTheory.instCategoryAdditiveFunctor (C : Type u_1) (D : Type u_2) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] : CategoryTheory.Category.{max u_1 u_4, max (max (max u_4 u_3) u_1) u_2} (C ⥤+ D)

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

the category of additive functors is denoted C ⥤+ D

instance CategoryTheory.instPreadditiveAdditiveFunctorInstCategoryAdditiveFunctor (C : Type u_1) (D : Type u_2) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] : CategoryTheory.Preadditive (C ⥤+ D)

def CategoryTheory.AdditiveFunctor.forget (C : Type u_1) (D : Type u_2) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] : CategoryTheory.Functor (C ⥤+ D) (CategoryTheory.Functor C D)

An additive functor is in particular a functor.

instance CategoryTheory.instFullAdditiveFunctorInstCategoryAdditiveFunctorFunctorCategoryForget (C : Type u_1) (D : Type u_2) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] : CategoryTheory.Full (CategoryTheory.AdditiveFunctor.forget C D)

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

instance CategoryTheory.instAdditiveAdditiveFunctorFunctorInstCategoryAdditiveFunctorCategoryInstPreadditiveAdditiveFunctorInstCategoryAdditiveFunctorFunctorCategoryPreadditiveForget {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] : CategoryTheory.Functor.Additive (CategoryTheory.AdditiveFunctor.forget C D)

instance CategoryTheory.instAdditiveObjFunctor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : C ⥤+ D) : CategoryTheory.Functor.Additive F.obj

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

Turn a left exact functor into an additive functor.

instance CategoryTheory.instFullLeftExactFunctorInstCategoryLeftExactFunctorAdditiveFunctorInstCategoryAdditiveFunctorOfLeftExact (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Full (CategoryTheory.AdditiveFunctor.ofLeftExact C D)

instance CategoryTheory.instFaithfulLeftExactFunctorInstCategoryLeftExactFunctorAdditiveFunctorInstCategoryAdditiveFunctorOfLeftExact (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Faithful (CategoryTheory.AdditiveFunctor.ofLeftExact C D)

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

Turn a right exact functor into an additive functor.

instance CategoryTheory.instFullRightExactFunctorInstCategoryRightExactFunctorAdditiveFunctorInstCategoryAdditiveFunctorOfRightExact (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Full (CategoryTheory.AdditiveFunctor.ofRightExact C D)

instance CategoryTheory.instFaithfulRightExactFunctorInstCategoryRightExactFunctorAdditiveFunctorInstCategoryAdditiveFunctorOfRightExact (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Faithful (CategoryTheory.AdditiveFunctor.ofRightExact C D)

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

Turn an exact functor into an additive functor.

instance CategoryTheory.instFullExactFunctorInstCategoryExactFunctorAdditiveFunctorInstCategoryAdditiveFunctorOfExact (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Full (CategoryTheory.AdditiveFunctor.ofExact C D)

instance CategoryTheory.instFaithfulExactFunctorInstCategoryExactFunctorAdditiveFunctorInstCategoryAdditiveFunctorOfExact (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Faithful (CategoryTheory.AdditiveFunctor.ofExact C D)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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