Group Theory/Groups with structure

Definition (group with structure):

Let ${\mathcal {C}}$ be a concrete category. Then the category of groups with structure is the subcategory of ${\mathcal {C}}$ which is defined as follows:

• Its objects are the objects $G$ of ${\mathcal {C}}$ such that the categorical product $G\times G$ exists (and, on a set level, equals the set-theoretic product of $G$ with itself, projections included) and whose underlying sets bear a group structure such that the group law is a morphism $G\times G\to G$ in ${\mathcal {C}}$ and inversion is a morphism $G\to G$ in ${\mathcal {C}}$.
• Its morphisms are morphisms $f:G\to G'$ in ${\mathcal {C}}$ that, on the set level, are also group homomorphisms.

Proposition (multipication by an element is an automorphism in the underlying concrete category for every group with structure in a category admitting enough constant morphisms):

Let $G$ be a group with structure whose additional structure is given by the concrete category ${\mathcal {C}}$, such that every constant morphism $G\to G$ is a morphism of ${\mathcal {C}}$. Further, suppose that $g\in G$. Then the function

$G\to G,h\mapsto gh$

is an automorphism of $G$ in the category ${\mathcal {C}}$.

Proof: If we show that the given function is a morphism, we've completed the proof, since an inverse is given by left multiplication by $g^{-1}$.

Thus, consider the morphism $G\to G\times G$ whose first component is given by the constant function associated to $g$ and whose second component is given by the identity on $G$: Postcomposing it with the group law yields the morphism in the theorem statement, which is hence a morphism of ${\mathcal {C}}$. $\Box$