Thanks Todd! Let me rephrase some of that in language more familiar to me. I think what you wrote about span composites is correct, but I’d be more inclined to say the same thing by saying that $M'$ is the (bo,ff) factorization of the counit $p\colon F[M] \to M$. And similarly, saying that that square is a pullback is just saying that the functor $M' \to M^{st}$ is fully faithful. (In fact, of course, it is an equivalence, since both $M'$ and $M^{st}$ are equivalent to $M$.)

I don’t quite understand the pointed cliques yet. Partly I don’t see why my $M^{st}$, being the left adjoint as above, should necessarily the same as your $M^{st}$ constructed using cliques – is it?

But let me say something different which this triggered in my head, namely how to deduce strictification from coherence. Suppose we know that $F[M] \to F_s[M]$ is an equivalence (where $F_s$ denotes the free strict monoidal category). Then from some inverse to it we obtain a map $F_s[M] \to F[M] \to M$, and we can define $M^{st}$ to be the (bo,ff) factorization of this. It inherits a strict monoidal structure from $F_s[M]$, and its map to $M$ is fully faithful by definition, and surjective on objects since we have $M$ sitting inside $F_s[M]$; thus every monoidal category $M$ is equivalent to a strict monoidal category. This is essentially Power’s “general coherence result” for pseudoalgebras over 2-monads, composed with the equivalence $F \simeq F_s$ to turn an $F$-algebra (a monoidal category) into a pseudo $F_s$-algebra (an unbiased monoidal category).

I think a proof of coherence from strictification can also be derived with a little more work. The 2-monad morphism $F \to F_s$ induces a functor $StrMonCat \to MonCat$ over $Cat$, where in both 2-categories we include pseudo morphisms (i.e. strong=weak monoidal functors). This functor is clearly 2-fully-faithful, and assuming strictification, it is also essentially surjective up to equivalence; hence it is a biequivalence. Moreover, each forgetful functor $MonCat \to Cat$ and $StrMonCat \to Cat$ has a left biadjoint, namely $F$ and $F_s$ respectively, so the fact of this equivalence over $Cat$ means that these biadjunctions must induce equivalent (pseudo)monads, i.e. $F\simeq F_s$. (The proof that $F$ and $F_s$ are left biadjoints landing in the 2-categories of *pseudo* morphisms, not just strict ones, is in Blackwell-Kelly-Power and uses properties of the pseudo morphism classifier $(-)'$.)

Sorry for the delay in responding to your question, Mike. I’m not sure how well the following observations answer it, but here goes.

Let’s see: the free monoidal category $F[C]$ generated by a category $C$ is, in the notation at club, $F[1] \circ C$, where $F[1]$ is the free monoidal category on one generator. When I say “free monoidal” here, this means the left adjoint to the forgetful functor

$MonCat_s \to Cat$It looks like your $(-)': MonCat \to MonCat_s$ can be described as taking a monoidal category $M$, which has an underlying endospan $M_0 \leftarrow M_1 \to M_0$, to a monoidal category $M'$ whose underlying endospan is the span composite

$F[M]_0 \stackrel{p_0}{\to} M_0 \stackrel{M_1}{\to} M_0 \stackrel{(p_0)^*}{\to} F[M]_0$where $p: F[M] \to M$ is the counit at $M$ of the adjunction for the monadic functor $MonCat_s \to Cat$, and $p_0$ is the underlying function between object-sets. So in other words, this endospan may be equivalently written $(M')_1 \to F[m]_0 \times F[M]_0$.

The free strict monoidal category on a category $C$ would be $\mathbb{N} \circ C$. There is a quotient functor $q: F[C] = F[1] \circ C \to \mathbb{N} \circ C$ (induced from the obvious functor $F[1] \to \mathbb{N}$) which is a monoidal equivalence, as you hinted in speaking of the abstract version of the all-diagrams-commute theorem. This induces a quotient function $q_0: F[C]_0 \to (\mathbb{N} \circ C)_0$. Now if $M$ is a monoidal category, then according to what you wrote in #27, $(\mathbb{N} \circ M)_0$ is the underlying object-set $(M^{st})_0$. The underlying morphism-set is $quot(M')_1 = (M^{st})_1$.

Adopting the clique point of view on the construction of the monoidal category $M^{st}$, one connection between the string of adjunctions you wrote down and the abstract all-diagrams-commute theorem is concentrated in the statement that the following diagram is a pullback:

$\array{ (M')_1 & \stackrel{\langle dom_{M'}, cod_{M'} \rangle}{\to} & F[m]_0 \times F[M]_0 \\ \pi \downarrow & & \downarrow q_0 \times q_0 \\ (M^{st})_1 & \underset{\langle dom, cod \rangle}{\to} & (M^{st})_0 \times (M^{st})_0 }$where $\pi$ is the quotient map $(M')_1 \to quot(M')_1$, where $quot$ is your functor $MonCat_s \to StrMonCat_s$.

I think this can be understood by viewing $M'$ as a monoidal category of *pointed cliques*. (A pointed clique is exactly what one might think: a triple $(g, G, F: G \to C)$ where $G$ is a contractible groupoid and $g$ is an object of $G$. A morphism $(g, G, F: G \to C) \to (g', G', F': G' \to C)$ is just the component $h_{g, g'}$ of a morphism of cliques $h: (G, F: G \to C) \to (G', F': G' \to C)$, or rather the pair $(h_{g g'}, h)$.)

Then the functor $M' \to quot(M')$ can be understood as the process of forgetting the point of the pointed clique.

]]>I think I don’t understand the relationship between the “all diagrams commute” coherence theorem and the strictification theorem as well as I thought I did. A naive version of the “all diagrams commute” theorem of course follows from the strictification theorem since all diagrams commute in a strict monoidal category, while your description shows where the all-diagrams-commute theorem comes into proving the strictification theorem. (In other versions of the strictification theorem, it comes in in other places.) But there’s a more abstract version of the all-diagrams-commute theorem which says that the free strict monoidal category on some data is equivalent to the free non-strict one; how is that related to the string of adjunctions I just wrote down?

]]>@Mike #27 – thanks; that makes sense.

I made a little beginning for coherence theorem for monoidal categories. Rather a lot more to be filled in.

]]>The quick and dirty way is to say that its objects are formal parenthesized strings of objects of M, and the functor $M' \to M$ is fully faithful. The elegant way is to say that it’s a codescent object, as described in Steve Lack’s paper “codescent objects and coherence.”

]]>How do you describe the pseudo morphism classifier?

]]>Hmm, sorry, Todd, you’re right and I was wrong. I think what I should have said is that there are two adjunctions:

$MonCat\; \underoverset{incl}{(-)'}{\rightleftarrows} \;MonCat_s \;\underoverset{incl}{quot}{\rightleftarrows} \;StrMonCat_s$where $MonCat_s$ denotes non-strict monoidal categories and strict monoidal functors. The left adjoint $quot$ is the “wrong way to prove coherence” by taking a quotient, but its composite with the “pseudo morphism classifier” $(-)'$ is a correct strictification functor $(-)^{st}$, i.e. $M^{st} = quot(M')$. The strict functor I was thinking of is the counit $M'\to M$, which is a surjective equivalence in $MonCat$ (but not in $MonCat_s$).

]]>Oh, I thought for some reason that your previous post was something along the lines of, “Oh, Mike, I guess I was wrong”, but rereading it now, it appears that you were confused with Mike’s statement, not that you were confused and that he was right.

]]>What statement on what page?

]]>So is the page on the lab incorrect?

]]>@Mike #20: sorry, I’m confused. I think I agree that we have the adjunction you gave at the bottom (so that my explanation involved the unit of the adjunction, $M \to i(M^{st})$). So if $M$ starts out being strict, we have a counit $(i(M))^{st} \to M$ which is strict monoidal. But I don’t see a strict monoidal $M^{st} \to M$ for non-strict $M$. I do see strong monoidal retractions $M^{st} \to M$ of the unit which are non-canonical.

]]>Yes, “strong” always means up to isomorphism (as opposed to lax/colax). It’s unfortunate that when people say “weak” to mean up to isomorphism (as opposed to strict), then it means that strong=weak. (-:

]]>Strong monoidal functor = weak monoidal functor?

]]>That’s a great explanation, Todd; maybe it should go on the nlab at coherence theorem for monoidal categories. It’s not the way I usually think of strictification, though. In my head, the fundamental functor is not the strong monoidal embedding $M\to M^{st}$, but a *strict* monoidal functor $M^{st} \to M$, which happens to have a strong monoidal section forming a monoidal equivalence. From this point of view, the way coherence works with diagrams is that you draw the diagram in the strict world $M^{st}$, where it commutes, and then then map it forward into $M$ to get a corresponding diagram that also commutes there. Moreover, these two functors are the unit and counit of a strict 2-adjunction

where the left adjoint is strictification and the right adjoint is the inclusion. In particular, the strictification has a universal property: strict monoidal functors out of $M^{st}$ are the same as strong monoidal functors out of $M$.

]]>That’s precisely the way I imagined doing it, believe it or not.

]]>Okay, I found a bit more time, so let me make some remarks on how monoidal strictification works and how it leads to an elegant resolution of the concerns about reinstating associativities in diagrams.

Most people, when they first hear about strictifications, imagine that strictifying a monoidal category is like taking a quotient, in order to identify associativities with identities. That’s actually the wrong picture, and it leads to a lot of confusion. The right picture is that a monoidal category $M$ can be monoidally *embedded* in a strict monoidal category $M^{st}$, in which associativity and unit isomorphisms of $M$ are assembled into what Joyal calls “contractible networks”, or cliques (aka anaobjects). The cliques that so arise are then the objects of the strictification.

So, for example, a 4-fold tensor product like $(a^b \otimes (b^c \otimes c^d)) \otimes d$ is a vertex in a clique which consists of all five ways of bracketing $a^b \otimes b^c \otimes c^d \otimes d$ and the groupoid of associativities between them. Or more precisely, it consists of the infinitely many such bracketings with units inserted (e.g., $((a^b \otimes I) \otimes (b^c \otimes c^d)) \otimes (I \otimes d)$), as objects of the groupoid generated by associativity and unit isomorphisms between them. By Mac Lane’s coherence theorem (“all diagrams commute”), there is exactly one morphism between any two vertices in the clique, meaning that the groupoid is equivalent to a terminal groupoid, and therefore contractible.

Formally, a *clique* in a category $C$ consists of a contractible groupoid $G$ and a functor $F: G \to C$. A *morphism* between two cliques $(G, F: G \to C)$, $(G', F': G' \to C)$ is a collection of morphisms $F(g) \to F'(g')$, where $(g, g')$ ranges over $Ob(G) \times Ob(G')$, making all triangles in sight commute. (In fact, by contractibility, any one of the $F(g) \to F'(g')$ uniquely determines all the rest.) To form the monoidal strictification $M^{st}$, we take as objects those cliques in the monoidal category $M$ which arise by application of the “all diagrams commute” formulation of Mac Lane’s coherence theorem (which specifies the structure of the free monoidal category on one generator as a disjoint sum of contractible groupoids), and the morphisms in $M^{st}$ are defined to be morphisms of cliques. The precise description is laid out here, where it is indicated that the evident embedding $i: M \to M^{st}$ is an equivalence in $MonCat$.

In any case, because $M$ is *embedded* in $M^{st}$, any diagram we are trying to prove commutative in $M$ is *physically there* in $M^{st}$, but any associativities and units in the diagram get absorbed into cliques, or rather: any such associativity is one of the components $F(g) \to F'(g')$ of, and uniquely determines, an identity morphism of cliques. Therefore any such associativity in $M$ is reinterpreted as an identity in $M^{st}$, and the diagram we are trying to prove commutative in $M$ uniquely generates a corresponding “larger” diagram of cliques in the strict monoidal category $M^{st}$. So it is enough to prove the diagram commutes when interpreted in a strict monoidal category: we can then interpret the result in $M^{st}$, and the original diagram in $M$, which is embedded in the clique diagram, is then automatically commutative as well.

One may have to practice visualizing this before it all sinks in, but it’s a tremendously potent principle.

]]>The all-too-brief reply is that you never have to worry or weaken later: if the sentence to be decided is a non-evil sentence in the language of monoidal categories, then the truth value is automatically reflected and preserved by monoidal equivalences. So insofar as any monoidal category is monoidally equivalent to a strictified monoidal category, one may as well assume that the model in which one is working is strict monoidal, and let Mac Lane’s theorem worry about the rest so to speak – you never need to go back and “improve” the proof to take care of weakening. Commutativity of diagrams (i.e., equality of morphisms belonging to the same hom-set) falls under that heading of non-evil sentences.

I began to write out a longer reply to say this much more convincingly; what is really needed is to develop a clear picture of how monoidal strictifications work, something I learned by reading stuff by Joyal and/or Street (as in Braided Tensor Categories or Geometry of Tensor Calculus I). But I realized I won’t have time to do this now, and it may be a while before I can return to it (very busy day tomorrow). I should have time by Wednesday if not before to explain it further.

]]>So Todd, when you’re working things out when you have coherence diagrams, do you do something like prove the strict version first, then worry about keeping track of coherence afterwards?

I’m trying to figure out strategies to get the hang of this, and I wonder if it’s possible to do a strict proof, then weaken it.

]]>If we didn’t use the coherence theorem, is the proof pretty similar?

Very similar, yes. But probably much harder to typeset.

You probably didn’t know this, but the topic of my dissertation was coherence theorems. Specifically the coherence problem for closed symmetric monoidal categories (which formal diagrams commute?) and related structures like star-autonomous categories.

]]>(You owe me one. :-) )

I owe you a bunch already =p.

If we didn’t use the coherence theorem, is the proof pretty similar?

]]>Right. Here goes.

Preliminaries: by Mac Lane’s coherence theorem, we may assume the closed symmetric monoidal $M$ is strict monoidal, to avoid the nuisance of shuffling around associativities. (I am prepared to discuss this point further if needed.) To save typographical space, I’ll denote the internal hom $[b, a]$ in $V$ by $a^b$. Thus the composition $M$ takes the form $a^b \otimes b^c \to a^c$, and we have an adjunction isomorphism of the form

$\Phi_{y d z}: \hom_V(y, z^d) \cong \hom_V(y \otimes d, z).$A handy lemma we will need is that $\Phi(x \stackrel{f}{\to} y \stackrel{g}{\to} z^d) = (x \otimes d \stackrel{f \otimes d}{\to} y \otimes d \stackrel{\Phi(g)}{\to} z)$. That can be proven using the recipe for $\Phi$ in terms of the counit, that we discussed above.

We are trying to prove that the following diagram “D” commutes:

$\array{ a^b \otimes b^c \otimes c^d & \stackrel{a^b \otimes M}{\to} & a^b \otimes b^d \\ M \otimes c^d \downarrow & & \downarrow M \\ a^c \otimes c^d & \underset{M}{\to} & a^d }$It is enough to check that we get the same result on applying $\Phi$ to both legs of D. First, hit the leg going across and then down with $\Phi$. By the lemma, this is the composite

$a^b \otimes b^c \otimes c^d \otimes d \stackrel{1 \otimes M \otimes d}{\to} a^b \otimes b^d \otimes d \stackrel{1 \otimes e}{\to} a^b \otimes b \stackrel{e}{\to} a \qquad (1)$The first two arrows in (1) go across then down in a square:

$\array{ a^b \otimes b^c \otimes c^d \otimes d & \stackrel{1 \otimes M \otimes 1}{\to} & a^b \otimes b^d \otimes d \\ 1 \otimes 1 \otimes e \downarrow & & \downarrow 1 \otimes e \\ a^b \otimes b^c \otimes c & \underset{1 \otimes e}{\to} & a^b \otimes b }$which commutes (just hit the equation $e(M \otimes 1) = e(1 \otimes e)$ with $1 \otimes -$, here $a^b \otimes -$). So we can replace the composite of the first two arrows in (1) with the leg which goes down then across; thus the composite in (1) equals the following composite:

$a^b \otimes b^c \otimes c^d \otimes d \stackrel{1 \otimes 1 \otimes e}{\to} a^b \otimes b^c \otimes c \stackrel{1 \otimes e}{\to} a^b \otimes b \stackrel{e}{\to} a \qquad (2)$Okay, now hit the other leg of D with $\Phi$. Applying the lemma again, the result is

$a^b \otimes b^c \otimes c^d \otimes d \stackrel{M \otimes 1 \otimes d}{\to} a^c \otimes c^d \otimes d \stackrel{1 \otimes e}{\to} a^c \otimes c \stackrel{e}{\to} a \qquad (3)$Now the composites of (2) and (3) form the outer perimeter of a diagram

$\array{ a^b \otimes b^c \otimes c^d \otimes d & \stackrel{1 \otimes 1 \otimes e}{\to} & a^b \otimes b^c \otimes c & \stackrel{1 \otimes e}{\to} & a^b \otimes b \\ M \otimes 1 \otimes 1 \downarrow & & M \otimes 1 \downarrow & & \downarrow e \\ a^c \otimes c^d \otimes d & \underset{1 \otimes e}{\to} & a^c \otimes c & \underset{e}{\to} & a }$which commutes: the left square commutes by functoriality of $\otimes$, and the right square is another instance of the all-important equation $e(M \otimes 1) = e(1 \otimes e)$. Hence the composites (2) and (3) are equal, and we are done.

(You owe me one. :-) )

]]>Alright, I’ve gotten all of the above stuff, but now how do we check axiom 1.3? What does that whole thing tell us about $1\otimes M$?

We’re trying to show now that $M(M\otimes 1)=M(1\otimes M)a$.

]]>@Todd: I’m sorry, but I still dont understand how to do the computation

$e(M\otimes 1)=e(1\otimes e)a$. I have the diagram drawn out, but it’s the matter of showing that it commutes that I guess I’m not getting.

Unless… since M is the map $\psi(e(1\otimes e)a)$, then $psi^{-1}(M)=L([y,z]\otimes [x,y])\stackrel{L(M)}{\to}L([x,z]) \stackrel{e}{\to} z$, but $psi^{-1}(M)=e(1\otimes e)a$?

Edit: all clear nevermind.

]]>Added content to adjunction based on comments above. Links still needed.

]]>