Kernels and cokernels in categories of homological complexes

theorem HomologicalComplex.hasKernel_of_hasKernel_f {ι : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) [∀ (i : ι), CategoryTheory.Limits.HasKernel (f.f i)] : CategoryTheory.Limits.HasKernel f

theorem HomologicalComplex.hasCokernel_of_hasCokernel_f {ι : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) [∀ (i : ι), CategoryTheory.Limits.HasCokernel (f.f i)] : CategoryTheory.Limits.HasCokernel f

theorem HomologicalComplex.eval_preservesLimit_of_hasKernel_f {ι : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) [∀ (i : ι), CategoryTheory.Limits.HasKernel (f.f i)] (i : ι) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) (eval C c i)

theorem HomologicalComplex.eval_preservesColimit_of_hasCokernel_f {ι : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) [∀ (i : ι), CategoryTheory.Limits.HasCokernel (f.f i)] (i : ι) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) (eval C c i)