mathlib documentation

category_theory.preadditive.additive_functor

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]
  • map_add' : (∀ {X Y : C} {f g : X Y}, F.map (f + g) = F.map f + F.map g) . "obviously"

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

Instances of this typeclass
@[simp]
theorem category_theory.functor.map_add {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C D) [F.additive] {X Y : C} {f g : X Y} :
F.map (f + g) = F.map f + F.map g

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

Equations
@[simp]
theorem category_theory.functor.map_neg {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C D) [F.additive] {X Y : C} {f : X Y} :
F.map (-f) = -F.map f
@[simp]
theorem category_theory.functor.map_sub {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C D) [F.additive] {X Y : C} {f g : X Y} :
F.map (f - g) = F.map f - F.map g
theorem category_theory.functor.map_nsmul {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C D) [F.additive] {X Y : C} {f : X Y} {n : } :
F.map (n f) = n F.map f
theorem category_theory.functor.map_zsmul {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C D) [F.additive] {X Y : C} {f : X Y} {r : } :
F.map (r f) = r F.map f
@[simp]
theorem category_theory.functor.map_sum {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C D) [F.additive] {X Y : C} {α : Type u_5} (f : α → (X Y)) (s : finset α) :
F.map (s.sum (λ (a : α), f a)) = s.sum (λ (a : α), F.map (f a))
@[nolint]

Bundled additive functors.

Equations
Instances for category_theory.AdditiveFunctor

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

Equations