Documentation

Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

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.

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} [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} [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} [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) [F.Additive] {X : C} {Y : C} {f : X Y} {g : X Y} :
    F.map (f + g) = F.map f + F.map g
    @[simp]

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

    Equations
    Instances For
      @[simp]
      @[simp]
      theorem CategoryTheory.Functor.map_sub {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) [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} [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) [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} [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) [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} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] {X : C} {Y : C} {α : Type u_4} (f : α(X Y)) (s : Finset α) :
      F.map (as, f a) = as, F.map (f a)

      Bundled additive functors.

      Equations
      Instances For

        the category of additive functors is denoted C ⥤+ D

        Equations
        Instances For

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

          Equations
          Instances For