Are all group monomorphisms regular, constructively?

Question

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).

[end of addition]

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?

Answer 1

Here is a constructive proof that can be enacted in any topos with a natural numbers object.

Let $i: H \to G$ be monic; let $\pi: G \to G/H$ be the canonical surjective function $g \mapsto g H$. Let $A$ be the free abelian group on $G/H$ with $j: G/H \to A$ the canonical injection, and let $A^G$ denote the set of functions $f: G \to A$, with the pointwise abelian group structure inherited from $A$. This carries a $G$-module structure defined by

$$(g \cdot f)(g') = f(g' g).$$

For any $f \in A^G$, the function $d_f: G \to A^G$ defined by $d_f(g) = g f - f$ defines a derivation. Passing to the wreath product $A^G \rtimes G$, we have two homomorphisms $\phi, \psi: G \rightrightarrows A^G \rtimes G$ defined by $\phi(g) := (d_{j \pi}(g), g)$ and $\psi(g) := (0, g)$. I claim that $i: H \to G$ is the equalizer of the pair $\phi, \psi$. For,

$$\begin{array}{lcl} d_{j\pi}(g) = 0 & \text{iff} & (\forall_{g': G})\; g\cdot j\pi(g') = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j\pi(g' g) = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j(g' gH) = j(g' H) \\ & \text{iff} & (\forall_{g': G})\; g' g H = g' H \\ & \text{iff} & g H = H \\ & \text{iff} & g \in H. \end{array}$$

(All we needed was some injection $j: G/H \to A$ into an abelian group; I chose the canonical one.)

Edit: Peter LeFanu Lumsdaine asked in a comment whether it is indeed constructively true that one can embed any set (or object in a topos) into an abelian group (object), and then later answered this affirmatively, which supplements this answer. The link to this effort is buried in a comment below; it deserves to be made more visible here: Constructively, is the unit of the “free abelian group” monad on sets injective?

Answer 2

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.

Answer 3

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.

Answer 4

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.

[Added Oct 8]

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.