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 : CategoryTheory.Functor C D}
{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.
Instances For
@[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 : CategoryTheory.Functor C D}
{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 : CategoryTheory.Functor C D}
{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 : CategoryTheory.Functor C D}
{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.
Instances For
@[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 : CategoryTheory.Functor C D}
{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 : CategoryTheory.Functor C D}
{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 : CategoryTheory.Functor C D}
{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 : CategoryTheory.Functor C D}
{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 : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(α : F ⟶ G)
:
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]
:
Equations
- CategoryTheory.Abelian.functorCategoryAbelian = CategoryTheory.Abelian.ofCoimageImageComparisonIsIso