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

noncomputable def CategoryTheory.Abelian.FunctorCategory.coimageObjIso {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{z, w} D] [Abelian D] {F G : Functor C D} (α : F ⟶ G) (X : C) : (Abelian.coimage α).obj X ≅ Abelian.coimage (α.app X)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{z, w} D] [Abelian D] {F G : Functor C D} (α : F ⟶ G) (X : C) : (coimageObjIso α X).inv = CategoryStruct.comp (Limits.cokernel.map (Limits.kernel.ι (α.app X)) ((Limits.kernel.ι α).app X) (Limits.PreservesKernel.iso ((evaluation C D).obj X) α).inv (CategoryStruct.id (F.obj X)) ⋯) (Limits.cokernelComparison (Limits.kernel.ι α) ((evaluation C D).obj X))

@[simp]

theorem CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{z, w} D] [Abelian D] {F G : Functor C D} (α : F ⟶ G) (X : C) : (coimageObjIso α X).hom = CategoryStruct.comp (Limits.PreservesCokernel.iso ((evaluation C D).obj X) (Limits.kernel.ι α)).hom (Limits.cokernel.map ((Limits.kernel.ι α).app X) (Limits.kernel.ι (α.app X)) (Limits.kernelComparison α ((evaluation C D).obj X)) (CategoryStruct.id (F.obj X)) ⋯)

noncomputable def CategoryTheory.Abelian.FunctorCategory.imageObjIso {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{z, w} D] [Abelian D] {F G : Functor C D} (α : F ⟶ G) (X : C) : (Abelian.image α).obj X ≅ Abelian.image (α.app X)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{z, w} D] [Abelian D] {F G : Functor C D} (α : F ⟶ G) (X : C) : (imageObjIso α X).inv = CategoryStruct.comp (Limits.kernel.map (Limits.cokernel.π (α.app X)) ((Limits.cokernel.π α).app X) (CategoryStruct.id (G.obj X)) (Limits.cokernelComparison α ((evaluation C D).obj X)) ⋯) (Limits.PreservesKernel.iso ((evaluation C D).obj X) (Limits.cokernel.π α)).inv

@[simp]

theorem CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{z, w} D] [Abelian D] {F G : Functor C D} (α : F ⟶ G) (X : C) : (imageObjIso α X).hom = CategoryStruct.comp (Limits.kernelComparison (Limits.cokernel.π α) ((evaluation C D).obj X)) (Limits.kernel.map ((Limits.cokernel.π α).app X) (Limits.cokernel.π (α.app X)) (CategoryStruct.id (G.obj X)) (Limits.PreservesCokernel.iso ((evaluation C D).obj X) α).hom ⋯)

theorem CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{z, w} D] [Abelian D] {F G : Functor C D} (α : F ⟶ G) (X : C) : coimageImageComparison (α.app X) = CategoryStruct.comp (coimageObjIso α X).inv (CategoryStruct.comp ((coimageImageComparison α).app X) (imageObjIso α X).hom)

theorem CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app' {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{z, w} D] [Abelian D] {F G : Functor C D} (α : F ⟶ G) (X : C) : (coimageImageComparison α).app X = CategoryStruct.comp (coimageObjIso α X).hom (CategoryStruct.comp (coimageImageComparison (α.app X)) (imageObjIso α X).inv)

instance CategoryTheory.Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{z, w} D] [Abelian D] {F G : Functor C D} (α : F ⟶ G) : IsIso (coimageImageComparison α)

@[implicit_reducible]

noncomputable instance CategoryTheory.Abelian.functorCategoryAbelian {C : Type u} [Category.{v, u} C] {D : Type w} [Category.{z, w} D] [Abelian D] : Abelian (Functor C D)

Equations

• CategoryTheory.Abelian.functorCategoryAbelian = CategoryTheory.Abelian.ofCoimageImageComparisonIsIso