Let $C$ be a category with finite products (and a terminal object). We can then define group objects as tuples $(G, m, e, inv)$ by requiring that the usual diagrams commute.
Is it true that the morphism $inv : G \to G$ is always an isomorphism?
It is certainly true for e.g. $C = \mathrm{Set}$, $C=\mathrm{Grp}$, $C=\mathrm{Top}$.
I would, in fact like to prove that $inv \circ inv = 1_G$. If it is true, the proof should be simple diagram chasing - but I have not been able to deduce the statement. Could you please provide a proof, hint, or reference?
I will show that $inv: G \to G$ is an isomorphism in our category $C$ by showing that $inv^2 = id$. That is, $inv$ composed with itself will be equal to the identity on $G$. If you wish to check that $inv$ is a group isomorphism (internal to $C$) you would of course need to check that it preserves the group structure (which it will).
Let's start by checking algebraically why applying $inv$ twice will be the identity, just for inspiration. So for the moment let us assume that $G$ is a group as usual in the category of sets. I will write $\star$ for the group multiplication, to make it explicit when it appears. For any $x \in G$ we have: $$ x = ((x^{-1})^{-1} \star x^{-1}) \star x = (x^{-1})^{-1} \star (x^{-1} \star x) = (x^{-1})^{-1}. $$ Next we translate this in terms of functions. We start with some $x \in G$ and send it to $((x^{-1})^{-1}, x^{-1}, x) \in G \times G \times G$. Then we obtain $(e, x)$ and $((x^{-1})^{-1}, e)$ in $G \times G$ by respectively multiplying the first two and last two coordinates. Applying the multiplication map again we get $x$ and $(x^{-1})^{-1}$ in $G$, which should be the same by associativity.
Now finally for the diagram. $$ \require{AMScd} \begin{CD} G @>{\langle inv^2, inv, id \rangle}>> G \times G \times G @>{id \times m}>> G \times G\\ @. @V{m \times id}VV @VV{m}V \\ @. G \times G @>{m}>> G \end{CD} $$ This diagram has to commute, because the square is the diagram expressing associativity. So going via the bottom route, we have $$ m \circ m \times id \circ \langle inv^2, inv, id \rangle = m \circ \langle e, id \rangle = id, $$ where the first equality is due to the commutativity of the diagram for the inverse map (precomposed with $inv$), and the second equality is the commutativity of the diagram for the identity element. Similarly, going via the top route we find $$ m \circ id \times m \circ \langle inv^2, inv, id \rangle = m \circ \langle inv^2, e \rangle = inv^2. $$ Since these two routes commute, we conclude that $inv^2 = id$, as required.