If D is abelian, then the functor category C ⥤ D is also abelian. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[simp]
theorem
category_theory.abelian.functor_category.coimage_obj_iso_hom
{C : Type (max v u)}
[category_theory.category C]
{D : Type w}
[category_theory.category D]
[category_theory.abelian D]
{F G : C ⥤ D}
(α : F ⟶ G)
(X : C) :
(category_theory.abelian.functor_category.coimage_obj_iso α X).hom = (category_theory.limits.preserves_cokernel.iso ((category_theory.evaluation C D).obj X) (category_theory.limits.kernel.ι α)).hom ≫ category_theory.limits.cokernel.map ((category_theory.limits.kernel.ι α).app X) (category_theory.limits.kernel.ι (α.app X)) (category_theory.limits.kernel_comparison α ((category_theory.evaluation C D).obj X)) (𝟙 (F.obj X)) _
@[simp]
theorem
category_theory.abelian.functor_category.coimage_obj_iso_inv
{C : Type (max v u)}
[category_theory.category C]
{D : Type w}
[category_theory.category D]
[category_theory.abelian D]
{F G : C ⥤ D}
(α : F ⟶ G)
(X : C) :
(category_theory.abelian.functor_category.coimage_obj_iso α X).inv = category_theory.limits.cokernel.map (category_theory.limits.kernel.ι (α.app X)) ((category_theory.limits.kernel.ι α).app X) (category_theory.limits.preserves_kernel.iso ((category_theory.evaluation C D).obj X) α).inv (𝟙 (F.obj X)) _ ≫ category_theory.limits.cokernel_comparison (category_theory.limits.kernel.ι α) ((category_theory.evaluation C D).obj X)
noncomputable
def
category_theory.abelian.functor_category.coimage_obj_iso
{C : Type (max v u)}
[category_theory.category C]
{D : Type w}
[category_theory.category D]
[category_theory.abelian D]
{F G : C ⥤ D}
(α : F ⟶ G)
(X : C) :
The abelian coimage in a functor category can be calculated componentwise.
Equations
- category_theory.abelian.functor_category.coimage_obj_iso α X = category_theory.limits.preserves_cokernel.iso ((category_theory.evaluation C D).obj X) (category_theory.limits.kernel.ι α) ≪≫ category_theory.limits.cokernel.map_iso (((category_theory.evaluation C D).obj X).map (category_theory.limits.kernel.ι α)) (category_theory.limits.kernel.ι (α.app X)) (category_theory.limits.preserves_kernel.iso ((category_theory.evaluation C D).obj X) α) (category_theory.iso.refl (((category_theory.evaluation C D).obj X).obj F)) _
noncomputable
def
category_theory.abelian.functor_category.image_obj_iso
{C : Type (max v u)}
[category_theory.category C]
{D : Type w}
[category_theory.category D]
[category_theory.abelian D]
{F G : C ⥤ D}
(α : F ⟶ G)
(X : C) :
The abelian image in a functor category can be calculated componentwise.
Equations
- category_theory.abelian.functor_category.image_obj_iso α X = category_theory.limits.preserves_kernel.iso ((category_theory.evaluation C D).obj X) (category_theory.limits.cokernel.π α) ≪≫ category_theory.limits.kernel.map_iso (((category_theory.evaluation C D).obj X).map (category_theory.limits.cokernel.π α)) (category_theory.limits.cokernel.π (α.app X)) (category_theory.iso.refl (((category_theory.evaluation C D).obj X).obj G)) (category_theory.limits.preserves_cokernel.iso ((category_theory.evaluation C D).obj X) α) _
@[simp]
theorem
category_theory.abelian.functor_category.image_obj_iso_hom
{C : Type (max v u)}
[category_theory.category C]
{D : Type w}
[category_theory.category D]
[category_theory.abelian D]
{F G : C ⥤ D}
(α : F ⟶ G)
(X : C) :
(category_theory.abelian.functor_category.image_obj_iso α X).hom = category_theory.limits.kernel_comparison (category_theory.limits.cokernel.π α) ((category_theory.evaluation C D).obj X) ≫ category_theory.limits.kernel.map ((category_theory.limits.cokernel.π α).app X) (category_theory.limits.cokernel.π (α.app X)) (𝟙 (G.obj X)) (category_theory.limits.preserves_cokernel.iso ((category_theory.evaluation C D).obj X) α).hom _
@[simp]
theorem
category_theory.abelian.functor_category.image_obj_iso_inv
{C : Type (max v u)}
[category_theory.category C]
{D : Type w}
[category_theory.category D]
[category_theory.abelian D]
{F G : C ⥤ D}
(α : F ⟶ G)
(X : C) :
(category_theory.abelian.functor_category.image_obj_iso α X).inv = category_theory.limits.kernel.map (category_theory.limits.cokernel.π (α.app X)) ((category_theory.limits.cokernel.π α).app X) (𝟙 (G.obj X)) (category_theory.limits.cokernel_comparison α ((category_theory.evaluation C D).obj X)) _ ≫ (category_theory.limits.preserves_kernel.iso ((category_theory.evaluation C D).obj X) (category_theory.limits.cokernel.π α)).inv
theorem
category_theory.abelian.functor_category.coimage_image_comparison_app
{C : Type (max v u)}
[category_theory.category C]
{D : Type w}
[category_theory.category D]
[category_theory.abelian D]
{F G : C ⥤ D}
(α : F ⟶ G)
(X : C) :
theorem
category_theory.abelian.functor_category.coimage_image_comparison_app'
{C : Type (max v u)}
[category_theory.category C]
{D : Type w}
[category_theory.category D]
[category_theory.abelian D]
{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)}
[category_theory.category C]
{D : Type w}
[category_theory.category D]
[category_theory.abelian D]
{F G : C ⥤ D}
(α : F ⟶ G) :
@[protected, instance]
noncomputable
def
category_theory.abelian.functor_category_abelian
{C : Type (max v u)}
[category_theory.category C]
{D : Type w}
[category_theory.category D]
[category_theory.abelian D] :
category_theory.abelian (C ⥤ D)
@[protected, instance]
noncomputable
def
category_theory.abelian.functor_category_abelian'
{C : Type u}
[category_theory.small_category C]
{D : Type (u+1)}
[category_theory.large_category D]
[category_theory.abelian D] :
category_theory.abelian (C ⥤ D)
A variant with specialized universes for a common case.