## Are all group monomorphisms regular, constructively?

By "constructive" I mean something that would go through in CZF for example.

[added Oct 6] A sketch of a standard proof (such as referenced in comment below), which is almost constructive: Let H be a subgroup of G, and consider the (say, left-) cosets of H, plus a distinguished element. There is a homomorphism f from G to the permutation group of these, given by left multiplication (leaving the extra element fixed). Construct an involution t which exchanges the coset of 1 and the distinguished element. Then for all g in G, f(g) = t.f(g).t iff g is in H.

The involution t distinguishes the coset of 1 from the other cosets. In other words t can distinguish elements of G which are in H from those which aren't. So in CZF we have the theorem: every "detachable" subgroup H of G is the equaliser of two group homomorphisms. That is, this seems to require the additional hypothesis that $\forall x \in G (x \in H \vee x \not\in H)$. Of course this is a classical tautology so it disappears when we go to ZF (which is CZF + law of excluded middle).

In practice, an answer to the following question will probably yield an answer (and if it fails to, it will probably be for an interesting reason)

I call a PER-Group a subset G of natural numbers, and equivalence relation R on G, with multiplication and inverse operations as partial computable functions, totally defined over G, and respecting R.

Note G and R need not even be c.e. [and in fact, if H is a decidable subset of G, then the problem is already solved, as above] For instance, addition over the computable reals is computable, even though the set of codes for computable reals is not c.e., nor is equality of two computable reals. Of course that example is abelian, and the proof that every abelian group monomorphism is normal is constructive. I am interested in the non-abelian case.

Is every PER-group inclusion the equaliser of two PER-group homomorphisms?

-
 Why is the usual proof (see for example exercise 7H (a) in "abstract and concrete categories", katmat.math.uni-bremen.de/acc/acc.pdf) not constructive? – Martin Brandenburg Oct 6 2010 at 8:16 Yeah, this deserves some text so I'm editing the question. – Monic Win Oct 6 2010 at 14:45 The edit currently has a few typos: you need to adjoin the additional element to the set of cosets before taking the permutation group and constructing the homormorphism from G to it; and at the end, the second homomorphism you construct should look at $t \cdot f(g) \cdot t$, not $t(f(t(g))$. Also, what you call “detachable subgroup” would I think normally be known as a “decidable subgroup” (since the condition is exactly that its membership predicate is decidable)? But this is in any case a lovely question! – Peter LeFanu Lumsdaine Oct 6 2010 at 17:15 Fixed the typos. "Decidable" has computational connotations. Of course there is a strong constructive/computational link, and I did in fact use "decidable" in the PER-version of the question. Still, for abstract set theory I think I prefer "detachable". – Monic Win Oct 6 2010 at 17:58 Hmmm… interesting — I'd thought it was fairly standard in constructive logic to call a proposition/predicate/subset decidable if (internally) one can prove the excluded middle for it, but googling for a few phrases like “decidable truth-values” etc. does suggest that it's mostly categorical logicians and computer scientists who use this terminology. – Peter LeFanu Lumsdaine Oct 7 2010 at 1:56

This theorem is a preculiarity of the theory of groups. It is not true in the category of commutative monoids, by contrast, where the composite of two regular monos is mono but need not be regular. We therefore need to get our hands dirty with some computation with groups - it is not enough to wave them about categorical definitions.

I am picking up the argument from Andrej Bauer's blog. As observed there, in a category with pushouts (known in group theory as free products with amalgamation) and equalisers, a map is regmono iff it is the equaliser of its cokernel (pushout against itself).

We need an explicit description of this pushout, and before that the coproduct (free product). Given two groups (call them red and blue) with decidable equality, their coproduct or free product $G_1*G_2$ consists of the strings of non-identity elements of alternating colour. The inverse of such a string is the reverse string of inverses. Multiplication is by concatenation with cancellation and the empty string serves as the identity. Such expressions therefore have a well defined length.

As Andrej describes, the pushout is obtained as the quotient of the coproduct by the normal subgroup $N$ generated by the primitive expressions $i_1(x) i_2(x)^{-1}$ where $x$ runs through the subgroup. In order to prove the theorem, it is necessary to show that if some primitive expression defined by a general element $x$ of the group happens to lie in $N$ then $x$ belongs to the subgroup.

The key observation is that any primitive expression has length 2, or 0 in the case where $x=1$.

On the other hand, the normal subgroup $N$ consists of products of conjugates of expressions like these. Conjugation in $G*G$ involves appending inverse strings either side. Any non-trivial conjugate or product therefore has length at least 3.

It follows that if $i_1(x) i_2(x)^{-1}\in N$ then this is not a non-trivial conjugate or product, so it was one of the generating elements, with $x\in H$.

There is a constructive version of this argument, ie not assuming that equality is decidable, but it is more complicated. Letters in the string may be identity elements, but then there are cancellation rules. Instead of the elements of $G*G$ (equivalence classes of strings), we use the strings themselves and then explicitly consider the cancellation rules.

Given a formal product of conjugates, if a cancellation rule applies then there is a shorter formal product that is equivalent to it in $G*G$. There are lots of cases, but I think that they will yield the result.

Andrej observed that this result fails if we replace ordinary sets by PERs, where the kernel of a quotient need not be the given equivalence relation. This property is known as Barr exactness. A category with sufficiently well behaved finite limits and finite colimits is called a pretopos.

However, my argument also relies on having well behaved lists (free monoids).

I don't know what the situation is in CZF, but would argue that the appropriate foundational setting for this question is an arithmetic universe. Roughly speaking, this is the kind of "set theory" that is taught to first year computer science undergraduates, involving finite powersets and the natural numbers.

The category of compact Hausdorff spaces is a pretopos but not an arithmetic universe. I conjecture therefore that there is a closed subgroup of a compact Hausdorff group that is not an equaliser.

-
 You probably know this, Paul, but for others' benefit I'll add that Palmgren's constructive foundations is basically the idea that the category Set is a well-pointed $\Pi$-pretopos with a NNO and enough projectives (see ncatlab.org/nlab/show/ETCS#references_19). However I don't know enough about this to know if the desired proof exists. – David Roberts Nov 14 2010 at 20:44 For my observation about "lengths" of elements of the pushout I need well behaved free monoids. The notion of arithmetic universe provides exactly this (or would, if anyone had ever written the paper about them). Maybe one could derive free monoids from Palmgren's system, but the $\Pi$s are surely overkill. – Paul Taylor Nov 14 2010 at 22:51

The answer for PERs is negative. In the category of PERs every regular subobject is $\lnot\lnot$-stable in the internal language (because equality is $\lnot\lnot$-stable), but not every subgroup is $\lnot\lnot$-stable. For example, consider the group $G = \mathbb{Z}_2^\mathbb{N}$ of infinite sequences of elements of $\mathbb{Z}_2$, with pointwise operations (I am now talking in the internal language of PERs so you have to figure out the concrete PER structure). Then $$H = \lbrace f \in G \mid \exists n . \forall m, f(m+n) = 0\rbrace$$ is a subgroup whose membership is not $\lnot\lnot$-stable. Suppose it were, i.e., $$\forall f \in G, \lnot\lnot (f \in H) \implies f \in H.$$ By Markov principle, which is valid in PER, the assumption $\lnot\lnot(f \in H)$ is equivalent to $\lnot\forall n . \exists m . f(m+n) = 1$. But the statement $$\forall f \in G. (\lnot\forall n . \exists m . f(m+n) = 1) \implies \exists n . \forall m . f(n + m) = 0.$$ cannot be computably realized. (I will think in more detail about this and update the answer when I know how to phrase things more concisely and without resort to a lot of realizability theory.)

The question is very interesting because it fails in PER but I do not see why it would fail in the effective topos. PER does not have powersets but a topos does. So this is a hint on how to proceed: we should use powersets in an essential way. A good test case is the group $G = \mathbb{Z}_2$ with the subgroup $H = \lbrace x \in G \mid p \lor (x = 0)\rbrace$ where $p \in \Omega$ is an arbitrary truth value.

-
 @Andrej: just dropping a comment here so you get a notification about Paul Taylor’s answer below. – Peter LeFanu Lumsdaine Nov 14 2010 at 16:59

Equality over the computable reals is stable, but it is not necessarily stable for all PERs. For example, a set of equivalence sets of words modulo a rewrite relation. Two words are equal iff there exists a rewrite path between them. This relation has positive content and is not stable under double negation.

Coming up with that counterexample to Andrej's claim actually led me to answer my own question.

A subgroup is the equaliser of its cokernel pair, which in the category of groups is the amalgamated free product. So we just have to constructively prove that this exists. Schreier's construction is very explicit, but word reduction is not computable. So, instead of using the set of reduced words, we work with, yes, the set of equivalence sets of words modulo the reduction relation.

Given a PER as $(G,R,mult,inv)$, and a subgroup $H$ of $G$, we form $G^{\ast}$ as a set of finite sequences of elements from the disjoint sum $G+G$, $R^{\ast}$ as an appropriate equivalence relation for the amalgamated free product (allowing combination of adjacent elements from the same copy of $G$ via multiplication, and also allowing switching between different copies of $G$ if the element in question is in $H$). Then multiplication and inversion are computable, even though in general $R^{\ast}$ isn't.

This same construction can be done in abstract set theory, where quotient sets are not a problem and work in weak subtheories of CZF.

As discussed below, the above is mistaken. As I understand it now -- please point out any error -- the construction above is well-defined and gives the cokernel pair, and in CZF, the subgroup is the equaliser of the cokernel pair, which answers the original question in the affirmative.

But in PER, the subgroup is not quite the equaliser of it. The morphism asserted to exist by the universal property isn't quite constructible in PER, sometimes some necessary information has been lost. The failure has nothing to do with group theory. We can forget the group operations and ask if every PER-injection is the equaliser of two PER-functions, and the answer is still no. PER isn't as good an approximation to constructive set theory as I thought.

-
Equality in the category of PERs is stable, I am very sure of this. Your existence of a rewrite path, for example, is external and not internal. Let me put this another way. Suppose we have an equivalence relation $\sim$ on a per $A$, i.e., a mono ${\sim} \to A \times A$ which is an equivalence relation. The quotient per $A/{\sim}$ satisfies in the internal language $$\lnot\lnot (x \sim y) \iff [x] = [y]$$ where $[{-}] : A \to A/{\sim}$ is the canonical quotient. Another way to say this is that quotients in PER are not effective. – Andrej Bauer Oct 7 2010 at 16:30
Your answer has a problem, at least in PERs, namely, because the "appropriate equivalence relation", call it $\sim$, is not $\lnot\lnot$-stable there is going to be a hole in your reasoning at some point: you will want to conclude $x \sim y$ from $[x] = [y]$, but that won't be possible. Nevertheless, I think your construction works in a setting in which equivalence relations are effective (a topos, for example). – Andrej Bauer Oct 7 2010 at 16:32
Is that right? I thought $\left|x\right| = \left|y\right|$ means exactly $R^{\ast}(x,y)$. Multiplication has to be compatible with $R^{\ast}$, but otherwise it just acts on the underlying $G^{\ast} \subset \mathbb{N}$. Notice that in my definition of PER I have not required the complement of $R$ to be c.e. either, perhaps that is what you are thinking? – Monic Win Oct 7 2010 at 20:26
Incidentally CZF is predicative. There are exponentials but no powersets (no subobject classifier). So I hope there is no need to go to toposes. – Monic Win Oct 7 2010 at 20:29
And I might write a blog post. It's interesting to have a non-contrived constructive result which fails in PERs. – Andrej Bauer Oct 8 2010 at 4:19