feat(CategoryTheory/Limits/Preserves/Shapes/Kernels): Mapping zeroKernelFork (#36410)

A compatibility iso relating `KernelFork.map` and `kernel.zeroKernelFork`.

Author: justus-springer

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean

@@ -326,4 +326,25 @@ lemma preservesCokernel_zero' (f : X ⟶ Y) (hf : f = 0) :
   rw [hf]
   infer_instance
 
+section ZeroObject
+
+variable [HasZeroObject C] [HasZeroObject D]
+
+variable {X Y : C} (f : X ⟶ Y)
+
+set_option backward.isDefEq.respectTransparency false in
+/-- Mapping a `zeroKernelFork` of `f : X ⟶ Y` along a functor `G` that preserves zero morphisms
+is isomorphic to the `zeroKernelFork` of `G.map f`. -/
+def mapZeroKernelFork :
+    (kernel.zeroKernelFork f).map G ≅ (kernel.zeroKernelFork (G.map f)) :=
+  Fork.ext G.mapZeroObject
+
+/-- Mapping a `zeroCokernelCofork` of `f : X ⟶ Y` along a functor `G` that preserves zero morphisms
+is isomorphic to the `zeroCokernelCofork` of `G.map f`. -/
+def mapZeroCokernelCofork :
+    (cokernel.zeroCokernelCofork f).map G ≅ (cokernel.zeroCokernelCofork (G.map f)) :=
+  Cofork.ext G.mapZeroObject
+
+end ZeroObject
+
 end CategoryTheory.Limits