What is the coproduct of two groups?

Introduction

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, |G|, and operations |\mathtt{e} : () \to G|, |\mathtt{i} : G \to G|, and |\mathtt{m} : G \times G \to G|. These operations satisfy the equations, \[ \begin{align} \mathtt{m}(\mathtt{m}(x, y), z) = \mathtt{m}(x, \mathtt{m}(y, z)) \\ \mathtt{m}(\mathtt{e}(), x) = x = \mathtt{m}(x, \mathtt{e}()) \\ \mathtt{m}(\mathtt{i}(x), x) = \mathtt{e}() = \mathtt{m}(x, \mathtt{i}(x)) \end{align} \] universally quantified over |x|, |y|, and |z|.

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, |G|, with itself. For example, the left inverse law becomes: \[ \mathtt{m} \circ (\mathtt{i} \times id_G) = \mathtt{e} \circ {!}_G \] where |{!}_G : G \to 1| is the unique arrow into the terminal object corresponding to the |0|-ary product of copies of |G|.

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, |\mathcal{T}_{\mathbf{Grp}}| whose objects are an object |\mathsf{G}| and all its powers, |\mathsf{G}^n|, where |\mathsf{G}^0 = 1| and |\mathsf{G}^{n+1} = \mathsf{G} \times \mathsf{G}^n|. The arrows consist of the relevant projection and tupling operations, the three arrows above, |\mathsf{m} : \mathsf{G}^2 \to \mathsf{G}^1|, |\mathsf{i} : \mathsf{G}^1 \to \mathsf{G}^1|, |\mathsf{e} : \mathsf{G}^0 \to \mathsf{G}^1|, 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 |\mathcal{T}_{\mathbf{Grp}} \to \mathbf{Set}|. It must be finite-product-preserving so the image of |\mathsf{m}| actually gets sent to a binary function and not some function with some arbitrary domain. The category, |\mathbf{Grp}|, of groups and group homomorphisms is equivalent to the category |\mathbf{Mod}_{\mathcal{T}_{\mathbf{Grp}}}| which is defined to be the full subcategory of the category of functors from |\mathcal{T}_{\mathbf{Grp}} \to \mathbf{Set}| 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 |\mathbf{Set}|. For example, we’ll show that |\mathbf{Grp}| 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, |\mathcal{C}|, we define |\mathcal{C}^{\times}|, or, more precisely, an inclusion |\sigma : \mathcal{C} \hookrightarrow \mathcal{C}^{\times}| to be the free category-with-finite-products generated from |\mathcal{C}|. Its universal property is: given any functor |F : \mathcal{C} \to \mathcal{E}| into a category-with-finite-products |\mathcal E|, there exists a unique finite-product-preserving functor |\bar{F} : \mathcal{C}^{\times} \to \mathcal E| such that |F = \bar{F} \circ \sigma|.

An explicit construction of |\mathcal{C}^{\times}| is the following. Its objects consist of (finite) lists of objects of |\mathcal{C}| 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 |[A, B] \to [B, A]| would be |((1, id_B), (0, id_A))|. Identity and composition is straightforward. |\sigma| then maps each object to a singleton list and each arrow |f| to |((0, f))|.

Like most free constructions, this construction completely ignores any finite products the original category may have had. In particular, we want the category |\mathcal{T}_{\mathbf{Set}} = \mathbf{1}^{\times}|, called the theory of a set. The fact that the one object of the category |\mathbf{1}| is terminal has nothing to do with its image via |\sigma| which is not the terminal object.

We now define the general notion of a (Lawvere) theory as a small category with finite products, |\mathcal{T}|, equipped with a finite-product-preserving, identity-on-objects functor |\mathcal{T}_{\mathbf{Set}} \to \mathcal{T}|. A morphism of (Lawvere) theories is a finite-product-preserving functor that preserves these inclusions a la: \[ \xymatrix { & \mathcal{T}_{\mathbf{Set}} \ar[dl] \ar[dr] & \\ \mathcal{T}_1 \ar[rr] & & \mathcal{T}_2 } \]

The identity-on-objects aspect of the inclusion of |\mathcal{T}_{\mathbf{Set}}| along with finite-product-preservation ensures that the only objects in |\mathcal{T}| are powers of a single object which we’ll generically call |\mathsf{G}|. This is sometimes called the “generic object”, though the term “generic object” has other meanings in category theory.

A model of a theory (in |\mathbf{Set}|) is then simply a finite-product-preserving functor into |\mathbf{Set}|. |\mathbf{Mod}_{\mathcal{T}}| is the full subcategory of functors from |\mathcal{T} \to \mathbf{Set}| which preserve finite products. The morphisms of models are simply the natural transformations. As an exercise, you should show that for a natural transformation |\tau : M \to N| where |M| and |N| are two models of the same theory, |\tau_{\mathsf{G}^n} = \tau_{\mathsf{G}}^n|.

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, |\mathbf{Set}| has all (co)limits, so all categories of |\mathbf{Set}|-valued functors have all (co)limits and they are computed pointwise.

However, the (co)limit of finite-product-preserving functors into |\mathbf{Set}| may not be finite-product-preserving, so we don’t immediately get that |\mathbf{Mod}_{\mathcal{T}}| 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 |\mathbf{Mod}_{\mathcal{T}}| has all limits and they are computed pointwise. Similarly, sifted colimits, which are colimits that commute with finite products in |\mathbf{Set}| also exist and are computed pointwise in |\mathbf{Mod}_{\mathcal{T}}|. 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 |U : \mathbf{Mod}_{\mathcal T} \to \mathbf{Set}| as |U(M) = M(\mathsf{G}^1)| and |U(\tau) = \tau_{\mathsf{G}^1}|. Identifying |\mathsf{G}^1| with the functor |\mathsf G : \mathbf{1} \to \mathcal{T}| we have |U(M) = M \circ \mathsf{G}| giving a functor |\mathbf{1} \to \mathbf{Set}| which we identify with a set. The left adjoint to precomposition by |\mathsf{G}| is the left Kan extension along |\mathsf{G}|.

We then compute |F(S) = \mathrm{Lan}_{\mathsf{G}}(S) \cong \int^{{*} : \mathbf{1}} \mathcal{T}(\mathsf{G}({*}), {-}) \times S({*}) \cong \mathcal{T}(\mathsf{G}^1, {-}) \times S|. This is the left Kan extension and does form an adjunction but not with the category of models because the functor produced by |F(S)| does not preserve finite products. We should have |F(S)(\mathsf{G}^n) \cong F(S)(\mathsf{G})^n|, but substituting in the definition of |F(S)| clearly does not satisfy this. For example, consider |F(\varnothing)(\mathsf{G}^0)|.

We can and will show that the left Kan extension of a functor into |\mathbf{Set}| 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 |S : \mathbf{1} \to \mathbf{Set}| with a functor that does preserve finite products, namely |\bar{S} : \mathbf{1}^{\times} \to \mathbf{Set}|. Of course, |\mathbf{1}^{\times}| is exactly our definition of |\mathcal{T}_{\mathbf{Set}}|. We see now that a model of |\mathcal{T}_{\mathbf{Set}}| is the same thing as having a set, hence the name. Indeed, we have an equivalence of categories between |\mathbf{Set}| and |\mathbf{Mod}_{\mathcal{T}_{\mathbf{Set}}}|. (More generally, this theory is called “the theory of an object” as we may consider models in categories other than |\mathbf{Set}|, and we’ll still have this relation.)

The correct definition of |F| is |F(S) = \mathrm{Lan}_{\iota}(\bar S) \cong \int^{\mathsf{G}^n:\mathcal{T}_{\mathbf{Set}}} \mathcal{T}(\iota(\mathsf{G}^n), {-}) \times \bar{S}(\mathsf{G}^n) \cong \int^{\mathsf{G}^n:\mathcal{T}_{\mathbf{Set}}} \mathcal{T}(\iota(\mathsf{G}^n), {-}) \times S^n| where |\iota : \mathcal{T}_{\mathbf{Set}} \to \mathcal{T}| is the inclusion we give as part of the definition of a theory. We can also see |\iota| as |\bar{\mathsf{G}}|.

We can start to see the term algebra in this definition. An element of |F(S)| is a choice of |n|, an |n|-tuple of elements of |S|, and a (potentially compound) |n|-ary operation. We can think of an element of |\mathcal{T}(\mathsf{G}^n, {-})| as a term with |n| free variables which we’ll label with the elements of |S^n| in |F(S)|. 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 |F \dashv U : \mathcal{D} \to \mathcal{C}| and |H : \mathcal D^{op} \times \mathcal{C} \to \mathcal{E}|. Then, |\int^C H(FC, C) \cong \int^D H(D, UD)| when one, and thus both, exist. Proof: \[ \begin{align} \mathcal{E}\left(\int^C H(FC, C), {-}\right) & \cong \int_C \mathcal{E}(H(FC, C), {-}) \tag{continuity} \\ & \cong \int_C \int_D [\mathcal{D}(FC, D), \mathcal{E}(H(D, C), {-})] \tag{Yoneda} \\ & \cong \int_C \int_D [\mathcal{C}(C, UD), \mathcal{E}(H(D, C), {-})] \tag{adjunction} \\ & \cong \int_D \int_C [\mathcal{C}(C, UD), \mathcal{E}(H(D, C), {-})] \tag{Fubini} \\ & \cong \int_D \mathcal{E}(H(D, UD), {-}) \tag{Yoneda} \\ & \cong \mathcal{E}\left(\int^D H(D, UD), {-}\right) \tag{continuity} \\ & \square \end{align} \]

Using the adjunction |\Delta \dashv \times : \mathcal{C} \times \mathcal{C}\to \mathcal{C}| gives the following corollary.

Corollary 2: For any |H : \mathcal{C}^{op} \times \mathcal{C}^{op} \times \mathcal{C} \to \mathcal{E}|, \[\int^{C} H(C, C, C) \cong \int^{C_1}\int^{C_2} H(C_1, C_2, C_1 \times C_2)\] when both exists. This allows us to combine two (co)ends into one.

Now our theorem.

Theorem 3: Let |F : \mathcal{T}_1 \to \mathbf{Set}| and |J : \mathcal{T}_1 \to \mathcal{T}_2| where |\mathcal{T}_1| and |\mathcal{T}_2| have finite products. Then |\mathrm{Lan}_J(F)| preserves finite products if |F| does.

Proof: \[ \begin{flalign} \mathrm{Lan}_J(F)(X \times Y) & \cong \int^A \mathcal{T}_2(J(A), X \times Y) \times F(A) \tag{coend formula for left Kan extension} \\ & \cong \int^A \mathcal{T}_2(J(A), X) \times \mathcal{T}_2(J(A), Y) \times F(A) \tag{continuity} \\ & \cong \int^{A_1}\int^{A_2}\mathcal{T}_2(J(A_1), X) \times \mathcal{T}_2(J(A_2), Y) \times F(A_1 \times A_2) \tag{Corollary 2} \\ & \cong \int^{A_1}\int^{A_2}\mathcal{T}_2(J(A_1), X) \times \mathcal{T}_2(J(A_2), Y) \times F(A_1) \times F(A_2) \tag{finite product preservation} \\ & \cong \left(\int^{A_1}\mathcal{T}_2(J(A_1), X) \times F(A_1) \right) \times \left(\int^{A_2}\mathcal{T}_2(J(A_2), Y) \times F(A_2)\right) \tag{commutativity and cocontinuity of $\times$} \\ & \cong \mathrm{Lan}_J(F)(X) \times \mathrm{Lan}_J(F)(Y) \tag{coend formula for left Kan extension} \\ & \square \end{flalign} \]

The Coproduct of Groups

To get general coproducts (and all colimits), we’ll show that |\mathbf{Mod}_{\mathcal{T}}| is a reflective subcategory of |[\mathcal{T}, \mathbf{Set}]|. Write |\iota : \mathbf{Mod}_{\mathcal{T}} \hookrightarrow [\mathcal{T}, \mathbf{Set}]|. If we had a functor |R| such that |R \dashv \iota|, then we have |R \circ \iota = Id| which allows us to quickly produce colimits in the subcategory via |\int^I D(I) \cong R\int^I \iota D(I)|. It’s easy to verify that |R\int^I \iota D(I)| has the appropriate universal property to be |\int^I D(I)|.

We’ll compute |R| by composing two adjunctions. First, we have |\bar{({-})} \dashv \iota({-}) \circ \sigma : \mathbf{Mod}_{\mathcal{T}^{\times}} \to [\mathcal T, \mathbf{Set}]|. This is essentially the universal property of |\mathcal{T}^{\times}|. When |\mathcal{T}| has finite products, which, of course, we’re assuming, then we can use the universal property of |\mathcal{T}^{\times}| to factor |Id_{\mathcal{T}}| into |Id = \bar{Id} \circ \sigma|. The second adjunction is then |\mathrm{Lan}_{\bar{Id}} \dashv {-} \circ \bar{Id} : \mathbf{Mod}_{\mathcal{T}} \to \mathbf{Mod}_{\mathcal{T}^{\times}}|. 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 |\iota({-} \circ \bar{Id}) \circ \sigma = \iota({-}) \circ \bar{Id} \circ \sigma = \iota({-})|. The composite of the right adjoint is \[ \begin{align} R(F) & = \mathrm{Lan}_{\bar{Id}}(\bar{F}) \\ & \cong \int^X \mathcal{T}(\bar{Id}(X), {-}) \times \bar{F}(X) \\ & \cong \int^X \mathcal{T}\left(\prod_{i=1}^{\lvert X\rvert} X_i, {-}\right) \times \prod_{i=1}^{\lvert X \rvert} F(X_i) \end{align} \] where we view the list |X : \mathcal{T}^{\times}| as a |\lvert X\rvert|-tuple with components |X_i|.

This construction of the reflector, |R|, is quite similar to the free construction. The main difference is that here we factor |Id| via |\mathcal{T}^{\times}| where there we factored |\mathsf{G} : \mathbf{1} \to \mathcal{T}| via |\mathbf{1}^{\times} = \mathcal{T}_{\mathbf{Set}}|.

Let’s now explicitly describe the coproducts via |R|. As a warm-up, we’ll consider the initial object, i.e. nullary coproducts. We consider |R(\Delta 0)|. Because |0 \times S = 0|, the only case in the coend that isn’t |0| is when |\lvert X \rvert = 0| so the underlying set of the coend reduces to |\mathcal{T}(\mathsf{G}^0, \mathsf{G}^1)|, 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, |R(\Delta 0)| matches |F(0)|, i.e. the free model on |0|.

Next, we consider two models |G| and |H|. First, we compute to the coproduct of |G| and |H| as (plain) functors which is just computed pointwise, i.e. |(G+H)(\mathsf{G}^n) = G(\mathsf{G}^n)+H(\mathsf{G}^n) \cong G(\mathsf{G^1})^n + H(\mathsf{G^1})^n|. Considering the case where |X_i = \mathsf{G}^1| for all |i| and where |\lvert X \rvert = n|, which subsumes all the other cases, we see we have a term with |n| free variables each labelled by either an element of |G| or an element of |H|. 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 |G| and |H|. However, for |R|, we quotient also by the action of the other operations. The lists of objects with |X_i \neq \mathsf{G}^1| come in here to support equating non-unary ops. For example, a pair of the binary term |\mathsf{m}| and the 2-tuple of elements |(g_1, g_2)| for |g_1, g_2 \in U(G)|, will be equated with the pair of the unary term |id| and the 1-tuple of elements |(g)| where |g = g_1 g_2| in |G|. Similarly for |H| 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 |U(G)| or |U(H)| 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 |F| and |R| 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 |\mathbf{Set}|. 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 |\mathbf{Set}|-valued functors is different from the copower for finite-product-preserving |\mathbf{Set}|-valued functors. For a category with (arbitrary) coproducts, the copower corresponds to the coproduct of a constant family. We get, |F(S) \cong \coprod_{S} \mathcal T(\mathsf{G}^1, {-})| as is immediately evident from |F| being a left adjoint and a set |S| being the coproduct of |1| |S|-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 |\mathcal{T}(\mathsf{G}^n, {-}) + \mathcal{T}(\mathsf{G}^m, {-})| 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.