# constructive Serre classes

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?

-
Silly answer: define a Serre class to be one closed under decidable subgroups and quotients by decidable normal subgroups. But you probably need fairly arbitrary quotients, yes? – Andrej Bauer May 29 '13 at 23:49
I was about to ask something along the lines of Andrej's comment but his formulation is better than mine. I have a hard time imagining what quotients by non-decidable subgroups. What does $\mathbb{R}/\mathbb{Q}$ look like constructively? – François G. Dorais May 30 '13 at 0:15
Yeah, I specifically don't want to change the definition of Serre class. I don't think the application I have in mind (spectral sequences) will yield any decidability conditions. – Mike Shulman May 30 '13 at 5:21
Just one word of warning. When working with constructive groups it makes sense to consider antisubgroups as well as subgroups. – Andrej Bauer Jun 1 '13 at 19:07
So if you take quotients of subgroups of finitely generated groups, how far are we from a Serre class? – Andrej Bauer Jun 1 '13 at 19:12

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.