[**Edit 2010-11-12: **Given the gap in my “proof”, I am changing the title of the post to a question.]

I would like to record the following fact, which is hard to find on the internet: *every subgroup is an equalizer, constructively*. In other words, all monos in the category of groups are regular, constructively. It is interesting that this fact fails if we work in a meta-theory with “poor quotients”.

The usual proof that every subgroup is an equalizer uses classical logic, see for example 7H(a) on page 129 of “Abstract and Concrete Categories – the Joy of Cats” by Jiri Adámek, Horst Herrlich, George E. Strecker. A question on MathOverflow motivated me to try to find a constructive proof. In the end it was found by Monic Win. I reproduce the proof here and also make a couple of further comments.

Theorem:Every subgroup is an equalizer.

Proof.A subroup is the equalizer of its cokerenel pair. QED.That is a bit cryptic. Let’s spell out the details. Consider a subgroup $H$ of a group $G$. Let $ G *_H G$ be the free product with amalgamation of $G$ with respect to the inclusion $H \to G$. Concretely, $G *_H G$ is the quotient group $(G * G)/N$ of the free product $G * G$ with respect to the least normal subgroup $N$ that contains elements of the form $\iota_1(x) \iota_2(x)^{-1}$ for $x \in H$, where $\iota_1, \iota_2 : G \to G * G$ are the canonical inclusions. Let $q : G * G \to (G * G)/N$ be the canonical quotient map and define $f = q \circ \iota_1$ and $g = q \circ \iota_2$. We claim that $H$ is the equalizer of $f$ and $g$: $$H = \{ x \in G \mid f(x) = g(x) \}.$$ If $x \in H$ then $\iota_1(x) \iota_2(x)^{-1} \in N$, hence $f(x) g(x)^{-1} = q(\iota_1(x) \iota_2(x)^{-1}) = 1_K$ and so $f(x) = g(x)$. Conversely, suppose $x \in G$ is such that $f(x) = g(x)$. Then $1_K = f(x) g(x)^{-1} = q(\iota_1(x) \iota_2(x)^{-1})$, hence $\iota_1(x) \iota_2(x)^{-1} \in N$. The proof is constructive. QED again.

However, the story does not end here. There seems to be a counter-example to the above theorem in the category of numbered sets (also known as partial numberings). The internal logic of this category is intuitionistic first-order logic with Number choice and Markov principle. Consider the group $G = \mathbb{Z}_2^\omega$ (countable product of copies of $\mathbb{Z}_2$) and the subgroup $$H = \lbrace a \in G \mid \exists n \in \mathbb{N} . \forall m \geq n . a_m = 0\rbrace.$$ In the category of numbered sets all equalizers are $\lnot\lnot$-stable. So, if $H$ were an equalizer this would imply, for all $a \in G$, $\lnot\lnot (a \in H) \Rightarrow a \in H$, which amounts to $$\forall a \in \mathbb{Z}_2^\omega . (\lnot \forall n \in \mathbb{N} . \exists m \geq n . a_m = 1) \Rightarrow \exists n \in \mathbb{N} . \forall m \geq n . a_m = 0$$ where we used Markov principle (can you spot it?). A realizer for the above statement is (a code of) a computable function that accepts (a code of) a total computable function $a : \mathbb{N} \to \lbrace 0, 1 \rbrace$ which does *not* attain value $1$ infinitely often, and outputs a number $n$ such that $a(m) = 0$ for all $m \geq n$. Clearly, such a realizer cannot exist as it would allows us to implement the Halting Oracle. Therefore, $H$ is not an equalizer.

What is going on? Well, numbered sets have slightly odd quotients. If $R$ is an equivalence relation on a numbered set $A$ and $q : A \to A/R$ is the canonical quotient map onto the quotient $A/R$ then in numbered sets $q(x) = q(y)$ implies only $\lnot\lnot R(x,y)$, rather than the expected $R(x,y)$. (In the parlance of category theory we say that numbered sets are a regular category which is not exact in the sense of Barr.) In the proof of our theorem we have a quotient map $q : G * G \to (G * G)/N$ and we used the fact that $q(\iota_1(x)) = q(\iota_2(x))$ implies $\iota_1(x) \iota_2(x)^{-1} \in N$, whereas in numbered sets we are only allowed to conclude $\lnot\lnot (\iota_1(x) \iota_2(x)^{-1} \in N)$. Consequently, in numbered sets the equalizer of $f, g : G \to (G * G)/N$ is the $\lnot\lnot$-closure of $H$, which is in general larger than $H$. The mystery is resolved (for those who are still following), and the counter-example in numbered sets shows that having just a regular category at the meta-level is not enough to conclude that every subgroup is an equalizer. This may have some relevance for minimalist type theories in which quotients misbehave.

Unless my mind is going very wrong, in a category with enough cokernel pairs, $f$ being an equaliser is equivalent to $f$ being an equaliser of its cokernel pair. So I hardly see the point of non-constructive proofs of such a statement.

Also I have a nice cheeky exercise. The statement above (all subgroups are equalisers) requires the principle of unique choice (if $f$ is a group morphism both epi and mono, then it is invertible). The exercise is to find where it was used in the proof above.

@Arnaud: I don’t see a point in having non-constructive proofs either, but they seem to be circulating around. With a bit of luck this blog post will appear as the first hit under “subgroup equalizer”. I am a bit worried that you phrase unique choice as “an epi-mono is iso”. Usually unique choice is stated as “a functional relation has a choice function”. By the way, in numbered sets not every epi-mono is iso, but Unique Choice expressed in terms of functional relations is valid.

@Andrej:

The functional-relation definition of unique choice is equivalent to

functions both injective and surjective are invertible. When generalising a property of sets to categories, the tension between being epi and surjective is always an issue. I tend to favour epi over surjective because I find it a more elegant property. I’ve never really had to care until today, I must say.So, I’m guessing that in numbered sets epi and surjective is not synonymous. I don’t know what a function between numbered sets is, to be honest.

@Arnaud: Ah yes. In a topos the internal statement “$f$ is surjective” corresponds to $f$ being epi. But in a topos all epis are regular. In numbered sets the internal statement “$f$ is surjective” corresponds to $f$ being

regularepi. Indeed, a morphism which is both mono and regular epi is iso. In any case, you need to be a bit careful here since the usual interpretation of first-order logic in a category validates unique choice.I like the counterexample! But I must be missing something obvious in the last step of the main proof, I think. You conclude that $\iota_1(x) \iota_2(x)^{-1} \in N$, and I’m fine with that. But how does it follow from this that $x \in H$?

@Peter: That’s a very good question. Paul Taylor also pointed out that there is a gap in my proof. We can describe $N$ explicitly, I think, as $N = \lbrace w \, \iota_1(x) \iota_2(x)^{-1} \, w^{-1} \mid x \in H, w \in G * G \rbrace$. So the missing lemma is this: suppose for $x \in G$, $y \in H$ and $w \in G * G$ we have $\iota_1(x) \iota_2(x)^{-1} = w \, \iota_1(y) \iota_2(y)^{-1} \, w^{-1}$. Does it follow that $x \in H$?

Hmm… clearly the set $\{\, w \iota_1(x) \iota_2(x)^{-1} w^{-1}\ |\ x \in H,\,w \in G * G\,\}$ generates $N$, but is it obvious that it’s closed under multiplication and hence is the whole of $N$?

Ooops, of course you are right. So $N$ must contain finite products of elements of the form $w \iota_1(x_1) \iota_2(x)^{-1} w^{-1}$, and then conjugates of those, and products of those, and conjugates of those. Yuck.

In case it is of interest, I gave a different constructive proof at the MathOverflow discussion, using wreath products, here: https://mathoverflow.net/a/272617/2926