# mathlibdocumentation

A functor between two preadditive categories is called additive provided that the induced map on hom types is a morphism of abelian groups.

# 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.

# Project: #

• Prove that a functor is additive if it preserves finite biproducts (See https://stacks.math.columbia.edu/tag/010M.)
@[class]
structure category_theory.functor.additive {C : Type u_1} {D : Type u_2} (F : C D) :
Prop
• map_zero' : (∀ {X Y : C}, F.map 0 = 0) . "obviously"
• 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
@[simp]
theorem category_theory.functor.map_zero {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] {X Y : C} :
F.map 0 = 0
@[simp]
theorem category_theory.functor.map_add {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] {X Y : C} {f g : X Y} :
F.map (f + g) = F.map f + F.map g
@[instance]
@[instance]
def category_theory.functor.comp.additive {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] {E : Type u_5} (G : D E) [G.additive] :
@[simp]
theorem category_theory.functor.map_add_hom_apply {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] {X Y : C} (f : X Y) :
def category_theory.functor.map_add_hom {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] {X Y : C} :
(X Y) →+ (F.obj X F.obj Y)

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

Equations
theorem category_theory.functor.coe_map_add_hom {C : Type u_1} {D : Type u_2} (F : C D) [F.additive] {X Y : C} :
@[simp]
theorem category_theory.functor.map_neg {C : Type u_1} {D : Type u_2} (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} (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_gsmul {C : Type u_1} {D : Type u_2} (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} (F : C D) [F.additive] {X Y : C} {α : Type u_5} (f : α → (X Y)) (s : finset α) :
F.map (∑ (a : α) in s, f a) = ∑ (a : α) in s, F.map (f a)
def category_theory.functor.map_zero_object {C : Type u_1} {D : Type u_2} (F : C D) [F.additive]  :
F.obj 0 0

An additive functor takes the zero object to the zero object (up to isomorphism).

Equations
@[simp]
theorem category_theory.functor.map_zero_object_hom {C : Type u_1} {D : Type u_2} (F : C D) [F.additive]  :
@[simp]
theorem category_theory.functor.map_zero_object_inv {C : Type u_1} {D : Type u_2} (F : C D) [F.additive]  :
@[instance]
def category_theory.functor.induced_functor_additive {C : Type u_1} {D : Type u_2} (F : C → D) :
@[instance]
def category_theory.functor.map_has_biproduct {C : Type u₁} {D : Type u₂} (F : C D) [F.additive] {J : Type v} [fintype J] [decidable_eq J] (f : J → C)  :