Subcategories of abelian categories

Let C be an abelian category. Given P : ObjectProperty C which contains zero, is closed under kernels, cokernels and finite products, we show that the full subcategory defined by P is abelian.

theorem CategoryTheory.ObjectProperty.preservesMonomorphisms_ι_of_isNormalEpiCategory {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Limits.HasZeroMorphisms C] [Limits.HasFiniteCoproducts C] [Limits.HasKernels C] [Limits.HasCokernels C] [IsNormalEpiCategory C] [Limits.HasZeroObject C] [P.ContainsZero] [P.IsClosedUnderKernels] : P.ι.PreservesMonomorphisms

instance CategoryTheory.ObjectProperty.instIsNormalMonoCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Abelian C] [P.ContainsZero] [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels] : IsNormalMonoCategory P.FullSubcategory

theorem CategoryTheory.ObjectProperty.preservesEpimorphisms_ι_of_isNormalMonoCategory {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Limits.HasZeroMorphisms C] [Limits.HasFiniteProducts C] [Limits.HasKernels C] [Limits.HasCokernels C] [IsNormalMonoCategory C] [Limits.HasZeroObject C] [P.ContainsZero] [P.IsClosedUnderCokernels] : P.ι.PreservesEpimorphisms

instance CategoryTheory.ObjectProperty.instIsNormalEpiCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Abelian C] [P.ContainsZero] [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels] : IsNormalEpiCategory P.FullSubcategory

@[implicit_reducible]

instance CategoryTheory.ObjectProperty.instAbelianFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernelsOfIsClosedUnderFiniteProducts {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Abelian C] [P.ContainsZero] [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels] [P.IsClosedUnderFiniteProducts] : Abelian P.FullSubcategory