a group is not the union of two proper subgroups - how to internalize this into other categories?

A well-known fact from group theory is that a group cannot be the union of two proper subgroups. I wonder, does this statement internalize into other categories than the category of sets? That is, is there some corresponding statement for group objects in, say, cartesian categories? It is certainly true for topoi, interpreted in a suitable way, since the usual proof is intuistic (however, note that $G=G_1 \cup G_2 \Rightarrow G=G_1 \vee G=G_2$ fails for disconnected topoi).

What about the following: Let $G:=(|G|,m,i,e)$ be a group object in the cartesian category $\mathcal{C}$. Let $G_1 \to G$ and $G_2 \to G$ be homomorphisms of group objects, which are no isomorphisms. Assume that $|G_1| \to |G|$ and $|G_2| \to |G|$ are monomorphisms. Is it not possible that $|G| \to |G|$ is their union, i.e. their sup in the preorder of subobjects of $|G|$?

Well as I've said, it fails for disconnected topoi. What do we have to assume on $\mathcal{C}$ so that it becomes true?

Solution 1:

First, another easy counterexample. Recall that an internal group in $\mathbf{Grp}$ is just an abelian group. So consider $G = \mathbb{Z} / 6 \mathbb{Z}$, let $G_1$ be the unique subgroup of order 2, and let $G_2$ be the unique subgroup of order 3. Then the smallest subgroup of $G$ containing $G_1$ and $G_2$ is $G$ itself, so the claim fails in $\mathbf{Grp}$ as well.

Now, for some slightly more positive results. Let's recall the standard proof. Let $G_1$ and $G_2$ be subgroups of $G$. Suppose $G = G_1 \cup G_2$, $g_1 \notin G_2$, $g_2 \notin G_1$. Consider $g_1 g_2$. If $g_1 g_2 \in G_1$, then $g_2 \in G_1$, a contradiction; and if $g_1 g_2 \in G_2$, then $g_1 \in G_2$ , also a contradiction. Thus, $g_1 g_2 \notin G_1 \cup G_2$, so $G \ne G_1 \cup G_2$.

As you say, this is intuitionistically valid. In fact it can even be interpreted in any coherent category. The only problem is that it does not mean what you think it means! The right formulation is the following:

If $G_1$ and $G_2$ are subgroups of $G$ and we (simultaneously) have (generalised) elements of $G \setminus G_1$ and $G \setminus G_2$, then $G \ne G_1 \cup G_2$.

More formally, $$g_1 \notin G_2, g_2 \notin G_1 \vdash_{g_1 : G, g_2 : G} \lnot (\forall g : G . g \in G_1 \lor g \in G_2)$$ but having $g_2 \notin G_1$ is generally a stronger condition than $G_1 \hookrightarrow G$ not being an isomorphism. In general, $G_1 \hookrightarrow G$ in an isomorphism (in a topos) if and only if the following formula holds in the internal logic: $$\forall g : G . g \in G_1$$ Unfortunately, it is not possible to express internally that a formula does not hold! Although we may write $$\lnot (\forall g : G . g \in G_1)$$ the above formula asserts that $G_1 \hookrightarrow G$ is not even an isomorphism locally: in a topos, the above formula is valid if and only if, for every $U$, the induced map $\mathrm{Hom}(U, G_1) \to \mathrm{Hom}(U, G)$ is not a surjection. Clearly, this is a stronger condition than $G_1 \hookrightarrow G$ not being an isomorphism.

Nonetheless, we may deduce that the claim is true for complemented proper subgroups $G_1$, $G_2$ in a topos in which the subobjects of $1$ form an irreducible locale: because under these hypotheses, the locus $U$ over which both $G \setminus G_1$ and $G \setminus G_2$ is inhabited is non-empty, so $G \ne G_1 \cup G_2$ in the topos over $U$. But this is enough to prove $G \ne G_1 \cup G_2$ globally as well – because passing to the topos over $U$ is a logical functor.

Postscript. A more sophisticated approach allows us to deduce another version of the claim. Suppose we have subgroups $G_1$ and $G_2$ of an internal group $G$ in a topos such that $G_1 \times G \cup G \times G_2$ is a proper subobject of $G \times G$. Noting that $G = G_1 \cup G_2$ if and only if this is true in all covers of the topos, by passing to a boolean cover if necessary, we may assume the law of excluded middle. But then in that case it is clear that $$(G \setminus G_1) \times (G \setminus G_2) = (G \times G) \setminus (G_1 \times G \cup G \times G_2)$$ so the LHS is non-empty. Thus we have reduced the question to the well-known case.