# mathlibdocumentation

category_theory.abelian.functor_category

# If D is abelian, then the functor category C ⥤ D is also abelian. #

@[simp]
theorem category_theory.abelian.functor_category.coimage_obj_iso_hom {C : Type (max v u)} {D : Type w} {F G : C D} (α : F G) (X : C) :
@[simp]
theorem category_theory.abelian.functor_category.coimage_obj_iso_inv {C : Type (max v u)} {D : Type w} {F G : C D} (α : F G) (X : C) :
noncomputable def category_theory.abelian.functor_category.coimage_obj_iso {C : Type (max v u)} {D : Type w} {F G : C D} (α : F G) (X : C) :

The abelian coimage in a functor category can be calculated componentwise.

Equations
noncomputable def category_theory.abelian.functor_category.image_obj_iso {C : Type (max v u)} {D : Type w} {F G : C D} (α : F G) (X : C) :

The abelian image in a functor category can be calculated componentwise.

Equations
@[simp]
theorem category_theory.abelian.functor_category.image_obj_iso_hom {C : Type (max v u)} {D : Type w} {F G : C D} (α : F G) (X : C) :
@[simp]
theorem category_theory.abelian.functor_category.image_obj_iso_inv {C : Type (max v u)} {D : Type w} {F G : C D} (α : F G) (X : C) :
theorem category_theory.abelian.functor_category.coimage_image_comparison_app {C : Type (max v u)} {D : Type w} {F G : C D} (α : F G) (X : C) :
theorem category_theory.abelian.functor_category.coimage_image_comparison_app' {C : Type (max v u)} {D : Type w} {F G : C D} (α : F G) (X : C) :
@[protected, instance]
def category_theory.abelian.functor_category.functor_category_is_iso_coimage_image_comparison {C : Type (max v u)} {D : Type w} {F G : C D} (α : F G) :
@[protected, instance]
noncomputable def category_theory.abelian.functor_category_abelian {C : Type (max v u)} {D : Type w}  :
Equations
@[protected, instance]
noncomputable def category_theory.abelian.functor_category_abelian' {C : Type u} {D : Type (u+1)}  :

A variant with specialized universes for a common case.

Equations