Ambiguity in the definition of group objects

Given a category $C$ with finite products and a terminal object, the usual definition of a group object $G$ in $C$ specifies certain morphisms along with commutativity of certain diagrams involving these morphisms. For example, we need a multiplication morphism $\mu : G\times G \to G$. But $G \times G$ isn't an object of $C$ as it is only well-defined up to isomorphism. Similarly, there is an ambiguity in the choice of the terminal object. Of course, up to isomorphism we'll end up getting the same thing, but is there a clean way to state this definition of group objects which avoids this ambiguity?

One thing one could do is to fix a choice (ignoring set-theoretical issues if there are any) of finite product object along with the projection maps for every finite collection of objects; then one gets well-defined product multifunctors. Using these choices, the definition of group objects becomes precise, but I assume that there is a better way to do this, without having to make choices.

On the wiki page, an equivalent definition for group objects is given: "Another way to state the above is to say $G$ is a group object in a category $C$ if for every object $X$ in $C$, there is a group structure on the morphisms $\text{hom}(X,G)$ from $X$ to $G$ such that the association of $X$ to $\text{hom}(X,G)$ is a (contravariant) functor from $C$ to the category of groups." This has no ambiguity, but I'm not sure how to translate it to an ambiguity-free definition of the other form.

Thanks.

• You could say "An internal group is an object $G$, together with a product $(G\times G, p_1,p_2)$ of $G$, a terminal object $1$ and morphisms $\dots$". – Stefan Perko Apr 16 '16 at 17:52
• Products and terminal objects are better than unique up to isomorphism: they're unique up to unique isomorphism. This is enough uniqueness that there are no problems in practice. – Qiaochu Yuan Apr 16 '16 at 18:04
• @StefanPerko Thanks, I guess I could. To formulate associativity though then I'd also have to make choices for $G \times (G \times G), (G \times G) \times G$ and associated projections, which I suppose is okay, but I wonder if there's a neater way to do it? – Santiago Apr 16 '16 at 18:12
• @QiaochuYuan I should've been more precise; I do understand that there is more uniqueness than what I stated and so that in practice there will never be problems, just wondering if there's a nice unambiguous way to write the definition down that's all. – Santiago Apr 16 '16 at 18:14
• This sort of "ambiguity" causes no problems at all! Things like this can happen for the traditional definition of group: someone might define $G \times G$ as a set of Kuratowski pairs (i.e., $(g,h) = \{\{g\},\{g,h\}\}$); someone else might think $G \times G = G^2$ is the set of functions $\{0,1\} \to G$; a third person might prefer "short pairs" $(g,h) = \{g,\{g,h\}\}$ or functions with domain $\{1,2\}$, etc. These hypothetical people are unlikely to even notice they are talking about different sets $G \times G$! – Omar Antolín-Camarena Apr 17 '16 at 1:47

Write it down as a product-preserving functor from the Lawvere theory of groups, $\mathcal{G}$, a certain category encoding all the data available in a group. This amounts to making a choice of object and projections for all finite powers of $G$ and of all partial multiplication maps, all of which are consistent with each other. This perspective also makes the equivalent characterization clear-to give a functor from $\mathcal{G}$ with base object $X$ is equivalent to giving a functor from $\mathcal{G}$ with base $C(-,X)$ when products of $X$ exist, by the Yoneda lemma in one direction and the fact that the Yoneda embedding preserves products in the other. Note that if such products don't exist, this equivalence does not hold. If $X$ is the sole object of $BG$, some group $G$ seen as a category, then of course $X$ is a group object in the representable sense, but not in the usual sense since there are no nontrivial products in $BG$ if $G$ is nontrivial.