Definition (group object):
Let
be a category that has a terminal object, which we shall denote by
. A group object of
consists of
- an object
of
such that the categorical products
,
and
exist
- a morphism
, thought of as the multiplication morphism,
- a morphism
, thought of as the constant identity map (even though
may not even be a set)
- and a morphism
, thought of as the inversion morphism
which satisfy the following equations:
(identity law)
, where
shall denote the diagonal of
and
is the unique morphism given by the definition of a terminal object (inverse law)
, where
is the canonical isomorphism (associative law)
Here, we wrote
for the morphism that is induced by two maps
and
and the universal property of the product, by specifying that the map from
to
shall be given by
, and that the map from
to
shall be given by
.