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?

  • $\begingroup$ 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? $\endgroup$ Commented Oct 6, 2010 at 8:16
  • $\begingroup$ Yeah, this deserves some text so I'm editing the question. $\endgroup$
    – Monic Win
    Commented Oct 6, 2010 at 14:45
  • $\begingroup$ 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! $\endgroup$ Commented Oct 6, 2010 at 17:15
  • $\begingroup$ 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". $\endgroup$
    – Monic Win
    Commented Oct 6, 2010 at 17:58
  • $\begingroup$ 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. $\endgroup$ Commented Oct 7, 2010 at 1:56

4 Answers 4


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?

  • 1
    $\begingroup$ Maybe I’m missing something obvious, but it’s not clear to me how to show constructively that there’s any injection from $G/H$ into an Abelian group. If there is such an injection, then of course the unit map into the free Abelian group on $G/H$ is one, but I don’t see how to show the unit is injective other than by exhibiting such an injection explicitly. Of course classically one can take the embedding into e.g. $\mathbb{Z}^{G/H}$, but constructively this only works when $G/H$ has decidable equality, which brings us back to the case of decidable $H$, proven in the question. $\endgroup$ Commented Jun 8, 2018 at 13:34
  • 1
    $\begingroup$ @PeterLeFanuLumsdaine Interesting! Now that you bring it up, I'm not seeing it clearly either. In a topos it would suffice to embed $\Omega$ into an abelian group, but that doesn't necessarily bring us closer. (I'm fond of this argument though; it'd be a pity to have to retract it.) $\endgroup$
    – Todd Trimble
    Commented Jun 8, 2018 at 13:49
  • 1
    $\begingroup$ It would help if we could know anything specific about the free group $A$. Actually, I imagine naively that existence of free groups is not under question here? $\endgroup$ Commented Jun 8, 2018 at 13:55
  • 1
    $\begingroup$ I was thinking more about the free commutative monoid as a stepping stone, which I was thinking should be internally constructible as $\sum_{n: \mathbb{N}} X^n/\Sigma_n$ with $X$ embedding into the $n=1$ part, similar to the list monad. $\endgroup$
    – Todd Trimble
    Commented Jun 8, 2018 at 14:10
  • $\begingroup$ Existence of free commutative groups/monoids is fine — the free monoid is as Todd says, while the free group can similarly be taken as the quotient of $\mathrm{List}(\{+,1\} \times X)$ by the congruence generated by the group axioms. The problem for injectivity is with giving a more explicit description of this congruence. Commutative monoids are much easier — $X$ embeds as singletons in $\mathcal{P}(X)$, which is a commutative monoid under $\land$ or $\lor$. But $\mathcal{P}(X)$ is absorbing, so any map from it to a group is constant, so I don’t see how to use it as a stepping stone. $\endgroup$ Commented Jun 8, 2018 at 15:07

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.

  • $\begingroup$ 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. $\endgroup$
    – David Roberts
    Commented Nov 14, 2010 at 20:44
  • $\begingroup$ 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. $\endgroup$ Commented Nov 14, 2010 at 22:51
  • $\begingroup$ Paul, the discussion is by now ancient, but I added an answer where $\Pi$s do come into play. :-) $\endgroup$
    – Todd Trimble
    Commented Jun 20, 2017 at 12:24
  • $\begingroup$ Regarding the conjecture: it turns out that all closed subgroup inclusions between compact Hausdorff groups are equalizers. This is shown in D. Poguntke, Einige Eigenschaften des Darstellungsringes kompakter Gruppen, Math. Z. 130, 107-117 (1973) (link: pub.uni-bielefeld.de/download/1775049/2311754); see Satz 1.3 and Bemerkung 1.4, page 109. $\endgroup$
    – Todd Trimble
    Commented Feb 1, 2020 at 17:17
  • $\begingroup$ Both my answer and Todd's require List() in the category, which suggests arithmetic universes, but he says that the result also holds for compact Hausdorff groups. So any categorist interested in this question should look for a proof in a pretopos and whatever extra condition is required to work in both cases. $\endgroup$ Commented Feb 3, 2020 at 10:01

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.

  • $\begingroup$ @Andrej: just dropping a comment here so you get a notification about Paul Taylor’s answer below. $\endgroup$ Commented 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.

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

  • $\begingroup$ 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. $\endgroup$ Commented Oct 7, 2010 at 16:30
  • $\begingroup$ 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). $\endgroup$ Commented Oct 7, 2010 at 16:32
  • $\begingroup$ 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? $\endgroup$
    – Monic Win
    Commented Oct 7, 2010 at 20:26
  • $\begingroup$ Incidentally CZF is predicative. There are exponentials but no powersets (no subobject classifier). So I hope there is no need to go to toposes. $\endgroup$
    – Monic Win
    Commented Oct 7, 2010 at 20:29
  • 1
    $\begingroup$ And I might write a blog post. It's interesting to have a non-contrived constructive result which fails in PERs. $\endgroup$ Commented Oct 8, 2010 at 4:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.