constructive Serre classes

Question

A Serre class (of abelian groups) is a class of abelian groups closed under subgroups, quotients, and extensions. For instance, finitely generated groups and finite groups are both Serre classes.

However, in constructive mathematics, these are no longer examples, at least not with the usual definition of "finite" (= in bijection with $\{0,1,\dots,n\}$ for some $n\in\mathbb{N}$). In particular, finite sets are not closed under subsets and quotients, so there is no reason that finite groups should be either.

There are other weaker constructive notions of "finite", some of which are described here: subfinite, finitely indexed, subfinitely indexed. It seems that subfinitely indexed sets — the subquotients of finite sets — are closed under subsets, quotients, and finite products, so that the subfinitely indexed groups should be a Serre class even constructively. Classically, of course, all subfinitely indexed sets are finite.

My original question was:

Is there a Serre class of abelian groups in constructive mathematics which reduces classically to the finitely generated ones?

As pointed out by Ingo, this has a trivial and uninteresting answer; the real question is

Is there a description of the Serre envelope of the class of finitely generated abelian groups which is more explicit than the trivial inductive one?

Answer 1

Any subclass $\mathcal{C}$ of an abelian category determines a smallest Serre class containing it, by iteratively adding (the zero object and) the object $Y$ for any exact sequence $X \to Y \to Z$ where $X$ and $Z$ are objects of the previous stage. Note the missing zeros at the ends of the sequence; alternatively, one can iteratively add the zero object, subobjects, quotients, and extensions (objects $Y$ such that there is a short exact sequence $0 \to X \to Y \to Z \to 0$ with $X$ and $Z$ previously added).

Anyway, this construction can in particular be performed with the class $\mathcal{C}$ of finitely generated abelian groups. Classically, its closure will coincide with $\mathcal{C}$, as $\mathcal{C}$ is already a Serre class.

However, this construction only answers the question in a technical sense, since it describes the sought-after class in rather abstract terms. The construction thus only shows that the question could profitably be reformulated in order to better capture its spirit: "Is there a description of the Serre envelope of the class of finitely generated abelian groups which is more explicit than the trivial inductive one?"