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?
Best Answer
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?