nLab
Mac Lane's proof of the coherence theorem for monoidal categories

Context

Monoidal categories

Category theory

Contents

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 \otimes, instead of Mac Lane’s \square notation.

Introduction and statement

Let B, B,α (B),e B,λ (B),ϱ (B),\langle B, \otimes_B, \alpha^{(B)}, e_B, \lambda^{(B)}, \varrho^{(B)}, \rangle be some monoidal category. At first, we would like the coherence theorem for monoidal categories to state that every diagram in BB built up from instances of α\alpha, λ (B)\lambda^{(B)}, ϱ (B)\varrho^{(B)} and identity arrows by multiplications B\otimes_B (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 BB, 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 DD is the denumerable set in a skeleton Set 0\mathbf{Set}_0 of Set\mathbf{Set}, then, although D×(D×D)D\times(D\times D) equals (D×D)×D(D\times D)\times D, the associator α D,D,D\alpha_{D,D,D} (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 𝒢 n\mathcal{G}'_n (nn\in \mathbb{N}). The vertices of 𝒢 n\mathcal{G}'_n will be binary words of length nn, and its arrows will represent the sort of arrows that participate in the coherence theorem.

We begin by defining the set WW of binary words inductively, as the set of all terms in one variable (denoted by -”) in the signature {e 0,}\{e_0, \otimes\}, where e 0e_0 is an 0-ary function symbol (a constant), and \otimes is a binary function symbol. So, WW is the smallest set of strings in the alphabet {e 0,,}\{e_0,\otimes,-\} satisfying W-\in W, e 0We_0\in W, and if u,vWu,v\in W then uv\otimes u v (usually written as (u)(v)(u) \otimes (v) or even uvu\otimes v for convenience) is also in WW.

Next, we define a set SS' of certain arrow symbols as follows (the reason for the tag in SS' will be clear later). Let SS' be the smallest set of strings in the alphabet W{1,α,α 1,λ,λ 1,ϱ,ϱ 1,^}W\cup\{1,\alpha,\alpha^{-1},\lambda,\lambda^{-1},\varrho,\varrho^{-1},\displaystyle{\hat{\otimes}\}} satisfying αuvw,α 1uvwS\alpha u v w, \alpha^{-1} u v w\in S' for all u,v,wWu,v,w\in W, λw,λ 1w,ϱw,ϱ 1wS\lambda w, \lambda^{-1} w, \varrho w, \varrho^{-1} w \in S' for all wWw\in W, and for all wWw\in W, if βS\beta\in S' then also (β)^(1w),(1w)^(β)S(\beta)\hat{\otimes} (1w), (1w)\hat{\otimes} (\beta)\in S' (more precisely, the last terms should be called, ^β1w\hat{\otimes} \beta 1 w and ^1wβ\hat{\otimes} 1 w \beta, but as before, we will usually use the more convenient infix notation). Note that elements of SS' are comprised of a single associator/unitor symbol (or their inverses) tensored with one or more strings of the form 1w1w. Later, when we will interpret the elements of SS' as arrows of a particular monoidal category BB, we will call them basic arrows. The idea is that every arrow of the ”right” kind in BB (the kind considered in the coherence theorem) factors as the composition of such basic arrows (because \otimes is a bifunctor).

It can be verified that every string of SS' is of one and only one of the following forms: αuvw\alpha u v w for some u,v,wWu, v, w\in W, α 1uvw\alpha^{-1} u v w for some u,v,wWu, v, w\in W, λw\lambda w for some wWw\in W, …, β^1w\beta \hat{\otimes} 1w for some wWw\in W and βS\beta \in S'. Also, in each case the ”arguments” are determined uniquely (for example, both β\beta and ww are determined from β^1w\beta \hat{\otimes} 1w), and so we may define functions on SS' inductively.

Let 𝒢\mathcal{G}' be the directed graph (quiver in nnLab jargon) with WW as the set of objects, SS' as the set of arrows, and with the obviously defined domdom and codcod (for example, For u,v,wWu,v,w \in W, dom(αuvw):=u(vw)=:cod(α 1uvw)dom(\alpha u v w) := u\otimes (v\otimes w) =:cod(\alpha^{-1} u v w), dom(β^1w):=dom(β)wdom(\beta \hat{\otimes} 1w) := dom(\beta)\otimes w, etc.

Define inductively the length len(w)len(w) of a binary word ww as follows:

len(e 0):=0,len():=1,len(uv):=len(u)+len(v). len(e_0):=0,\quad len(-):=1,\quad len(u\otimes v):= len(u) + len(v).

Since for all sSs\in S', len(dom(s))=len(cod(s))len(dom(s))=len(cod(s)) (this can be verified by induction), 𝒢\mathcal{G}' is the union of disjoint graphs 𝒢 n\mathcal{G}'_n, where for nn\in \mathbb{N}, the vertices of 𝒢 n\mathcal{G}'_n are the binary words of length nn, and the edges are all sSs\in S' with len(dom(s))=nlen(dom(s)) = n.

Now, let us fix some monoidal category B, B,α (B),e B,λ (B),ϱ (B),\langle B, \otimes_B, \alpha^{(B)}, e_B, \lambda^{(B)}, \varrho^{(B)}, \rangle, and some object bobj(B)b\in obj(B). We can interpret vertices and edges of 𝒢\mathcal{G}' in BB by defining inductively functions () b:Wobj(B)(\cdot)_b: W\to obj(B), :Sarr(B)\mathcal{I}:S'\to arr(B) as follows:

(e 0) b:=e B, () b:=b,(uv) b:=u b Bv b, (e_0)_b:=e_B,\text{ } (-)_b:=b, (u\otimes v)_b:= u_b\otimes_B v_b,
(αuvw):=α u b,v b,w b (B),(α 1uvw):=(α u b,v b,w b (B)) 1, (λu):=λ u b (B),(λ 1u):=(λ u b (B)) 1, (ϱu):=ϱ u b (B),(ϱ 1u):=(ϱ u b (B)) 1, (β^1w):=(β) B1 w b,(1w^β):=1 w b B(β) \begin{aligned} &&\mathcal{I}(\alpha u v w) := \alpha^{(B)}_{u_b,v_b,w_b},\quad \mathcal{I}(\alpha^{-1} u v w):= (\alpha^{(B)}_{u_b,v_b,w_b})^{-1},\\ && \mathcal{I}(\lambda u) := \lambda^{(B)}_{u_b}, \quad \mathcal{I}(\lambda^{-1} u) := (\lambda^{(B)}_{u_b})^{-1},\\ && \mathcal{I}(\varrho u) := \varrho^{(B)}_{u_b}, \quad \mathcal{I}(\varrho^{-1} u) := (\varrho^{(B)}_{u_b})^{-1},\\ && \mathcal{I}(\beta\hat{\otimes} 1w) := \mathcal{I}(\beta)\otimes_B 1_{w_b},\quad \mathcal{I}(1w\hat{\otimes} \beta) := 1_{w_b}\otimes_B\mathcal{I}(\beta) \end{aligned}

(for u,v,wWu,v,w\in W and βS\beta\in S').

It is straightforward to verify that the pair () b,\langle (\cdot)_b,\mathcal{I}\rangle is a morphism of graphs 𝒢UB\mathcal{G}'\to U B (where UBUB is the underlying graph of BB), that is, that for all sSs\in S', we have

(dom(s)) b=dom B((s)),(cod(s)) b=cod B((s)). (dom(s))_b = dom_B(\mathcal{I}(s)),\quad (cod(s))_b = cod_B(\mathcal{I}(s)).

Therefore, if s 1,,s ms_1,\ldots,s_m form a path in 𝒢\mathcal{G}' (i.e., dom(s i+1)=cod(s i)dom(s_{i+1})=cod(s_i) for all ii), then (s 1),,(s m)\mathcal{I}(s_1),\ldots,\mathcal{I}(s_m) (in that order) are composable arrows in BB. We can finally state the coherence theorem:

Theorem

(Mac Lane’s Coherence Theorem, version 1). Let v,wWv,w\in W be two binary words of the same length nn. Suppose that s 1,,s ms_1,\ldots,s_m and s 1,s ms'_1,\ldots s'_{m'} form two paths from vv to ww in 𝒢 n\mathcal{G}'_n. Then the two corresponding sequences of arrows in BB have the same composition in BB:

(s m)(s 1)=(s m)(s 1) \mathcal{I}(s_m)\circ \cdots\circ \mathcal{I}(s_1) = \mathcal{I}(s'_{m'})\circ \cdots\circ \mathcal{I}(s'_1)

Note that at a first glance, this ”single variable coherence” looks quite limited: We only prove commutativity of diagrams in BB whose vertices are obtained by tensoring a single element bb (e.g., vertices such as b B((b Bb) Bb)b\otimes_B ((b\otimes_B b)\otimes_B b)). However, it turns out that the general case follows almost immediately from this case. The trick is to construct an appropriate monoidal category It(B)It(B) in a way that the coherence in one variable for It(B)It(B) and one special object of It(B)It(B) is the general coherence for BB.

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 𝒲\mathcal{W} be the category whose objects are binary words, with a single arrow uvu\to v between any two binary words of the same length and with the obvious composition. The monoidal structure on 𝒲\mathcal{W} is the obvious one: The unit is e 0e_0, 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:

Theorem

(Mac Lane’s Coherence Theorem, version 2). For any monoidal category BB and any object bb of BB, there is a unique strict morphism of monoidal categories 𝒲B\mathcal{W}\to B with ()b (-)\mapsto b.

Version 2 says that 𝒲\mathcal{W} 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 Moncat sSet\mathbf{Moncat}_s \to \mathbf{Set}, where Moncat s\mathbf{Moncat}_s 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 F[1]F[1] that will be almost evidently free (and hence, given version 2, isomorphic to 𝒲\mathcal{W}).

Coherence only for the associator

It will be simpler to first prove coherence only for the associator, forgetting about the unit and the unitors. Let 𝒢\mathcal{G} be the full subgraph of 𝒢\mathcal{G}' whose vertex set consists only of those binary words that do not involve e 0e_0. We will write W 0W_0 for the subset of WW consisting of such binary words (that is, for the vertex set of 𝒢\mathcal{G}).

Let SS be the subset of SS' consisting of the strings that
involve only instances of α\alpha and α 1\alpha^{-1} (but not λ\lambda, λ 1\lambda^{-1}, ϱ\varrho, and ϱ 1\varrho^{-1}) and also do not involve e 0e_0 (e.g., as in αe 0vw\alpha e_0 v w). Actually, SS could be defined inductively, similarly to SS', omitting the reference to λ\lambda, λ 1\lambda^{-1}, ϱ\varrho, and ϱ 1\varrho^{-1}, and using W 0W_0 instead of WW. Note that SS is the set of arrows of 𝒢\mathcal{G}: S={sSdom(s),cod(s)W 0}S=\{s\in S'|dom(s),cod(s)\in W_0\}. For simplicity, we will use the same names dom,coddom,cod for the restriction of dom,coddom, cod to SS.

Let 𝒢 n\mathcal{G}_n be the full subgraph of 𝒢\mathcal{G} on the vertices of length nn. The proof will use a certain vertex w (n)w^{(n)} of 𝒢 n\mathcal{G}_n as a”pivot.” Specifically, we let w (n)W 0w^{(n)}\in W_0 be the unique word of length nn in which all pairs of parentheses start in front (e.g., ()(-\otimes -)\otimes - for n=3n=3, (())((-\otimes -)\otimes -)\otimes - for n=4n=4, and ((()))(((-\otimes-)\otimes - )\otimes -)\otimes - for n=5n=5; a precise inductive definition is w (1)=w^{(1)}=-, w (n)=w (n1)w^{(n)}= w^{(n-1)}\otimes - for n1n\geq 1).

The proof will also use a measure ρ\rho of how ”far” is a word wW 0w\in W_0 from being w (n)w^{(n)}. So, we define ρ\rho inductively by

ρ()=0,ρ(vw)=ρ(v)+ρ(w)+len(w)1. \rho(-) = 0, \quad \rho(v\otimes w) = \rho(v)+\rho(w)+len(w)-1.

It is easily verified that ρ(u)0\rho(u)\geq 0 for all uW 0u\in W_0, with equality iff u=w (n)u = w^{(n)}. In fact, ρ(u)\rho(u) is the length of the longest directed path (see ahead for what ”directed” means here) from uu to w (n)w^{(n)}. [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 sSs\in S that involves α\alpha a directed arrow, and any sSs\in S that involves α 1\alpha^{-1} an anti-directed arrow. A more precise inductive definition is this: For all u,v,wW 0u,v,w\in W_0, αuvw\alpha u v w is directed, and if β\beta is directed, then β^1w\beta\hat{\otimes} 1 w and 1w^β1 w\hat{\otimes} \beta are directed for all wW 0w\in W_0. The definition of anti-directed is obtained by replacing α\alpha by α 1\alpha^{-1} and ”directed” by ”anti-directed” in the previous definition. It can be shown by induction that if sSs\in S is directed, then ρ(cod(s))\rho(cod(s)) is strictly smaller that ρ(dom(s))\rho(dom(s)).

For future reference, define the ”formal inverse” of sSs'\in S' in the obvious inductive way, by setting, for example, inv(αuvw):=α u,v,w 1inv(\alpha uvw): = \alpha^{-1}_{u,v,w}, inv(α 1uvw):=αuvwinv(\alpha^{-1} uvw):= \alpha uvw inv(β^1w):=inv(β)^1winv(\beta\hat{\otimes} 1w):= inv(\beta) \hat{\otimes} 1w, 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 wW 0w\in W_0 of length nn, there is a ”canonical” path, involving only directed arrows, from ww to w (n)w^{(n)} in 𝒢 n\mathcal{G}_n, obtained by successively moving the outermost parentheses to the left with the appropriate α\alpha. For an example, consider the paths \to\to and \to\uparrow in the pentagon (5) on p. 162 of CWM. Note that if v,wW 0v,w\in W_0 are both of length nn, then there is a path in 𝒢 n\mathcal{G}_n from vv to ww: Take the canonical path from vv to w (n)w^{(n)}, and then extend it by reversing (using invinv) every edge of the canonical path from ww to w (n)w^{(n)}.

Given v,wW 0v,w\in W_0 of the same length nn, our task is to show that for any path from vv to ww in 𝒢 n\mathcal{G}_n, applying \mathcal{I} to the arrows of the path and composing in BB results in the same arrow v bw bv_b\to w_b in BB, independently of the choice of path. In other words, we would like to prove the theorem obtained from replacing WW by W 0W_0 and 𝒢 n\mathcal{G}'_n by 𝒢 n\mathcal{G}_n 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 ss and ss'.

Proposition

There are no parallel directed arrows in 𝒢 n\mathcal{G}_n: If s,sSs,s'\in S are directed arrows with dom(s)=dom(s)dom(s) = dom(s') and cod(s)=cod(s)cod(s) = cod(s'), then s=ss=s'.

Now, take some path s 1,,s ms_1,\ldots,s_m from vv to ww, as in

Coh_fig_1

In BB, we have the corresponding path (note that both in 𝒢 n\mathcal{G}_n and in BB, it is possible that some of the vertices are in fact equal)

Coh_fig_2

In our original path, it is possible that some arrows (some s is_i’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 s 2s_2 and s 3s_3 are the only anti-directed arrows in our path, then after formally inverting them we get the following series of arrows in 𝒢 n\mathcal{G}_n:

Coh_fig_3

In BB, we get

Coh_fig_4

Let us write can(u)can(u) for the canonical path from uW 0u\in W_0 with len(u)=nlen(u)=n and with uw (n)u \neq w^{(n)} to w (n)w^{(n)}. Let us also write (can(u))\mathcal{I}(can(u)) for the arrow of BB obtained by composing \mathcal{I} of all arrows of can(u)can(u). Suppose that all squares in the following diagram of BB commute:

Coh_fig_5

(where we write w b (n)w_b^{(n)} for [w (n)] b[w^{(n)}]_b). This would imply that all squares in

Coh_fig_6

commute, which also implies that the outer rectangle commutes, that is:

(s m)(s 1)=(can(w)) 1(can(v)). \mathcal{I}(s_m)\circ \cdots \circ\mathcal{I}(s_1) = \mathcal{I}(can(w))^{-1}\circ \mathcal{I}(can(v)).

The right-hand side depends only on ww and vv (and not on the particular choice of the path s 1,s ms_1,\ldots s_m), 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:

Proposition

Let vW 0v\in W_0 be a word of length nn, different from w (n)w^{(n)}. Then applying \mathcal{I} to any two directed paths (paths consisting only of directed arrows) from vv to w (n)w^{(n)} results in two paths in BB that have the same composition in BB.

The proof is by induction on ρ(v)\rho(v). For the basis, if ρ(v)=0\rho(v)=0 then v=w (n)v = w^{(n)} and the assertion is trivial. Suppose, therefore, that ρ(v)\rho(v)>00 and the assertion is true for all vW 0v'\in W_0 with ρ(v)\rho(v')<ρ(v)\rho(v). For reasons that will be understood later, we will prove this part by one additional induction: on the length len(v)len(v).

Hence, we have to prove that if the assertion holds for all vv' of rank smaller than r:=ρ(v)r := \rho(v) and for all vv' of rank rr and length smaller than nn (for nn>11 – the basis for n=1n=1 is trivial as then v=()=w (1)v' = (-) = w^{(1)}), then it holds also for all vv' of rank rr
and length nn.

From ρ(v)\rho(v)>00 we know that vv\neq - , and hence there exist u,wW 0u,w\in W_0 such that v=uwv = u\otimes w. Consider two paths from vv to w (n)w^{(n)}. Let βS\beta\in S be the first edge of the first path, and let γS\gamma\in S be the first edge of the second path (so that in particular dom(β)=v=dom(γ)dom(\beta) = v = dom(\gamma)). Write v:=cod(β)v':=cod(\beta) and v:=cod(γ)v'':=cod(\gamma), so that in 𝒢 n\mathcal{G}_n we have

Coh_fig_7

Since ρ(v)\rho(v')<ρ(v)\rho(v) and ρ(v)\rho(v'')<ρ(v)\rho(v), by hypothesis any two paths from vv' to w (n)w^{(n)} have the same composition in BB, and similarly for vv''. In particular, if β=γ\beta = \gamma, then we are done:

Coh_fig_8

So, we will continue by assuming that βγ\beta\neq \gamma. Note that in this case vvv'\neq v'', because it can verified by induction that there are no parallel arrows in 𝒢 n\mathcal{G}_n. In this case, it will be sufficient to find some zW 0z\in W_0 of length nn and directed paths (recall that here a directed path is a path consisting only of directed arrows) in 𝒢 n\mathcal{G}_n from vv' to zz and from vv'' to zz such that applying \mathcal{I} to the following diamond (upper part of the diagram) results in a commutative diamond in BB:

Coh_fig_9

(the outer paths are our two paths from vv to w (n)w^{(n)}). This is indeed enough, because by hypothesis, the two lower trapezoids are commutative in BB.

The existence of zW 0z\in W_0 and of directed paths from vv' and vv'' to zz such that the above diamond is commutative in BB will be proved by considering all possible cases for β\beta and γ\gamma. For β\beta, we have three possibilities:

  • β=β^1w˜\beta = \beta'\hat{\otimes} 1\tilde{w} for some w˜W 0\tilde{w}\in W_0 and some directed βS\beta'\in S. In this case
v=uw=dom(β)=dom(β)w˜ v = u\otimes w = dom(\beta) = dom(\beta')\otimes \tilde{w}

and therefore dom(β)=udom(\beta') = u and w˜=w\tilde{w}=w (by standard ”unique decomposition” of terms in a first-order language). Also, v=cod(β)=cod(β)wv' = cod(\beta) = cod(\beta')\otimes w .

  • β=1u˜^β\beta = 1\tilde{u}\hat{\otimes}\beta'' for some u˜W 0\tilde{u}\in W_0 and some directed βS\beta''\in S. As above, we get in this case that dom(β)=wdom(\beta'') =w and u˜=u\tilde{u} = u. Also, v=cod(β)=ucod(β)v' = cod(\beta) = u\otimes cod(\beta'').

  • β=αu˜st\beta = \alpha \tilde{u} s t for some u˜,s,tW 0\tilde{u},s,t\in W_0, in which case

v=uw=dom(β)=u˜(st), v = u\otimes w = dom(\beta) = \tilde{u}\otimes (s\otimes t),

so that u˜=u\tilde{u} = u and w=stw = s\otimes t. Also, v=cod(β)=(us)tv' = cod(\beta) = (u\otimes s)\otimes t.

In summary, we have the following 3 cases for β\beta:

  • Case 1 β1_{\beta}: β=β^1w\beta = \beta'\hat{\otimes} 1w for some directed βS\beta'\in S with dom(β)=udom(\beta')=u. Also, v=cod(β)wv' = cod(\beta')\otimes w.

  • Case 2 β2_{\beta}: β=1u^β\beta = 1u \hat{\otimes} \beta'' for some directed βS\beta''\in S with dom(β)=wdom(\beta'') = w. Also, v=ucod(β)v' = u\otimes cod(\beta'').

  • Case 3 β3_{\beta}: β=αust\beta = \alpha u s t for some s,tW 0s,t\in W_0, and also w=stw = s\otimes t and v=(us)tv' = (u\otimes s)\otimes t.

Similarly, we have Case 1 γ1_{\gamma}, Case 2 γ2_{\gamma} and Case 3 γ3_{\gamma} for γ\gamma. We will now consider each one of the possible cases for β\beta and γ\gamma:

1 β1_{\beta} and 1 γ1_{\gamma}: The situation is as follows:

Coh_fig_10

Since len(u)len(u)<len(v)len(v) (as wW 0w\in W_0 cannot be e 0e_0) and since

ρ(u)=ρ(v)(ρ(w) 0+len(w)1 0)ρ(v), \rho(u) = \rho(v) - (\underbrace{\rho(w)}_{\geq 0} + \underbrace{len(w) - 1}_{\geq 0}) \leq \rho(v),

it follows from the induction hypothesis that any two directed paths from uu to w (len(u))w^{(len(u))} have the same composition in BB. In particular, applying \mathcal{I} to the following diamond in 𝒢 len(u)\mathcal{G}_{len(u)} results in a commutative diamond in BB:

Coh_fig_11

Since B\otimes_B is a bifunctor, it follows that the following diagram is again commutative when interpreted in BB:

Coh_fig_12

(where for xW 0x\in W_0 with len(x)=len(u)len(x) = len(u), we write can(x)^1wcan(x)\hat{\otimes} 1 w for the directed path in 𝒢 n\mathcal{G}_n obtained by ^\hat{\otimes}-ing each arrow of can(x)can(x) from the right with 1w1 w). This completes the proof for the current case.

2 β2_{\beta} and 2 γ2_{\gamma}: Proved similarly to the previous case.

1 β1_{\beta} and 2 γ2_{\gamma} (or 2 β2_{\beta} and 1 γ1_{\gamma}): We have the following diamond:

Coh_fig_13

which commutes in BB, because B\otimes_B is a bifunctor.

3 β3_{\beta} or 3 γ3_{\gamma}: W.l.o.g., we will assume 3 β3_{\beta}. Note that in this case, it is not possible that also 3 γ3_{\gamma} holds, that is, that γ=αust\gamma = \alpha u s' t' for some s,ts',t' with w=stw = s'\otimes t', for then st=sts'\otimes t' = s \otimes t, which implies that s=ss' = s and t=tt' = t, so that γ=β\gamma = \beta, contradicting our assumption. So, we have to consider only 1 γ1_{\gamma} and 2 γ2_{\gamma}. For 1 γ1_{\gamma}, we have γ=γ^1st w\gamma = \gamma'\hat{\otimes} 1 \underbrace{s\otimes t}_{w} and dom(γ)=udom(\gamma') = u, and we get the following diamond:

Coh_fig_15

which commutes in BB by the naturality of α (B)\alpha^{(B)}.

For 2 γ2_{\gamma} (γ=1u^γ\gamma =1 u\hat{\otimes} \gamma'' and dom(γ)=w=stdom(\gamma'') = w = s\otimes t), we have to consider the three possible cases for γ\gamma''.

If γ=1s˜^δ\gamma'' = 1\tilde{s}\hat{\otimes} \delta for some s˜W 0\tilde{s}\in W_0 and some directed δS\delta\in S, then by comparing domains we get st=dom(γ)=s˜dom(δ)s\otimes t = dom(\gamma'') = \tilde{s}\otimes dom(\delta), which implies that s˜=s\tilde{s} =s and dom(δ)=tdom(\delta) = t, that is, γ=1s^δ\gamma'' = 1 s \hat{\otimes} \delta with dom(δ)=tdom(\delta) = t. Hence we get the diamond

Coh_fig_15

which commutes in BB, because α (B)\alpha^{(B)} is natural.

The case where γ=δ^1t˜\gamma'' = \delta\hat{\otimes} 1\tilde{t} for some t˜W 0\tilde{t}\in W_0 and some directed δS\delta\in S can be treated similarly.

Finally, if γ=αrpq\gamma'' = \alpha r p q, then by comparing domains we get st=dom(γ)=r(pq)s\otimes t = dom(\gamma'') = r\otimes(p\otimes q), and therefore r=sr = s and t=pqt = p\otimes q. Hence, γ=αspq\gamma'' = \alpha s p q and t=pqt = p\otimes q. In this case, the two first edges β\beta, γ\gamma in our two paths from vv to w (n)w^{(n)} look like part of the coherent pentagon (Eq. (5) on p. 162 of CWM):

Coh_fig_16

All edges in the above pentagon are directed, and the diagram is obviously commutative in BB (as BB is monoidal). This completes the proof of the proposition.

Including the unit and the unitors

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 λ e B (B)=ϱ e B (B)\lambda^{(B)}_{e_B} = \varrho^{(B)}_{e_B} 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 𝒢 n\mathcal{G}'_n 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 BB as the original path. The main ingredient in the following proposition:

Proposition

Let

ususu u \stackrel{s'}{\to} u' \stackrel{s''}{\to} u''

be two directed arrows of 𝒢 n\mathcal{G}'_n with an associator appearing in ss' and a unitor appearing in ss'' (note: the definition of ”directed” is extended in an obvious way to include unitors). Then either there exists a directed arrow us 1uu\stackrel{s_1}{\to} u'' containing a unitor with (s 1)=(s)(s)\mathcal{I}(s_1)=\mathcal{I}(s'')\circ\mathcal{I}(s'), or there exist directed s 1s_1, s 2s_2 as in

us 1?s 2u u \stackrel{s_1}{\to} ? \stackrel{s_2}{\to} u''

with s 1s_1 containing a unitor, s 2s_2 containing an associator, and (s 2)(s 1)=(s)(s)\mathcal{I}(s_2)\circ\mathcal{I}(s_1) = \mathcal{I}(s'')\circ\mathcal{I}(s').

This proposition may be proved by a long and tedious induction on ss' and ss''.

For this I needed the triangle identities and the naturality of α (B)\alpha^{(B)} (as mentioned in CWM), but also the naturality of ϱ (B)\varrho^{(B)} and λ (B)\lambda^{(B)}, as well as the bifunctoriality of B\otimes_B. For example, consider:

Coh_fig_17

(where some associator appears in β\beta). So – what am I missing here?

Recall that our original goal is to show that any two paths in 𝒢 n\mathcal{G}'_n with the same starting vertex and the same ending vertex have the same composition in BB. There is still a path from any vertex of 𝒢 n\mathcal{G}'_n to w (n)w^{(n)} (first remove all units, then proceed as in the case of 𝒢 n\mathcal{G}_n), 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 𝒢 n\mathcal{G}'_n starting at some vertex vv and ending at w (n)w^{(n)} have the same composition in BB. 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

Coh_fig_18

Here, clean(v)clean(v) is the word obtained by removing all instances of the unit from vv (this can be defined rigorously by induction), and rr is the total number of units appearing in vv. The right part of the last diagram, where there are no units and unitors, commutes in BB 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 BB (”coherence for the unitors”).

First one must prove that two parallel directed arrows with unitors in 𝒢 n\mathcal{G}'_n have the same interpretation in BB .
Recall that in 𝒢 n\mathcal{G}_n (no units and no unitors), there are no parallel directed arrows. However, this is not the case in 𝒢 n\mathcal{G}'_n (for example, consider λe 0e 0,1e 0^λe 0,1e 0^ϱe 0:e 0(e 0e 0)e 0e 0\lambda e_0\otimes e_0,1 e_0\hat{\otimes} \lambda e_0, 1 e_0\hat{\otimes} \varrho e_0\colon e_0\otimes(e_0\otimes e_0)\rightrightarrows e_0\otimes e_0). Hence, we must settle for equality of the interpretations in BB.

For this, I used induction on the total number of ^\hat{\otimes} in both ss and ss', using ϱ e B (B)=λ e B (B)\varrho^{(B)}_{e_B}=\lambda^{(B)}_{e_B} and the naturality of ϱ (B)\varrho^{(B)} and λ (B)\lambda^{(B)}. 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 rr of units in vv. Considering the left part of the last diagram, if u 1=u 1u_1=u'_1, as in

Coh_fig_19

then the parallel arrows are equal in BB, while the ”large diamond” on the right commutes in BB by the induction hypothesis.

We can therefore assume that u 1u 1u_1 \neq u'_1. As in the case of coherence for the associator, it is sufficient to
find a commutative diamond, that is, to find some vertex ww of 𝒢 n\mathcal{G}'_n and directed arrows γ\gamma and γ\gamma' in SS' containing unitors, as in

Coh_fig_20

such that the diamond on the left commutes in \mathcal{B}:
If we find such ww, γ\gamma and γ\gamma', then since by the induction hypothesis the upper and lower parallelograms on the right commute in BB, we are done.

Finally, the required commutative diamond may be found by induction on vv.

Proof of version 2 of the coherence (Theorem VII.2.1 of CWM)

I intend to come back and fill this. The most difficult part was already proved above.

The construction of F[1]F[1] and proof of universality

The category 𝒲\mathcal{W} 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 F[1]F[1] that will be almost obviously a free monoidal category on one generator. This would mean that F[1]F[1] is isomorphic to 𝒲\mathcal{W}, and in particular has one-element hom-sets. The fact that F[1]F[1] is free and has one-element hom-sets may then serve as yet a third version of coherence.

This should still be filled.

Moving from one variable to any number of variables: The category It(B)It(B)

This should still be filled.

References

Revised on January 17, 2013 01:10:45 by Urs Schreiber (203.116.137.162)