mathlib3 documentation

category_theory.preadditive.additive_functor

Additive Functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[class]
structure category_theory.functor.additive {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) :
Prop

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

Instances of this typeclass
source
@[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
source
@[simp]
theorem category_theory.functor.map_add_hom_apply {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.map_add_hom) = F.map
source
def category_theory.functor.map_add_hom {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} :
(X ⟶ Y) →+ (F.obj X ⟶ F.obj Y)

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

Equations
source
theorem category_theory.functor.coe_map_add_hom {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.map_add_hom) = F.map
source
@[protected, instance]
def category_theory.functor.preserves_zero_morphisms_of_additive {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] :
F.preserves_zero_morphisms
source
@[protected, instance]
def category_theory.functor.id.additive {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] :
(𝟭 C).additive
source
@[protected, instance]
def category_theory.functor.comp.additive {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] {E : Type u_5} [category_theory.category E] [category_theory.preadditive E] (G : D ⥤ E) [G.additive] :
(F ⋙ G).additive
source
@[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
source
@[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
source
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
source
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
source
@[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))
source
@[protected, instance]
def category_theory.functor.induced_functor_additive {C : Type u_1} {D : Type u_2} [category_theory.category D] [category_theory.preadditive D] (F : C → D) :
(category_theory.induced_functor F).additive
source
@[protected, instance]
def category_theory.functor.full_subcategory_inclusion_additive {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] (Z : C → Prop) :
(category_theory.full_subcategory_inclusion Z).additive
source
@[protected, instance]
def category_theory.functor.preserves_finite_biproducts_of_additive {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C ⥤ D) [F.additive] :
category_theory.limits.preserves_finite_biproducts F
Equations
source
theorem category_theory.functor.additive_of_preserves_binary_biproducts {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (F : C ⥤ D) [category_theory.limits.has_binary_biproducts C] [F.preserves_zero_morphisms] [category_theory.limits.preserves_binary_biproducts F] :
F.additive
source
@[protected, instance]
def category_theory.equivalence.inverse_additive {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] (e : C ≌ D) [e.functor.additive] :
e.inverse.additive
source
@[protected, instance]
def category_theory.AdditiveFunctor.category (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] :
category_theory.category (C ⥤+ D)
source
@[nolint]
def category_theory.AdditiveFunctor (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] :
Type (max u_3 u_4 u_1 u_2)

Bundled additive functors.

Equations
Instances for category_theory.AdditiveFunctor
source
@[protected, instance]
def category_theory.AdditiveFunctor.preadditive (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] :
category_theory.preadditive (C ⥤+ D)
Equations
source
@[protected, instance]
def category_theory.AdditiveFunctor.forget.faithful (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] :
category_theory.faithful (category_theory.AdditiveFunctor.forget C D)
source
def category_theory.AdditiveFunctor.forget (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] :
(C ⥤+ D) ⥤ C ⥤ D

An additive functor is in particular a functor.

Equations
Instances for category_theory.AdditiveFunctor.forget
source
@[protected, instance]
def category_theory.AdditiveFunctor.forget.full (C : Type u_1) (D : Type u_2) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] :
category_theory.full (category_theory.AdditiveFunctor.forget C D)
source
def category_theory.AdditiveFunctor.of {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] :
C ⥤+ D

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

Equations
source
@[simp]
theorem category_theory.AdditiveFunctor.of_fst {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] :
(category_theory.AdditiveFunctor.of F).obj = F
source
@[simp]
theorem category_theory.AdditiveFunctor.forget_obj {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) :
(category_theory.AdditiveFunctor.forget C D).obj F = F.obj
source
theorem category_theory.AdditiveFunctor.forget_obj_of {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] :
(category_theory.AdditiveFunctor.forget C D).obj (category_theory.AdditiveFunctor.of F) = F
source
@[simp]
theorem category_theory.AdditiveFunctor.forget_map {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 G : C ⥤+ D) (α : F ⟶ G) :
(category_theory.AdditiveFunctor.forget C D).map α = α
source
@[protected, instance]
def category_theory.AdditiveFunctor.forget.functor.additive {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] :
(category_theory.AdditiveFunctor.forget C D).additive
source
@[protected, instance]
def category_theory.AdditiveFunctor.field_1.functor.additive {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.obj.additive
source
@[protected, instance]
def category_theory.AdditiveFunctor.of_left_exact.full (C : Type u₁) (D : Type u₂) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] :
category_theory.full (category_theory.AdditiveFunctor.of_left_exact C D)
source
@[protected, instance]
def category_theory.AdditiveFunctor.of_left_exact.faithful (C : Type u₁) (D : Type u₂) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] :
category_theory.faithful (category_theory.AdditiveFunctor.of_left_exact C D)
source
def category_theory.AdditiveFunctor.of_left_exact (C : Type u₁) (D : Type u₂) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] :
(C ⥤ₗ D) ⥤ C ⥤+ D

Turn a left exact functor into an additive functor.

Equations
Instances for category_theory.AdditiveFunctor.of_left_exact
source
def category_theory.AdditiveFunctor.of_right_exact (C : Type u₁) (D : Type u₂) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] :
(C ⥤ᵣ D) ⥤ C ⥤+ D

Turn a right exact functor into an additive functor.

Equations
Instances for category_theory.AdditiveFunctor.of_right_exact
source
@[protected, instance]
def category_theory.AdditiveFunctor.of_right_exact.full (C : Type u₁) (D : Type u₂) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] :
category_theory.full (category_theory.AdditiveFunctor.of_right_exact C D)
source
@[protected, instance]
def category_theory.AdditiveFunctor.of_right_exact.faithful (C : Type u₁) (D : Type u₂) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] :
category_theory.faithful (category_theory.AdditiveFunctor.of_right_exact C D)
source
@[protected, instance]
def category_theory.AdditiveFunctor.of_exact.full (C : Type u₁) (D : Type u₂) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] :
category_theory.full (category_theory.AdditiveFunctor.of_exact C D)
source
@[protected, instance]
def category_theory.AdditiveFunctor.of_exact.faithful (C : Type u₁) (D : Type u₂) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] :
category_theory.faithful (category_theory.AdditiveFunctor.of_exact C D)
source
def category_theory.AdditiveFunctor.of_exact (C : Type u₁) (D : Type u₂) [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] :
(C ⥤ₑ D) ⥤ C ⥤+ D

Turn an exact functor into an additive functor.

Equations
Instances for category_theory.AdditiveFunctor.of_exact
source
@[simp]
theorem category_theory.AdditiveFunctor.of_left_exact_obj_fst {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] (F : C ⥤ₗ D) :
((category_theory.AdditiveFunctor.of_left_exact C D).obj F).obj = F.obj
source
@[simp]
theorem category_theory.AdditiveFunctor.of_right_exact_obj_fst {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] (F : C ⥤ᵣ D) :
((category_theory.AdditiveFunctor.of_right_exact C D).obj F).obj = F.obj
source
@[simp]
theorem category_theory.AdditiveFunctor.of_exact_obj_fst {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] (F : C ⥤ₑ D) :
((category_theory.AdditiveFunctor.of_exact C D).obj F).obj = F.obj
source
@[simp]
theorem category_theory.Additive_Functor.of_left_exact_map {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] {F G : C ⥤ₗ D} (α : F ⟶ G) :
(category_theory.AdditiveFunctor.of_left_exact C D).map α = α
source
@[simp]
theorem category_theory.Additive_Functor.of_right_exact_map {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] {F G : C ⥤ᵣ D} (α : F ⟶ G) :
(category_theory.AdditiveFunctor.of_right_exact C D).map α = α
source
@[simp]
theorem category_theory.Additive_Functor.of_exact_map {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] [category_theory.preadditive C] [category_theory.preadditive D] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [category_theory.limits.has_binary_biproducts C] {F G : C ⥤ₑ D} (α : F ⟶ G) :
(category_theory.AdditiveFunctor.of_exact C D).map α = α