Theorems · Definition · category theory

CategoryTheory.AdditiveFunctor.ofExact

(C : Type u₁) →
  (D : Type u₂) →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : 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.

Defined in

Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Cited by

2 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.PreadditiveCategoryTheory.Limits.HasZeroObjectCategoryTheory.Limits.HasZeroObjectCategoryTheory.Limits.HasBinaryBiproducts