The purpose of this article is to answer the question: what is the coproduct
of two groups? The approach, however, will be somewhat absurd. Instead of
simply presenting a construction and proving that it satisfies the appropriate
universal property, I want to find the general answer and simply instantiate
it for the case of groups.
Specifically, this will be a path through the theory of Lawvere theories and
their models with the goal of motivating some of the theory around it in
pursuit of the answer to this relatively simple question.
If you really just want to know the answer to the title question, then the
construction is usually called the free product
and is described on the linked Wikipedia page.
Groups as Models of a Lawvere Theory
A group is a model of an equational theory. This means a group is described by a set
equipped with a collection of operations that must satisfy some equations. So we’d
have a set, , and operations , ,
and . These operations satisfy the equations,
universally quantified over , , and .
These equations can easily be represented by commutative diagrams, i.e. equations
of compositions of arrows, in any category with finite products of an object, ,
with itself. For example, the left inverse law becomes:
where is the unique arrow into the terminal object corresponding
to the -ary product of copies of .
One nice thing about this categorical description is that we can now talk about
a group object in any category with finite products. Even better, we can make this
pattern describing what a group is first-class. The (Lawvere) theory of a
group is a (small) category, whose objects are an object and
all its powers, , where
and . The arrows consist
of the relevant projection and tupling operations, the three arrows above,
, ,
, and all composites that could
be made with these arrows. See my previous article
for a more explicit description of this, but it should be fairly intuitive.
An actual group is then, simply, a finite-product-preserving functor
. It must be finite-product-preserving
so the image of actually gets sent to a binary function
and not some function with some arbitrary domain. The category, , of
groups and group homomorphisms is equivalent to the category
which is defined to be the full subcategory of the category of functors from
consisting of the functors which preserve finite products. While we’ll not explore it more
here, we could use any category with finite products as the target, not just .
For example, we’ll show that has finite products, and in fact all limits
and colimits, so we can talk about the models of the theory of groups in the
category of groups. This turns out to be equivalent to the category of Abelian
groups via the well-known Eckmann-Hilton argument.
A Bit of Organization
First, a construction that will become even more useful later. Given any category, ,
we define , or, more precisely, an inclusion
to be the free category-with-finite-products generated from. Its universal property is:
given any functor into a category-with-finite-products ,
there exists a unique finite-product-preserving functor
such that .
An explicit construction of is the following. Its objects consist
of (finite) lists of objects of with concatenation as the categorical product
and the empty list as the terminal object. The arrows are tuples with a component for each
object in the codomain list. Each component is a pair of an index into the domain list and
an arrow from the corresponding object in the domain list to the object in the codomain list
for this component. For example, the arrow would be .
Identity and composition is straightforward. then maps each object to a singleton
list and each arrow to .
Like most free constructions, this construction completely ignores any finite products the
original category may have had. In particular, we want the category
, called the theory of a set.
The fact that the one object of the category is terminal has nothing to do
with its image via which is not the terminal object.
We now define the general notion of a (Lawvere) theory as a small category
with finite products, , equipped with a finite-product-preserving, identity-on-objects
functor . A morphism of (Lawvere) theories
is a finite-product-preserving functor that preserves these inclusions a la:
The identity-on-objects aspect of the inclusion of
along with finite-product-preservation ensures that the only objects in
are powers of a single object which we’ll generically call . This is
sometimes called the “generic object”, though the term “generic object” has other
meanings in category theory.
A model of a theory (in ) is then simply a finite-product-preserving
functor into . is the full subcategory
of functors from which preserve finite products.
The morphisms of models are simply the natural transformations. As an exercise,
you should show that for a natural transformation where
and are two models of the same theory, .
The Easy Categorical Constructions
This relatively simple definition of model already gives us a large swathe of results.
An easy result in basic category theory is that (co)limits in functor
categories are computed pointwise whenever the corresponding (co)limits exist
in the codomain category. In our case, has all (co)limits, so
all categories of -valued functors have all (co)limits and they
are computed pointwise.
However, the (co)limit of finite-product-preserving functors into
may not be finite-product-preserving, so we don’t immediately get that
has all (co)limits (and they are computed pointwise). That said, finite products
are limits and limits commute with each other, so we do get that
has all limits and they are computed pointwise. Similarly, sifted colimits, which are
colimits that commute with finite products in also exist and are
computed pointwise in . Sifted colimits include the
better known filtered colimits which commute with all finite limits.
I’ll not elaborate on sifted colimits.
We’re here for (finite) coproducts, and, as you’ve probably already guessed,
coproducts are not sifted colimits.
When the Coproduct of Groups is Easy
There is one class of groups whose coproduct is easy to compute for
general reasons: the free groups. The free group construction, like
most “free constructions”, is a left adjoint and left adjoints
preserve colimits, so the coproduct of two free groups is just the
free group on the coproduct, i.e. disjoint union, of their generating
sets. We haven’t defined the free group yet, though.
Normally, the free group construction would be defined as left
adjoint to the underlying set functor. We have a very straightforward
way to define the underlying set functor. Define
as and .
Identifying with the functor
we have giving a functor
which we identify with a set. The left adjoint to precomposition
by is the left Kan extension along .
We then compute . This is the left
Kan extension and does form an adjunction but not with the category
of models because the functor produced by does not preserve finite products.
We should have , but substituting
in the definition of clearly does not satisfy this. For example,
consider .
We can and will show that the left Kan extension of a functor into
preserves finite products when the original functor did. Once
we have that result we can correct our definition of the free construction.
We simply replace with a functor that
does preserve finite products, namely .
Of course, is exactly our definition of .
We see now that a model of is the same thing as having
a set, hence the name. Indeed, we have an equivalence of categories between
and . (More generally, this theory is called
“the theory of an object” as we may consider models in categories other than ,
and we’ll still have this relation.)
The correct definition of is
where is the inclusion
we give as part of the definition of a theory. We can also see as .
We can start to see the term algebra in this definition. An element of is
a choice of , an -tuple of elements of , and a (potentially compound) -ary operation.
We can think of an element of as a term with
free variables which we’ll label with the elements of in . The equivalence
relation in the explicit construction of the coend allows us to swap projections and
tupling morphisms from the term to the tuple of labels. For example, it equates a
unary term paired with one label with a binary term paired with two labels but where
the binary term immediately discards one of its inputs. Essentially, if you are
given a unary term and two labels, you can either discard one of the labels or you
can make the unary term binary by precomposing with a projection. Similarly for
tupling.
It’s still not obvious this definition produces a functor which preserves finite products.
As a lemma to help in the proof of that fact, we have a bit of coend calculus.
Lemma 1: Let and .
Then, when one, and thus both, exist. Proof:
Using the adjunctions
and , where we’re treating as the functor
which picks out a terminal object of ,
gives the following corollary.
Corollary 2: For any ,
when
both exists and for any , .
The former allows us to combine two (co)ends into one. The latter reproduces a standard result about
colimits over diagrams whose index category has a terminal object.
Now our theorem.
Theorem 3: Let and
where and have finite products. Then
preserves finite products if does.
Proof:
and for the 0-ary product case:
The Coproduct of Groups
To get general coproducts (and all colimits), we’ll show that
is a reflective subcategory of . Write
.
If we had a functor such that , then we have
which allows us to quickly produce colimits
in the subcategory via .
It’s easy to verify that has the appropriate universal property
to be .
We’ll compute by composing two adjunctions. First,
we have .
This is essentially the universal property of .
When has finite products, which, of course, we’re assuming,
then we can use the universal property of to factor
into . The second adjunction is then .
The left adjoint sends finite-product-preserving functors to finite-product-preserving functors
via Theorem 3. The right adjoint is the composition of finite-product-preserving functors.
The composite of the left adjoints is .
The composite of the right adjoint is
where we view the list as a -tuple with components .
This construction of the reflector, , is quite similar to the free construction.
The main difference is that here we factor via where there we factored
via .
Let’s now explicitly describe the coproducts via . As a warm-up, we’ll consider the initial object, i.e.
nullary coproducts. We consider . Because , the only case in the coend
that isn’t is when so the underlying set of the coend reduces to
, i.e. the nullary terms. For groups, this is just the unit
element. For bounded lattices, it would be the two element set consisting of the top and bottom elements.
For lattices without bounds, it would be the empty set. Of course, matches , i.e.
the free model on .
Next, we consider two models and . First, we compute to the coproduct of and as (plain)
functors which is just computed pointwise, i.e. .
Considering the case where for all and where , which
subsumes all the other cases, we see we have a term with free variables each labelled by either
an element of or an element of . If we normalized the term into a list of variables representing
a product of variables, then we’d have a essentially a word as described on the Wikipedia page
for the free product. If we then only considered
quotienting by the equivalences induced by projection and tupling, we’d have the free group on the
disjoint union of the underlying sets of the and . However, for , we quotient also by
the action of the other operations. The lists of objects with come in here
to support equating non-unary ops. For example, a pair of the binary term and
the 2-tuple of elements for , will be equated with the pair of
the unary term and the 1-tuple of elements where in . Similarly for
and the other operations (and terms generally). Ultimately, the quotient identifies every
element with an element that consists of a pair of a term that is a fully right associated
set of multiplications ending in a unit where each variable is labelled with an element from
or in an alternating fashion. These are the reduced words in the Wikipedia
article.
This, perhaps combined with a more explicit spelling out of the equivalence relation, should make
it clear that this construction does actually correspond to the usual free product construction.
The name “free product” is also made a bit clearer, as we are essentially building the free
group on the disjoint union of the underlying sets of the inputs, and then quotienting that to
get the result. While there are some categorical treatments of normalization, the normalization
arguments used above were not guided by the category theory. The (underlying sets of the) models
produced by the above and functors big equivalence classes of “terms”. The above constructions
provide no guidance for finding “good” representatives of those equivalence classes.
Conclusions
This was, of course, a very complex and round-about way of answering the title question.
Obviously the real goal was illustrating these ideas and illustrating how “abstract” categorical
reasoning can lead to relatively “concrete” results. Of course, these concrete constructions
are derived from other concrete constructions, usually concrete constructions of limits and
colimits in . That said, category theory allows you to get a lot from a small
collection of relatively simple concrete constructions. Essentially, category theory is like
a programming language with a small set of primitives. You can write “abstract” programs in
terms of that language, but once you provide an “implementation” for those primitives, all
those “abstract” programs can be made concrete.
I picked (finite) coproducts, in particular, as they are where a bunch of complexity suddenly
arises when studying algebraic objects categorically, but (finite) coproducts are still
fairly simple.
For Lawvere theories, one thing to note is that the Lawvere theory is independent of the
presentation. Any presentation of the axioms of a group would give rise to the same Lawvere
theory. Of course, to explicitly describe the category would end up requiring a presentation
of the category anyway. Beyond Lawvere theories are algebraic theories and algebraic categories,
and further into essentially algebraic theories and categories. These extend to the multi-sorted
case and then into the finite limit preserving case. The theory of categories, for example,
cannot be presented as a Lawvere theory but is an essentially algebraic theory. There’s much
more that can be said even about specifically Lawvere theories, both from a theoretical
perspective, starting with monadicity, and from practical perspectives like algebraic effects.
Familiarity with the properties of functor categories, and especially categories of (co)presheaves
was behind many of these results, and many that I only mentioned in passing. It is always
useful to learn more about categories of presheaves. That said, most of the theory works
in an enriched context and often without too many assumptions. The fact that all we need
to talk about models is for the codomains of the functors to have finite products allows
quite broad application. We can talk about algebraic objects almost anywhere. For example,
sheaves of rings, groups, etc. can equivalently be described as models of the theories of
rings, groups, etc. in sheaves of sets.
Kan extensions unsurprisingly played a large role, as they almost always do when you’re
talking about (co)presheaves. One of the motivations for me to make this article was
a happy confluence of things I was reading leading to a nice, coend calculus way of
describing and proving finite-product-preservation for free models.
Thinking about what exactly was going on around finite-product-preservation was fairly interesting.
The incorrect definition of the free model functor could be corrected in a different
(though, of course, ultimately equivalent) way. The key is to remember that the coend
formula for the left Kan extension is generally a copower and not a cartesian product.
The copower for -valued functors is different from the copower for
finite-product-preserving -valued functors. For a category with (arbitrary)
coproducts, the copower corresponds to the coproduct of a constant family. We get,
as is immediately
evident from being a left adjoint and a set being the coproduct of -many times.
For the purposes of this article, this would have been less than satisfying as figuring
out what coproducts were was the nominal point.
That said, it isn’t completely unsatisfying
as this defines the free model in terms of a coproduct of, specifically, representables
and those are more tractable. In particular, an easy and neat exercise is to work
out what is.
Just use Yoneda and work out what must be true of the mapping out property, and remember
that the object you’re mapping into preserves finite products. Once you have finite
coproducts described, you can get all the rest via filtered colimits, and since those
commute with finite products that gives us arbitrary coproducts.