Name for the group generated by a groupoid Is there a name for a group generated by a groupoid?
I'm defining a groupoid as a category $\mathcal{C}$ where every arrow has a unique inverse that is both a left inverse and a right inverse.
I'm interested in ways of taking a groupoid and scrunching it down into a group. I'm secondarily curious about how much of the groupoid structure this construction preserves.

Suppose I have a groupoid $\mathcal{G}$ and I'm trying to turn it into a group $G$. Let's call the group operation $+$ for convenience regardless of whether it is commutative or not.
Let $X$ be the set of finite formal sums of $\mathcal{G}$ arrows.
Let's define the negation of a formal sum $a_1 + \cdots + a_n$ as $(-a_n) + \cdots + (-a_1)$.
Here are some rewrites on elements of $X$.
Suppose we have a finite sum $\cdots + a + b + \cdots $.
If $a + b$ is defined in $\mathcal{G}$, rewrite this to $\cdots + w + \cdots$ where $w$ is $a+b$ in $\mathcal{G}$.
Suppose any identity element of $\mathcal{G}$ appears anywhere in a sum, $\cdots + 0 + a + \cdots$. Let's remove it giving $\cdots + a + \cdots$.
Now let's define an equivalence relation.
Suppose $a \in X$ and $b \in X$. Then, $a \equiv b$ holds if and only if $a - b$ reduces to the empty formal sum.
Let's check that $\equiv$ is an equivalence relation.

*

*$a \equiv a$ holds because in $a + (-a)$ we can keep converting the innermost terms to identities and then dropping them.

*$a \equiv b$ holds if and only if $b \equiv a$ holds because any series of reduction steps that leads to the empty formal sum on the LHS can be applied in reverse to the RHS and vice versa.

*$a \equiv b$ and $b \equiv c$ implies $a \equiv c$. We can conclude $a - b \equiv 0$ and $b - c \equiv 0$ and thus $a -c \equiv 0$.

$\equiv$ is also a congruence.
I think this construction is equivalent to taking all the arrows of $\mathcal{G}$ as the set of generators and then imposing as relations:

*

*$\text{id}_X = 0$ for all objects $X$ in $\mathcal{G}$.

*All true equations about arrows of $\mathcal{G}$.

 A: $
\newcommand\G{\mathcal G}
\newcommand\F{\mathbb F}
$Preliminaries

*

*If $X$ is any set, the pair groupoid $P_X$ consists of the set $X\times X$, with operation defined by
$$
  (x,y)(z,w)=\left\{\matrix{
  (x,w), & \text {if } y=z,\cr
  \text{undefined}, & \text {otherwise}.\cr
  }\right.
  $$


*If $G$ is any group one may define a groupoid structure on the cartesian product  $G\times P_X$ by introducing the multiplication
$$
  (g,p)(h,q)=\left\{\matrix{
  (gh,pq), & \text {if $pq$ is defined} ,\cr
  \text{undefined}, & \text {otherwise}.\cr
  }\right.
  $$


*It is not hard to show that any groupoid is a disjoint union of a family of groupoids of the form $G\times P_X$ (the
multiplication being undefined when the factors come from two different subgroupoids).
OK, so now back to the question.
Given a groupoid $\G$ let us denote by $U(\G)$ the group obtained by scrunching  down $\G$, namely the group
generated by a set $\{[\gamma ]: \gamma \in \G\}$ subject to the relations $[\alpha ][\beta ]=[\alpha \beta ]$, whenever $\alpha \beta $ is defined in $\G$.
If $\G$ is the disjoint union of subgroupoids $\G_1$ and $\G_2$, it is fairly obvious that
$$
  U(\G) =   U(\G_1) *  U(\G_2),
  $$
(free product) so it is enough to describe $U(\G)$ for connected, or transitive, groupoids, all of which necessarily
have the form $G\times P_X$, as above.
Given such a groupoid, I claim that $U(G\times P_X)$ is isomorphic to the free product  $G*\F$, where $\F$ is the free
group generated by a set with one element less than $X$.
In order to prove it, let us first observe that $\F$ is isomorphic to the subgroup of $\F(X)$ (free group on
$X$) generated by the subset $\{xy^{-1}: x, y\in  X\}$, so this is the model for $\F$ we shall adopt.
Fixing some  $x_0$ in $X$,
observe that  the map
$$
  \varphi :\big [g,(x,y)\big ] \in  G\times P_X \mapsto  xx_0^{-1}\cdot g\cdot x_0y^{-1}\in  G*\F,
  $$
is compatible with the relations defining $U(G\times P_X)$, so it induces a group homomorphism
$$
  \Phi :U(G\times P_X)\to  G*\F,
  $$
which I claim is an isomorphism.
In order to exhibit an inverse for $\Phi $, let us first consider  the group homomorphism
$$
  \Delta  :\F(X) \to  U(G\times P_X),
  $$
specified on the generating set $X$ by
$$
  \Delta (x) = [1,(x, x_0)].
  $$
It might be worth observing that
$
  \Delta (xy^{-1}) = [1,(x, y)],
  $
for every $x$ and $y$ in $X$.
We then consider the unique group homomorphism
$$
  \Psi  :G*\F \to U(G\times P_X),
  $$
such that
$$
  \Psi (g)= [g,(x_0,x_0)],\quad \forall g\in G,
  $$
and
$$
  \Psi (w)=\Delta (w),\quad\forall w\in \F.
  $$
It is now easy to see that $\Phi $ and $\Psi $ are each other's inverse.
