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

def CategoryTheory.Abelian.FunctorCategory.coimageObjIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C) : (CategoryTheory.Abelian.coimage α).obj X ≅ CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C) : (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map (CategoryTheory.Limits.kernel.ι (α.app X)) ((CategoryTheory.Limits.kernel.ι α).app X) (CategoryTheory.Limits.PreservesKernel.iso ((CategoryTheory.evaluation C D).obj X) α).inv (CategoryTheory.CategoryStruct.id (F.obj X)) ⋯) (CategoryTheory.Limits.cokernelComparison (CategoryTheory.Limits.kernel.ι α) ((CategoryTheory.evaluation C D).obj X))

@[simp]

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

def CategoryTheory.Abelian.FunctorCategory.imageObjIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C) : (CategoryTheory.Abelian.image α).obj X ≅ CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C) : (CategoryTheory.Abelian.FunctorCategory.imageObjIso α X).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map (CategoryTheory.Limits.cokernel.π (α.app X)) ((CategoryTheory.Limits.cokernel.π α).app X) (CategoryTheory.CategoryStruct.id (G.obj X)) (CategoryTheory.Limits.cokernelComparison α ((CategoryTheory.evaluation C D).obj X)) ⋯) (CategoryTheory.Limits.PreservesKernel.iso ((CategoryTheory.evaluation C D).obj X) (CategoryTheory.Limits.cokernel.π α)).inv

@[simp]

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

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