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)) ⋯

@[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] : Fork.ι (c.map G) = G.map (Fork.ι c)

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] : IsLimit (G.mapCone c) ≃ IsLimit (c.map G)

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.

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)

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

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

• CategoryTheory.Limits.isLimitForkMapOfIsLimit' G w l = (CategoryTheory.Limits.isLimitMapConeForkEquiv' G w) (CategoryTheory.Limits.isLimitOfPreserves G l)

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] : IsLimit (Fork.ofι (G.map (kernel.ι f)) ⋯)

If G preserves kernels and C has them, then the fork constructed of the mapped morphisms of a kernel fork is a limit.

Equations

• CategoryTheory.Limits.isLimitOfHasKernelOfPreservesLimit G f = CategoryTheory.Limits.isLimitForkMapOfIsLimit' G ⋯ (CategoryTheory.Limits.kernelIsKernel f)

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] : G.obj (kernel f) ≅ kernel (G.map f)

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.

@[simp]

theorem CategoryTheory.Limits.PreservesKernel.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] : CategoryStruct.comp (iso G f).inv (G.map (kernel.ι f)) = kernel.ι (G.map f)

@[simp]

theorem CategoryTheory.Limits.PreservesKernel.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] {Z : D} (h : G.obj X ⟶ Z) : CategoryStruct.comp (iso G f).inv (CategoryStruct.comp (G.map (kernel.ι f)) h) = CategoryStruct.comp (kernel.ι (G.map f)) h

@[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)) ⋯

@[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] : Cofork.π (c.map G) = G.map (Cofork.π c)

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] : IsColimit (G.mapCocone c) ≃ IsColimit (c.map G)

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.

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)

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

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

• CategoryTheory.Limits.isColimitCoforkMapOfIsColimit' G w l = (CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv' G w) (CategoryTheory.Limits.isColimitOfPreserves G l)

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

• CategoryTheory.Limits.isColimitOfHasCokernelOfPreservesColimit G f = CategoryTheory.Limits.isColimitCoforkMapOfIsColimit' G ⋯ (CategoryTheory.Limits.cokernelIsCokernel f)

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] : G.obj (cokernel f) ≅ cokernel (G.map f)

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.

@[simp]

theorem CategoryTheory.Limits.PreservesCokernel.π_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) [HasCokernel f] [HasCokernel (G.map f)] [PreservesColimit (parallelPair f 0) G] : CategoryStruct.comp (G.map (cokernel.π f)) (iso G f).hom = cokernel.π (G.map f)

@[simp]

theorem CategoryTheory.Limits.PreservesCokernel.π_iso_hom_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] {Z : D} (h : cokernel (G.map f) ⟶ Z) : CategoryStruct.comp (G.map (cokernel.π f)) (CategoryStruct.comp (iso G f).hom h) = CategoryStruct.comp (cokernel.π (G.map f)) h

@[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.