Characterization of internal groupoids via pullbacks

Question

The most intuitive way (for me) to define an internal groupoid is as an internal category with extra structure, namely an involution on the object of morphisms which "produces inverses".

In Borceux and Janelidze's Galois Theories, section 7.1, the authors remark that an internal category is an internal groupoid if and only if the commutative squares below - which are part of the structure of an internal category - are pullbacks. This means being an internal groupoid is a property of an internal category.

$$\require{AMScd} \begin{CD} C_2 @>{m}>> C_1\\ @V{f_0}VV @VV{d_0}V\\ C_1 @>>{d_0}> C_0 \end{CD}\;\;\;\;\ \begin{CD} C_2 @>{m}>> C_1\\ @V{f_1}VV @VV{d_1}V\\ C_1 @>>{d_1}> C_0 \end{CD}$$

I think I understand the idea: the left square being a pullback means that composable pairs are identifiable both composable pairs of arrows sharing the same domain, where the correspondence is just given by composing the composite arrow on the inverse of the first. Analogously for the right pullback square.

However, the authors leave the proof as an exercise, and I'm not sure how to proceed formally (or whether I'm even correct).

How to prove this characterization of internal groupoids?

Answer 1

Let me write $d_0 = t$ and $d_1 = s$ for target and source of a morphism, because otherwise I will get confused.

Your intuition is correct. Recall that $C_1$ is the set of morphisms, $$C_2 = \{ (f_0, f_1) \in C_1 \times C_1 \mid s(f_0) = t(f_1) \}$$ is the set of composable morphisms, and $m : C_2 \to C_1$ is composition $m(f_0, f_1) = f_0 \circ f_1$. Then your first diagram being a pullback means that, to gives a composable pair $(f_0, f_1)$, is the same thing as to give their composition $f_0 \circ f_1$ and to give $f_0$. The other diagram is the same thing but replacing the last $f_0$ by $f_1$.

Armed with this, how would we define $\tau : C_1 \to C_1$ if we were dealing with sets? For $f : A \to B$, $\tau(f)$ is supposed to be the morphism such that $\tau(f) \circ f = \operatorname{id}_A$ and $f \circ \tau(f) = \operatorname{id}_B$. So if we consider the composable pair $(\tau(f), f) \in C_2$, we know their composite $\tau(f) \circ f = \operatorname{id}_A$, and we know the second factor, $f$. The cartesianness of the second square means that we can recover $\tau(f)$ from this.

So let's define first a morphism $C_1 \to C_2$ using the second pullback square (informally taking $f$ to $(\tau(f), f)$). The composite has to be the identity $\operatorname{id}_A$, so for the first $h_1 : C_1 \to C_1$ we take $n \circ s = n \circ d_1$. The second $h_2 : C_1 \to C_1$ is just the identity. By the axioms of internal categories, $d_1 \circ h_1 = d_1 \circ h_2$ (not hard to check). Thus there exists a unique morphism $h : C_1 \to C_2$ such that $m \circ h = h_1 = n \circ d_1$ and $f_1 \circ h = h_2 = \operatorname{id}_{C_1}$. Now define: $$\tau = f_0 \circ h : C_1 \to C_2 \to C_1.$$ It is now a game of thrones commutative square to check that all the axioms of an internal groupoid are satisfied with this $\tau$. It's a bit tedious, but it's a good exercise (you will have to use the cartesianness of the first square at some point, which I haven't used so far).