Subgroups are equalizers, constructively?
- 10 November 2010
- General
[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.
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
Comments
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 regular epi. 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