A Serre subcategory of an abelian category is abelian

Mathlib has both ends of this and not the join. ObjectProperty.IsSerreClass is closure under subobjects, quotients and extensions, and it already supplies ContainsZero, IsClosedUnderKernels and IsClosedUnderCokernels. Mathlib's abelian-subcategory instance (CategoryTheory/Abelian/Subcategory.lean) asks for those three and IsClosedUnderFiniteProducts, which is not among a Serre class's defining closures and does not follow by instance search.

It does follow mathematically, and the object-level step is Mathlib's too: ObjectProperty.prop_biprod derives P (X ⊞ Y) from closure under extensions, because X ⊞ Y is a split extension of Y by X. This file packages that as the two closure instances, after which the abelian structure is Mathlib's.

Main results

• ObjectProperty.serreIsClosedUnderBinaryProducts and ObjectProperty.serreIsClosedUnderFiniteProducts: a Serre class is closed under finite products.

Together with Mathlib's instance these give Abelian P.FullSubcategory, recorded as a regression check below rather than restated as an instance.

Why this is needed

Stacks 13.17.4 (tag 0FCL) states that D⁻(𝓑) → D⁻_𝓑(𝓐) is an equivalence for a Serre subcategory 𝓑 ⊆ 𝓐 in which every object of 𝓑 admitting a surjection from an object of 𝓐 admits one from a subobject lying in 𝓑. Its source D⁻(𝓑) cannot be formed at all without an abelian structure on 𝓑, so this is that theorem's first prerequisite.

AlgebraicGeometry/Modules/Coherent/Abelian/Basic.lean runs the same binary-product argument by hand for coherent sheaves. That instance could be derived from this one once Scheme.coherent is known to be a Serre class; it is left alone here.

instance CategoryTheory.ObjectProperty.serreIsClosedUnderBinaryProducts {A : Type u} [Category.{v, u} A] [Abelian A] (P : ObjectProperty A) [P.IsSerreClass] : P.IsClosedUnderBinaryProducts

A Serre class is closed under binary products: the limit of a pair is its biproduct, and prop_biprod puts that in P by closure under extensions.

The proof shape is the one AlgebraicGeometry.Scheme.coherent_isClosedUnderBinaryProducts uses for coherent sheaves, transporting the biproduct's limit cone onto the given one.

instance CategoryTheory.ObjectProperty.serreIsClosedUnderFiniteProducts {A : Type u} [Category.{v, u} A] [Abelian A] (P : ObjectProperty A) [P.IsSerreClass] : P.IsClosedUnderFiniteProducts

A Serre class is closed under finite products, the one hypothesis of Mathlib's abelian-subcategory instance that IsSerreClass does not already provide.