Theorems · Theorem · category theory

CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{z, w} D]
  [inst_2 : 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 ⋯)

Defined in

Mathlib.CategoryTheory.Abelian.FunctorCategory

Cited by

0 results in Mathlib

Foundations

Depth 44 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Abelian