Preserving (co)kernels #
Constructions to relate the notions of preserving (co)kernels and reflecting (co)kernels to concrete (co)forks.
In particular, we show that kernel_comparison f g G is an isomorphism iff G preserves
the limit of the parallel pair f,0, as well as the dual result.
@[simp]
theorem
CategoryTheory.Limits.KernelFork.map_condition
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : KernelFork f)
(G : Functor C D)
[G.PreservesZeroMorphisms]
:
CategoryStruct.comp (G.map (Fork.ι c)) (G.map f) = 0
@[simp]
theorem
CategoryTheory.Limits.KernelFork.map_condition_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : KernelFork f)
(G : Functor C D)
[G.PreservesZeroMorphisms]
{Z : D}
(h : G.obj Y ⟶ Z)
:
CategoryStruct.comp (G.map (Fork.ι c)) (CategoryStruct.comp (G.map f) h) = CategoryStruct.comp 0 h
def
CategoryTheory.Limits.KernelFork.map
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : KernelFork f)
(G : Functor C D)
[G.PreservesZeroMorphisms]
:
KernelFork (G.map f)
A kernel fork for f is mapped to a kernel fork for G.map f if G is a functor
which preserves zero morphisms.
Equations
- c.map G = CategoryTheory.Limits.KernelFork.ofι (G.map (CategoryTheory.Limits.Fork.ι c)) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Limits.KernelFork.map_ι
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : KernelFork f)
(G : Functor C D)
[G.PreservesZeroMorphisms]
:
def
CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : KernelFork f)
(G : Functor C D)
[G.PreservesZeroMorphisms]
:
The underlying cone of a kernel fork is mapped to a limit cone if and only if the mapped kernel fork is limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.KernelFork.mapIsLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : KernelFork f)
(hc : IsLimit c)
(G : Functor C D)
[G.PreservesZeroMorphisms]
[PreservesLimit (parallelPair f 0) G]
:
IsLimit (c.map G)
A limit kernel fork is mapped to a limit kernel fork by a functor G when this functor
preserves the corresponding limit.
Equations
- c.mapIsLimit hc G = (c.isLimitMapConeEquiv G) (CategoryTheory.Limits.isLimitOfPreserves G hc)
Instances For
def
CategoryTheory.Limits.isLimitMapConeForkEquiv'
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y Z : C}
{f : X ⟶ Y}
{h : Z ⟶ X}
(w : CategoryStruct.comp h f = 0)
:
IsLimit (G.mapCone (KernelFork.ofι h w)) ≃ IsLimit (KernelFork.ofι (G.map h) ⋯)
The map of a kernel fork is a limit iff
the kernel fork consisting of the mapped morphisms is a limit.
This essentially lets us commute KernelFork.ofι with Functor.mapCone.
This is a variant of isLimitMapConeForkEquiv for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
Equations
- CategoryTheory.Limits.isLimitMapConeForkEquiv' G w = (CategoryTheory.Limits.KernelFork.ofι h w).isLimitMapConeEquiv G
Instances For
def
CategoryTheory.Limits.isLimitForkMapOfIsLimit'
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y Z : C}
{f : X ⟶ Y}
{h : Z ⟶ X}
(w : CategoryStruct.comp h f = 0)
[PreservesLimit (parallelPair f 0) G]
(l : IsLimit (KernelFork.ofι h w))
:
IsLimit (KernelFork.ofι (G.map h) ⋯)
The property of preserving kernels expressed in terms of kernel forks.
This is a variant of isLimitForkMapOfIsLimit for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
Equations
Instances For
def
CategoryTheory.Limits.isLimitOfHasKernelOfPreservesLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasKernel f]
[PreservesLimit (parallelPair f 0) G]
:
If G preserves kernels and C has them, then the fork constructed of the mapped morphisms of
a kernel fork is a limit.
Equations
Instances For
instance
CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasKernel f]
[PreservesLimit (parallelPair f 0) G]
:
HasKernel (G.map f)
theorem
CategoryTheory.Limits.PreservesKernel.of_iso_comparison
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasKernel f]
[HasKernel (G.map f)]
[i : IsIso (kernelComparison f G)]
:
PreservesLimit (parallelPair f 0) G
If the kernel comparison map for G at f is an isomorphism, then G preserves the
kernel of f.
def
CategoryTheory.Limits.PreservesKernel.iso
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasKernel f]
[HasKernel (G.map f)]
[PreservesLimit (parallelPair f 0) G]
:
If G preserves the kernel of f, then the kernel comparison map for G at f is
an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PreservesKernel.iso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasKernel f]
[HasKernel (G.map f)]
[PreservesLimit (parallelPair f 0) G]
:
(iso G f).hom = kernelComparison f G
instance
CategoryTheory.Limits.instIsIsoKernelComparison
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasKernel f]
[HasKernel (G.map f)]
[PreservesLimit (parallelPair f 0) G]
:
IsIso (kernelComparison f G)
theorem
CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasKernel f]
[HasKernel (G.map f)]
[PreservesLimit (parallelPair f 0) G]
{X' Y' : C}
(g : X' ⟶ Y')
[HasKernel g]
[HasKernel (G.map g)]
[PreservesLimit (parallelPair g 0) G]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : CategoryStruct.comp f q = CategoryStruct.comp p g)
:
CategoryStruct.comp (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) (PreservesKernel.iso G g).inv = CategoryStruct.comp (PreservesKernel.iso G f).inv (G.map (kernel.map f g p q hpq))
theorem
CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasKernel f]
[HasKernel (G.map f)]
[PreservesLimit (parallelPair f 0) G]
{X' Y' : C}
(g : X' ⟶ Y')
[HasKernel g]
[HasKernel (G.map g)]
[PreservesLimit (parallelPair g 0) G]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : CategoryStruct.comp f q = CategoryStruct.comp p g)
{Z : D}
(h : G.obj (kernel g) ⟶ Z)
:
CategoryStruct.comp (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
(CategoryStruct.comp (PreservesKernel.iso G g).inv h) = CategoryStruct.comp (PreservesKernel.iso G f).inv (CategoryStruct.comp (G.map (kernel.map f g p q hpq)) h)
@[simp]
theorem
CategoryTheory.Limits.CokernelCofork.map_condition
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : CokernelCofork f)
(G : Functor C D)
[G.PreservesZeroMorphisms]
:
CategoryStruct.comp (G.map f) (G.map (Cofork.π c)) = 0
@[simp]
theorem
CategoryTheory.Limits.CokernelCofork.map_condition_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : CokernelCofork f)
(G : Functor C D)
[G.PreservesZeroMorphisms]
{Z : D}
(h : G.obj (((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.one) ⟶ Z)
:
CategoryStruct.comp (G.map f) (CategoryStruct.comp (G.map (Cofork.π c)) h) = CategoryStruct.comp 0 h
def
CategoryTheory.Limits.CokernelCofork.map
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : CokernelCofork f)
(G : Functor C D)
[G.PreservesZeroMorphisms]
:
CokernelCofork (G.map f)
A cokernel cofork for f is mapped to a cokernel cofork for G.map f if G is a functor
which preserves zero morphisms.
Equations
- c.map G = CategoryTheory.Limits.CokernelCofork.ofπ (G.map (CategoryTheory.Limits.Cofork.π c)) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Limits.CokernelCofork.map_π
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : CokernelCofork f)
(G : Functor C D)
[G.PreservesZeroMorphisms]
:
def
CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : CokernelCofork f)
(G : Functor C D)
[G.PreservesZeroMorphisms]
:
The underlying cocone of a cokernel cofork is mapped to a colimit cocone if and only if the mapped cokernel cofork is colimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.CokernelCofork.mapIsColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
{f : X ⟶ Y}
(c : CokernelCofork f)
(hc : IsColimit c)
(G : Functor C D)
[G.PreservesZeroMorphisms]
[PreservesColimit (parallelPair f 0) G]
:
IsColimit (c.map G)
A colimit cokernel cofork is mapped to a colimit cokernel cofork by a functor G
when this functor preserves the corresponding colimit.
Equations
- c.mapIsColimit hc G = (c.isColimitMapCoconeEquiv G) (CategoryTheory.Limits.isColimitOfPreserves G hc)
Instances For
def
CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv'
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y Z : C}
{f : X ⟶ Y}
{h : Y ⟶ Z}
(w : CategoryStruct.comp f h = 0)
:
IsColimit (G.mapCocone (CokernelCofork.ofπ h w)) ≃ IsColimit (CokernelCofork.ofπ (G.map h) ⋯)
The map of a cokernel cofork is a colimit iff
the cokernel cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute CokernelCofork.ofπ with Functor.mapCocone.
This is a variant of isColimitMapCoconeCoforkEquiv for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
Equations
- CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv' G w = (CategoryTheory.Limits.CokernelCofork.ofπ h w).isColimitMapCoconeEquiv G
Instances For
def
CategoryTheory.Limits.isColimitCoforkMapOfIsColimit'
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y Z : C}
{f : X ⟶ Y}
{h : Y ⟶ Z}
(w : CategoryStruct.comp f h = 0)
[PreservesColimit (parallelPair f 0) G]
(l : IsColimit (CokernelCofork.ofπ h w))
:
IsColimit (CokernelCofork.ofπ (G.map h) ⋯)
The property of preserving cokernels expressed in terms of cokernel coforks.
This is a variant of isColimitCoforkMapOfIsColimit for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
Equations
Instances For
def
CategoryTheory.Limits.isColimitOfHasCokernelOfPreservesColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasCokernel f]
[PreservesColimit (parallelPair f 0) G]
:
IsColimit (Cofork.ofπ (G.map (cokernel.π f)) ⋯)
If G preserves cokernels and C has them, then the cofork constructed of the mapped morphisms of
a cokernel cofork is a colimit.
Equations
Instances For
instance
CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasCokernel f]
[PreservesColimit (parallelPair f 0) G]
:
HasCokernel (G.map f)
theorem
CategoryTheory.Limits.PreservesCokernel.of_iso_comparison
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasCokernel f]
[HasCokernel (G.map f)]
[i : IsIso (cokernelComparison f G)]
:
PreservesColimit (parallelPair f 0) G
If the cokernel comparison map for G at f is an isomorphism, then G preserves the
cokernel of f.
def
CategoryTheory.Limits.PreservesCokernel.iso
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasCokernel f]
[HasCokernel (G.map f)]
[PreservesColimit (parallelPair f 0) G]
:
If G preserves the cokernel of f, then the cokernel comparison map for G at f is
an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PreservesCokernel.iso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasCokernel f]
[HasCokernel (G.map f)]
[PreservesColimit (parallelPair f 0) G]
:
(iso G f).inv = cokernelComparison f G
instance
CategoryTheory.Limits.instIsIsoCokernelComparison
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasCokernel f]
[HasCokernel (G.map f)]
[PreservesColimit (parallelPair f 0) G]
:
IsIso (cokernelComparison f G)
theorem
CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasCokernel f]
[HasCokernel (G.map f)]
[PreservesColimit (parallelPair f 0) G]
{X' Y' : C}
(g : X' ⟶ Y')
[HasCokernel g]
[HasCokernel (G.map g)]
[PreservesColimit (parallelPair g 0) G]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : CategoryStruct.comp f q = CategoryStruct.comp p g)
:
CategoryStruct.comp (PreservesCokernel.iso G f).hom (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) = CategoryStruct.comp (G.map (cokernel.map f g p q hpq)) (PreservesCokernel.iso G g).hom
theorem
CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(G : Functor C D)
[G.PreservesZeroMorphisms]
{X Y : C}
(f : X ⟶ Y)
[HasCokernel f]
[HasCokernel (G.map f)]
[PreservesColimit (parallelPair f 0) G]
{X' Y' : C}
(g : X' ⟶ Y')
[HasCokernel g]
[HasCokernel (G.map g)]
[PreservesColimit (parallelPair g 0) G]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : CategoryStruct.comp f q = CategoryStruct.comp p g)
{Z : D}
(h : cokernel (G.map g) ⟶ Z)
:
CategoryStruct.comp (PreservesCokernel.iso G f).hom
(CategoryStruct.comp (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) h) = CategoryStruct.comp (G.map (cokernel.map f g p q hpq)) (CategoryStruct.comp (PreservesCokernel.iso G g).hom h)
instance
CategoryTheory.Limits.preservesKernel_zero
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(X Y : C)
(G : Functor C D)
[G.PreservesZeroMorphisms]
:
PreservesLimit (parallelPair 0 0) G
instance
CategoryTheory.Limits.preservesCokernel_zero
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
(X Y : C)
(G : Functor C D)
[G.PreservesZeroMorphisms]
:
PreservesColimit (parallelPair 0 0) G
theorem
CategoryTheory.Limits.preservesKernel_zero'
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
(G : Functor C D)
[G.PreservesZeroMorphisms]
(f : X ⟶ Y)
(hf : f = 0)
:
PreservesLimit (parallelPair f 0) G
The kernel of a zero map is preserved by any functor which preserves zero morphisms.
theorem
CategoryTheory.Limits.preservesCokernel_zero'
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[HasZeroMorphisms D]
{X Y : C}
(G : Functor C D)
[G.PreservesZeroMorphisms]
(f : X ⟶ Y)
(hf : f = 0)
:
PreservesColimit (parallelPair f 0) G
The cokernel of a zero map is preserved by any functor which preserves zero morphisms.