feat(CategoryTheory/Abelian): Criterion for full subcategory of abelian category to be abelian (leanprover-community#36483)

If `P` is an object property in an abelian category and

- `P` contains zero,
- `P` is closed under kernels and cokernels,
- `P` is closed under finite products,

then the full subcategory defined by `P` is abelian.

Author: justus-springer

Mathlib.lean

@@ -2377,6 +2377,7 @@ public import Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
 public import Mathlib.CategoryTheory.Abelian.SerreClass.Localization
 public import Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
 public import Mathlib.CategoryTheory.Abelian.ShortExact
+public import Mathlib.CategoryTheory.Abelian.Subcategory
 public import Mathlib.CategoryTheory.Abelian.Subobject
 public import Mathlib.CategoryTheory.Abelian.Transfer
 public import Mathlib.CategoryTheory.Abelian.Yoneda

Mathlib/CategoryTheory/Abelian/Subcategory.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2026 Justus Springer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Justus Springer
+-/
+module
+
+public import Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
+public import Mathlib.CategoryTheory.ObjectProperty.Kernels
+
+/-!
+# 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.
+
+-/
+
+@[expose] public section
+
+namespace CategoryTheory.ObjectProperty
+
+open Limits
+
+variable {C : Type*} [Category* C] (P : ObjectProperty C)
+
+lemma preservesMonomorphisms_ι_of_isNormalEpiCategory [HasZeroMorphisms C] [HasFiniteCoproducts C]
+    [HasKernels C] [HasCokernels C] [IsNormalEpiCategory C] [HasZeroObject C] [P.ContainsZero]
+    [P.IsClosedUnderKernels] : P.ι.PreservesMonomorphisms :=
+  have := P.preservesKernels_ι
+  NormalEpiCategory.preservesMonomorphisms_of_preservesKernels P.ι
+
+instance [Abelian C] [P.ContainsZero] [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels] :
+    IsNormalMonoCategory P.FullSubcategory where
+  normalMonoOfMono {X Y} f :=
+    have := P.preservesMonomorphisms_ι_of_isNormalEpiCategory
+    ⟨{Z := .mk _ (P.prop_cokernel f.hom X.property Y.property)
+      g := P.homMk (cokernel.π f.hom)
+      w := by cat_disch
+      isLimit := isLimitOfReflects P.ι ((KernelFork.isLimitMapConeEquiv _ _).symm
+        (Abelian.monoIsKernelOfCokernel _ (cokernelIsCokernel (P.ι.map f)) :))}⟩
+
+lemma preservesEpimorphisms_ι_of_isNormalMonoCategory [HasZeroMorphisms C] [HasFiniteProducts C]
+    [HasKernels C] [HasCokernels C] [IsNormalMonoCategory C] [HasZeroObject C] [P.ContainsZero]
+    [P.IsClosedUnderCokernels] : P.ι.PreservesEpimorphisms :=
+  have := P.preservesCokernels_ι
+  NormalMonoCategory.preservesEpimorphisms_of_preservesCokernels P.ι
+
+instance [Abelian C] [P.ContainsZero] [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels] :
+    IsNormalEpiCategory P.FullSubcategory where
+  normalEpiOfEpi {X Y} f :=
+    have := P.preservesEpimorphisms_ι_of_isNormalMonoCategory
+    ⟨{W := .mk _ (P.prop_kernel f.hom X.property Y.property)
+      g := P.homMk (kernel.ι f.hom)
+      w := by cat_disch
+      isColimit := isColimitOfReflects P.ι ((CokernelCofork.isColimitMapCoconeEquiv _ _).symm
+        (Abelian.epiIsCokernelOfKernel _ (kernelIsKernel (P.ι.map f)) :))}⟩
+
+instance [Abelian C] [P.ContainsZero] [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels]
+    [P.IsClosedUnderFiniteProducts] : Abelian P.FullSubcategory where
+
+end CategoryTheory.ObjectProperty

Mathlib/CategoryTheory/ObjectProperty/Kernels.lean

@@ -100,6 +100,12 @@ noncomputable def createsKernels [P.IsClosedUnderKernels] {X Y : P.FullSubcatego
   · exact (IsLimit.postcomposeInvEquiv _ _).symm (kernelIsKernel f.hom)
   · exact P.prop_kernel f.hom X.property Y.property
 
+lemma preservesKernels_ι [HasKernels C] [P.IsClosedUnderKernels] ⦃X Y : P.FullSubcategory⦄
+    (f : X ⟶ Y) : PreservesLimit (parallelPair f 0) P.ι := by
+  have := P.createsKernels f
+  have := P.hasLimit_parallelPair_comp_ι f
+  exact preservesLimit_of_createsLimit_and_hasLimit _ _
+
 instance [P.IsClosedUnderKernels] [HasKernels C] : HasKernels P.FullSubcategory where
   has_limit f :=
     letI := P.createsKernels f
@@ -142,6 +148,12 @@ noncomputable def createsCokernels [P.IsClosedUnderCokernels] {X Y : P.FullSubca
   · exact (IsColimit.precomposeHomEquiv _ _).symm (cokernelIsCokernel f.hom)
   · exact P.prop_cokernel f.hom X.property Y.property
 
+lemma preservesCokernels_ι [HasCokernels C] [P.IsClosedUnderCokernels] ⦃X Y : P.FullSubcategory⦄
+    (f : X ⟶ Y) : PreservesColimit (parallelPair f 0) P.ι := by
+  have := P.createsCokernels f
+  have := P.hasColimit_parallelPair_comp_ι f
+  exact preservesColimit_of_createsColimit_and_hasColimit _ _
+
 instance [P.IsClosedUnderCokernels] [HasCokernels C] : HasCokernels P.FullSubcategory where
   has_colimit f :=
     letI := P.createsCokernels f