Serre classes

For any abelian category C, we introduce a type class IsSerreClass C for Serre classes in C (also known as "Serre subcategories"). A Serre class is a property P : ObjectProperty C of objects in C which holds for a zero object, and is closed under subobjects, quotients and extensions.

Future work

• Show that the localization of C with respect to a Serre class is an abelian category.

References

• Jean-Pierre Serre, Groupes d'homotopie et classes de groupes abéliens

class CategoryTheory.ObjectProperty.IsSerreClass {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) extends P.ContainsZero, P.IsClosedUnderSubobjects, P.IsClosedUnderQuotients, P.IsClosedUnderExtensions : Prop

A Serre class in an abelian category consists of a predicate which holds for the zero object and is closed under subobjects, quotients, extensions.

• exists_zero : ∃ (Z : C), Limits.IsZero Z ∧ P Z
• prop_of_mono {X Y : C} (f : X ⟶ Y) [Mono f] (hY : P Y) : P X
• prop_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] (hX : P X) : P Y
• prop_X₂_of_shortExact {S : ShortComplex C} (hS : S.ShortExact) (h₁ : P S.X₁) (h₃ : P S.X₃) : P S.X₂

instance CategoryTheory.ObjectProperty.instIsSerreClassTop {C : Type u} [Category.{v, u} C] [Abelian C] : ⊤.IsSerreClass

instance CategoryTheory.ObjectProperty.instIsSerreClassIsZero {C : Type u} [Category.{v, u} C] [Abelian C] : IsSerreClass Limits.IsZero

theorem CategoryTheory.ObjectProperty.prop_iff_of_shortExact {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {S : ShortComplex C} (hS : S.ShortExact) : P S.X₂ ↔ P S.X₁ ∧ P S.X₃

theorem CategoryTheory.ObjectProperty.prop_X₂_of_exact {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {S : ShortComplex C} (hS : S.Exact) (h₁ : P S.X₁) (h₃ : P S.X₃) : P S.X₂

instance CategoryTheory.ObjectProperty.instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) {D : Type u'} [Category.{v', u'} D] [Abelian D] [P.IsSerreClass] (F : Functor D C) [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : (P.inverseImage F).IsSerreClass