category with duals (list of them)
dualizable object (what they have)
Throughout, we will use the notation and terminology of Ch. VII of CWM, with the exception that the product bifunctor of a monoidal category will be denoted by , instead of Mac Lane’s notation.
Let be some monoidal category. At first, we would like the coherence theorem for monoidal categories to state that every diagram in built up from instances of , , and identity arrows by multiplications (such as the pentagon diagram) commutes. This, however, is not possible, because some formally different vertices of such a diagram might turn out to be the same in our particular monoidal category , in a way that makes the diagram non-commutative.
As a concrete example of the problem in a particular monoidal category, consider Isbell’s famous example for showing that moving to skeleta does not assure that all monoidal categories are strict (see p. 164 of CWM). In this example, one shows that if is the denumerable set in a skeleton of , then, although equals , the associator (defined as usual to commute with the projections) cannot be the identity.
So, in order for coherence to work, we must change it to the statement that every ‘’formal’‘ diagram commutes.
The formal diagrams that commute will be described through certain graphs (). The vertices of will be binary words of length , and its arrows will represent the sort of arrows that participate in the coherence theorem.
We begin by defining the set of binary words inductively, as the set of all terms in one variable (denoted by ‘’’’) in the signature , where is an 0-ary function symbol (a constant), and is a binary function symbol. So, is the smallest set of strings in the alphabet satisfying , , and if then (usually written as or even for convenience) is also in .
Next, we define a set of certain arrow symbols as follows (the reason for the tag in will be clear later). Let be the smallest set of strings in the alphabet satisfying for all , for all , and for all , if then also (more precisely, the last terms should be called, and , but as before, we will usually use the more convenient infix notation). Note that elements of are comprised of a single associator/unitor symbol (or their inverses) tensored with one or more strings of the form . Later, when we will interpret the elements of as arrows of a particular monoidal category , we will call them basic arrows. The idea is that every arrow of the ‘’right’‘ kind in (the kind considered in the coherence theorem) factors as the composition of such basic arrows (because is a bifunctor).
It can be verified that every string of is of one and only one of the following forms: for some , for some , for some , …, for some and . Also, in each case the ‘’arguments’‘ are determined uniquely (for example, both and are determined from ), and so we may define functions on inductively.
Let be the directed graph (quiver in Lab jargon) with as the set of objects, as the set of arrows, and with the obviously defined and (for example, For , , , etc.
Define inductively the length of a binary word as follows:
Since for all , (this can be verified by induction), is the union of disjoint graphs , where for , the vertices of are the binary words of length , and the edges are all with .
Now, let us fix some monoidal category , and some object . We can interpret vertices and edges of in by defining inductively functions , as follows:
(for and ).
It is straightforward to verify that the pair is a morphism of graphs (where is the underlying graph of ), that is, that for all , we have
Therefore, if form a path in (i.e., for all ), then (in that order) are composable arrows in . We can finally state the coherence theorem:
(Mac Lane’s Coherence Theorem, version 1). Let be two binary words of the same length . Suppose that and form two paths from to in . Then the two corresponding sequences of arrows in have the same composition in :
Note that at a first glance, this ‘’single variable coherence’‘ looks quite limited: We only prove commutativity of diagrams in whose vertices are obtained by tensoring a single element (e.g., vertices such as ). However, it turns out that the general case follows almost immediately from this case. The trick is to construct an appropriate monoidal category in a way that the coherence in one variable for and one special object of is the general coherence for .
The coherence theorem in CWM (Theorem VII.2.1) is stated in a different way, but the main bulk of its proof is actually devoted to prove the above coherence theorem. To state also the version of Theorem VII.2.1 of CWM, let be the category whose objects are binary words, with a single arrow between any two binary words of the same length and with the obvious composition. The monoidal structure on is the obvious one: The unit is , and the components of the associator and the unitors are each the appropriate single arrow of the relevant hom-set. The coherence theorem in CWM is as follows:
(Mac Lane’s Coherence Theorem, version 2). For any monoidal category and any object of , there is a unique strict morphism of monoidal categories with .
Version 2 says that is the free monoidal category on one generator (that is, that it is the object part of a universal arrow from to the forgetful (object) functor , where stands for monoidal categories with strict morphisms of monoidal categories) . As we shall see later, this version follows almost immediately from version 1. While this is not clear at a first glance, it is also true that version 1 follows from version 2. For this, we will define a monoidal category that will be almost evidently free (and hence, given version 2, isomorphic to ).
It will be simpler to first prove coherence only for the associator, forgetting about the unit and the unitors. Let be the full subgraph of whose vertex set consists only of those binary words that do not involve . We will write for the subset of consisting of such binary words (that is, for the vertex set of ).
Let be the subset of consisting of the strings that
involve only instances of and (but not , , , and ) and also do not involve (e.g., as in ). Actually, could be defined inductively, similarly to , omitting the reference to , , , and , and using instead of . Note that is the set of arrows of : . For simplicity, we will use the same names for the restriction of to .
Let be the full subgraph of on the vertices of length . The proof will use a certain vertex of as a’‘pivot.’‘ Specifically, we let be the unique word of length in which all pairs of parentheses start in front (e.g., for , for , and for ; a precise inductive definition is , for ).
The proof will also use a measure of how ‘’far’‘ is a word from being . So, we define inductively by
It is easily verified that for all , with equality iff . In fact, is the length of the longest directed path (see ahead for what ‘’directed’‘ means here) from to . [Intuitively, the idea is that if , then we may first handle , then handle , in order to reach (with and ) but not yet to . Then, by additional applications of associators, we finally reach .]
We will call any that involves a directed arrow, and any that involves an anti-directed arrow. A more precise inductive definition is this: For all , is directed, and if is directed, then and are directed for all . The definition of anti-directed is obtained by replacing by and ‘’directed’‘ by ’‘anti-directed’‘ in the previous definition. It can be shown by induction that if is directed, then is strictly smaller that .
For future reference, define the ‘’formal inverse’‘ of in the obvious inductive way, by setting, for example, , , etc. It can be verified that the formal inverse has all expected properties (such as being idempotent, switching domain and codomain, taking an anti-directed arrow to a directed one, and being interpreted as the inverse of the interpretation of the original arrow).
From each of length , there is a ‘’canonical’‘ path, involving only directed arrows, from to in , obtained by successively moving the outermost parentheses to the left with the appropriate . For an example, consider the paths and in the pentagon (5) on p. 162 of CWM. Note that if are both of length , then there is a path in from to : Take the canonical path from to , and then extend it by reversing (using ) every edge of the canonical path from to .
Given of the same length , our task is to show that for any path from to in , applying to the arrows of the path and composing in results in the same arrow in , independently of the choice of path. In other words, we would like to prove the theorem obtained from replacing by and by in the first version of the coherence theorem.
As a preparation, we start with the following degenerate case, that can be proved (as usual) by induction on and .
There are no parallel directed arrows in : If are directed arrows with and , then .
Now, take some path from to , as in
In , we have the corresponding path (note that both in and in , it is possible that some of the vertices are in fact equal)
In our original path, it is possible that some arrows (some ‘s) are anti-directed. We can replace each anti-directed arrow by its formal inverse so that we are left only with directed arrows. For example, if and are the only anti-directed arrows in our path, then after formally inverting them we get the following series of arrows in :
In , we get
Let us write for the canonical path from with and with to . Let us also write for the arrow of obtained by composing of all arrows of . Suppose that all squares in the following diagram of commute:
(where we write for ). This would imply that all squares in
commute, which also implies that the outer rectangle commutes, that is:
The right-hand side depends only on and (and not on the particular choice of the path ), which is exactly what we would like to prove. Hence, it is sufficient to show that all squares in the last but one diagram commute. For this, it is clearly sufficient to prove the following proposition:
Let be a word of length , different from . Then applying to any two directed paths (paths consisting only of directed arrows) from to results in two paths in that have the same composition in .
The proof is by induction on . For the basis, if then and the assertion is trivial. Suppose, therefore, that > and the assertion is true for all with <. For reasons that will be understood later, we will prove this part by one additional induction: on the length .
Hence, we have to prove that if the assertion holds for all of rank smaller than and for all of rank and length smaller than (for > – the basis for is trivial as then ), then it holds also for all of rank
and length .
From > we know that , and hence there exist such that . Consider two paths from to . Let be the first edge of the first path, and let be the first edge of the second path (so that in particular ). Write and , so that in we have
Since < and <, by hypothesis any two paths from to have the same composition in , and similarly for . In particular, if , then we are done:
So, we will continue by assuming that . Note that in this case , because it can verified by induction that there are no parallel arrows in . In this case, it will be sufficient to find some of length and directed paths (recall that here a directed path is a path consisting only of directed arrows) in from to and from to such that applying to the following diamond (upper part of the diagram) results in a commutative diamond in :
(the outer paths are our two paths from to ). This is indeed enough, because by hypothesis, the two lower trapezoids are commutative in .
The existence of and of directed paths from and to such that the above diamond is commutative in will be proved by considering all possible cases for and . For , we have three possibilities:
and therefore and (by standard ‘’unique decomposition’‘ of terms in a first-order language). Also, .
for some and some directed . As above, we get in this case that and . Also, .
for some , in which case
so that and . Also, .
In summary, we have the following 3 cases for :
Case : for some directed with . Also, .
Case : for some directed with . Also, .
Case : for some , and also and .
Similarly, we have Case , Case and Case for . We will now consider each one of the possible cases for and :
and : The situation is as follows:
Since < (as cannot be ) and since
it follows from the induction hypothesis that any two directed paths from to have the same composition in . In particular, applying to the following diamond in results in a commutative diamond in :
Since is a bifunctor, it follows that the following diagram is again commutative when interpreted in :
(where for with , we write for the directed path in obtained by -ing each arrow of from the right with ). This completes the proof for the current case.
and : Proved similarly to the previous case.
and (or and ): We have the following diamond:
which commutes in , because is a bifunctor.
or : W.l.o.g., we will assume . Note that in this case, it is not possible that also holds, that is, that for some with , for then , which implies that and , so that , contradicting our assumption. So, we have to consider only and . For , we have and , and we get the following diamond:
which commutes in by the naturality of .
For ( and ), we have to consider the three possible cases for .
If for some and some directed , then by comparing domains we get , which implies that and , that is, with . Hence we get the diamond
which commutes in , because is natural.
The case where for some and some directed can be treated similarly.
Finally, if , then by comparing domains we get , and therefore and . Hence, and . In this case, the two first edges , in our two paths from to look like part of the coherent pentagon (Eq. (5) on p. 162 of CWM):
All edges in the above pentagon are directed, and the diagram is obviously commutative in (as is monoidal). This completes the proof of the proposition.
Note: By Kelly’s 1964 paper, we know that the pentagon identity and one triangle identity are all that is required (that the two other triangle identities follow from the above is shown both in CWM an in Kelly, while the fact that follows from the pentagon and the triangle identities is proved in Kelly). From this point on, we will be using freely all identities from pp. 162-163 of CWM.
Still need to fill this. The following are the highlights.
First, show that any directed path in path in may be replaced by a path with the same starting and ending vertices in which all associators (if any) are at the end, and with the same composition in as the original path. The main ingredient in the following proposition:
be two directed arrows of with an associator appearing in and a unitor appearing in (note: the definition of ‘’directed’‘ is extended in an obvious way to include unitors). Then either there exists a directed arrow containing a unitor with , or there exist directed , as in
with containing a unitor, containing an associator, and .
This proposition may be proved by a long and tedious induction on and .
For this I needed the triangle identities and the naturality of (as mentioned in CWM), but also the naturality of and , as well as the bifunctoriality of . For example, consider:
(where some associator appears in ). So – what am I missing here?
Recall that our original goal is to show that any two paths in with the same starting vertex and the same ending vertex have the same composition in . There is still a path from any vertex of to (first remove all units, then proceed as in the case of ), and we can use exactly the same method used above (when only the associator was considered) to reduce the problem to: Any two directed paths of starting at some vertex and ending at have the same composition in . From what we have seen above, any two arbitrary such paths may be replaced be two paths starting with unitors and ending with associators, as in
Here, is the word obtained by removing all instances of the unit from (this can be defined rigorously by induction), and is the total number of units appearing in . The right part of the last diagram, where there are no units and unitors, commutes in by the ‘’coherence for the associator’‘ that was already proved. Hence, it remains to prove that the left part, where all arrows involve unitors, commutes in (’‘coherence for the unitors’’).
First one must prove that two parallel directed arrows with unitors in have the same interpretation in .
Recall that in (no units and no unitors), there are no parallel directed arrows. However, this is not the case in (for example, consider ). Hence, we must settle for equality of the interpretations in .
For this, I used induction on the total number of in both and , using and the naturality of and . Am I missing something here? Is there an obvious one-line argument that I’m failing to see?
Now, we can finally prove coherence for the unitors, by induction on the number of units in . Considering the left part of the last diagram, if , as in
then the parallel arrows are equal in , while the ‘’large diamond’‘ on the right commutes in by the induction hypothesis.
We can therefore assume that . As in the case of coherence for the associator, it is sufficient to
find a commutative diamond, that is, to find some vertex of and directed arrows and in containing unitors, as in
such that the diamond on the left commutes in :
If we find such , and , then since by the induction hypothesis the upper and lower parallelograms on the right commute in , we are done.
Finally, the required commutative diamond may be found by induction on .
I intend to come back and fill this. The most difficult part was already proved above.
The category has one-element hom-sets by construction, but it was not at all obvious that it is indeed the free monoidal category on one generator. Alternatively, it is possible to construct a category that will be almost obviously a free monoidal category on one generator. This would mean that is isomorphic to , and in particular has one-element hom-sets. The fact that is free and has one-element hom-sets may then serve as yet a third version of coherence.
This should still be filled.
This should still be filled.
Saunders Mac Lane, Categories for the Working Mathematician, 2nd edition, Springer GTM, 1998.
Max Kelly On MacLane’s conditions for coherence of natural associators, commutativities, etc., Journal of Algebra, 1, pp. 397–402, 1964.
I. Beylin and P. Dybjer, Extracting a proof of coherence for monoidal categories from a formal proof of normalization of monoids, available online
J. Armstrong, Mac Lane’s coherence theorem