Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Counterexample to "folk coherence"

Jules Hedges (Jul 19 2020 at 10:04):

Several years ago (I think 2015) I saw a seminar by Peter Hines about Mac Lane's coherence theorem. It seems he never wrote a paper about it, and I'm planning to contact him to ask what happened, but I'll ask here first whether anyone knows this construction or anything equivalent. Everything I'm about to write is from 5 years ago and has the potential to be inaccurate. Hines constructed an example of a monoidal category using Thompson's Group F as a starting point, which was (obviously) not a counterexample to Mac Lane's coherence theorem but was a counterexample to the "folk" version, ie. "all diagrams commute", ie. admits a diagram that looks like it ought to commute but doesn't. I think the point of the seminar was that it is unsound to draw string diagrams in this category, but it might have been a more general moral like "people who draw string diagrams ought to be less blasé about coherence"

Amar Hadzihasanovic (Jul 19 2020 at 10:21):

Could this be it?

Amar Hadzihasanovic (Jul 19 2020 at 10:21):

Or at least a related talk

Jules Hedges (Jul 19 2020 at 10:26):

Definitely related. I saw it in London, and I think he made the example with Thompson's F (which he mentions right at the end of these slides) the central example. But this would be equally good as a counterexample, maybe clearer

Amar Hadzihasanovic (Jul 19 2020 at 10:32):

I agree that the “all diagrams commute” formulation of coherence is misleading.

Amar Hadzihasanovic (Jul 19 2020 at 10:33):

But “string diagrams are sound for non-strict monoidal categories” would be a good folk statement of coherence.

Amar Hadzihasanovic (Jul 19 2020 at 10:34):

So I do not think that his point would have been that string diagrams are not sound for a certain example. Maybe a “naive” interpretation of string diagrams is unsound.

Jules Hedges (Jul 19 2020 at 10:34):

Context: I remembered this talk deep down this twitter thread: https://twitter.com/danghica/status/1284390006921068544

Does anyone have any references on string diagrams for non-strict monoidal categories?

- danghica (@danghica)

Amar Hadzihasanovic (Jul 19 2020 at 10:42):

Yeah, I don't think I've seen anywhere that really spells it out.

Amar Hadzihasanovic (Jul 19 2020 at 10:43):

I know exactly how to do it, though. When I have time maybe I should write some short note and put it on the arxiv for reference.

Jules Hedges (Jul 19 2020 at 10:47):

Here's the answer I gave (which is entirely pragmatic, it's an algorithm I implemented once in code that is now deployed, and it hasn't gone wrong): https://twitter.com/_julesh_/status/1284793008655867904

@danghica @johncarlosbaez Here's the algorithm I used. Every vertical cut cuts through a bunch of strings, ie. an object. You have (possibly different) bracketings of that object on the left and right, which come from the choice of horizontal cuts on the immediate left and right....

- julesh (@_julesh_)

Amar Hadzihasanovic (Jul 19 2020 at 10:49):

Yes, that's exactly right.

Amar Hadzihasanovic (Jul 19 2020 at 10:51):

The way I would put it is that coherence enters at the level of the “pasting theorem for monoidal categories”:

On individual nodes/boxes of a string diagrams, you make a choice of bracketing for the interpretation. E.g. you interpret a node with inputs $(a_1,\ldots,a_n)$ and outputs $(b_1, \ldots, b_m)$ as a morphism with fully left-bracketed inputs and outputs.

Amar Hadzihasanovic (Jul 19 2020 at 10:52):

Then coherence tells you that you can extend this interpretation uniquely to string diagrams with multiple nodes.

Amar Hadzihasanovic (Jul 19 2020 at 10:53):

And that's because whenever you do an allowed composition (along $k$ wires, $k \geq 0$) you can insert a unique structural morphism that rebrackets everything in order to make the types match.

Amar Hadzihasanovic (Jul 19 2020 at 11:00):

Now I think the kind of incorrect “folk” reasoning with string diagrams that Hines may be targeting is this:

• “Unitors and associators become 'invisible'/become identities with string diagrams!”

Jules Hedges (Jul 19 2020 at 11:00):

I guess this works because you only invoke coherence for each individual "infinitesimally thick" structure morphism that sits on a vertical cut. Mac Lane's theorem says that there is only one choice. If you attempted to apply coherence to a whole diagram, it might go wrong

Amar Hadzihasanovic (Jul 19 2020 at 11:02):

I'm not sure I understand what “applying coherence to a whole diagram” would mean...

Jules Hedges (Jul 19 2020 at 11:05):

If you say "this diagram can be interpreted as all these different composite morphisms, which are the same except they involve some different structure morphisms, which is ok because Mac Lane says they are equal" - an incorrect use of the coherence theorem

Jules Hedges (Jul 19 2020 at 11:06):

Amar Hadzihasanovic said:

Now I think the kind of incorrect “folk” reasoning with string diagrams that Hines may be targeting is this:

• “Unitors and associators become 'invisible'/become identities with string diagrams!”

As far as I can tell "unitors and associators become invisible" is basically correct, if possibly not precise enough to be promoted to a theorem

Amar Hadzihasanovic (Jul 19 2020 at 11:06):

Yes, I agree. The correct thing to say is “this diagram has a unique interpretation by Mac Lane coherence: this one”.

Amar Hadzihasanovic (Jul 19 2020 at 11:08):

So, here's another thing that's counterintuitive, but the case of unitors and the case of associators are somehow really logically independent.

Jules Hedges (Jul 19 2020 at 11:09):

To be precise: Let's say you have a diagram with one vertical cut, with $f$ on the left and $g$ on the right, and with 2 possible structure morphisms on the boundary $\alpha$ and $\alpha'$. Incorrect reasoning: "The diagram can be interpreted as either $g \circ \alpha \circ f$ or $g \circ \alpha' \circ f$, which are equal by Mac Lane's theorem." Correct reasoning: "$\alpha = \alpha'$ by Mac Lane's theorem, and therefore $g \circ \alpha \circ f = g \circ \alpha' \circ f$"

Amar Hadzihasanovic (Jul 19 2020 at 11:09):

Which is why “strictify associators” generalises very nicely to higher dimensions, but “strictify unitors” does not.

Amar Hadzihasanovic (Jul 19 2020 at 11:11):

So I would agree that “unitors and units can be rendered invisible” is a correct folksy statement of that part.

Amar Hadzihasanovic (Jul 19 2020 at 11:12):

But associators are different.

Amar Hadzihasanovic (Jul 19 2020 at 11:12):

First of all, as I said earlier, to even start making sense of string diagrams in a monoidal category, you have to make a choice of bracketing.

Amar Hadzihasanovic (Jul 19 2020 at 11:13):

So say you make the choice of leftmost (or rightmost) bracketing.

Amar Hadzihasanovic (Jul 19 2020 at 11:13):

Now try to draw an associator as a 3 input, 3 output diagram. You can't!

Amar Hadzihasanovic (Jul 19 2020 at 11:13):

It's not that it's invisible, it's just that it's not the right type!

Amar Hadzihasanovic (Jul 19 2020 at 11:14):

What you can draw is the “rebracketed associator”, which... just is the identity

Amar Hadzihasanovic (Jul 19 2020 at 11:15):

You could make the “perverse” choice of saying: well, instead I'm going to have inputs with leftmost bracketing and outputs with rightmost bracketing...

Amar Hadzihasanovic (Jul 19 2020 at 11:16):

Then you can draw an associator... but you can't draw an identity :>

Amar Hadzihasanovic (Jul 19 2020 at 11:17):

Whatever choice you make, you'll either be able to represent certain identities or certain structural morphisms, either one will “play the role of the identity”.

Amar Hadzihasanovic (Jul 19 2020 at 11:20):

Now, you can certainly represent an associator as a diagram with one input and one output (or two inputs $(a \otimes b, c)$ and two outputs, $(a, b \otimes c)$ etc). But then it will just be some morphism, it will play no structural role.

Amar Hadzihasanovic (Jul 19 2020 at 11:20):

And then certainly you can't “make it invisible”. This is the kind of wrong reasoning that Hines's counterexample is targeting.

Amar Hadzihasanovic (Jul 19 2020 at 11:21):

He has a diagram with two parallel “structural morphisms seen as morphisms with one input and one output”, and they are different.

Amar Hadzihasanovic (Jul 19 2020 at 11:21):

Which happens all the time.

Amar Hadzihasanovic (Jul 19 2020 at 11:25):

Perhaps a good way to condense some of this would be: “structurality is not a property of morphisms, it is a property of morphisms with a type...”

Jules Hedges (Jul 19 2020 at 11:30):

The level of subtlety here is ridiculous for something so apparently basic...

Jules Hedges (Jul 19 2020 at 11:31):

This makes sense though

Amar Hadzihasanovic (Jul 19 2020 at 11:32):

As I said, with units the story is different. There's no problem “drawing units and unitors” in string diagrams. Rather, the result here is that you can always push the unitors to the outside of the diagram in a unique way. And then you can invert them in a unique way to get rid of all the units. So you have a unique way to pass from a diagram-with-units to a diagram-without-units. It's more of a kind of elimination procedure.

Amar Hadzihasanovic (Jul 19 2020 at 11:33):

And one dimension up, that stops working, because as you move units around, you create braids.

Amar Hadzihasanovic (Jul 19 2020 at 11:38):

It's like the units are trying to bubble up to the surface of the diagram. In 2D the wires around them are inescapable walls. They have to be squeezed up straight.

Amar Hadzihasanovic (Jul 19 2020 at 11:39):

In 3D suddenly they have a choice. They can run loops around the wires...

Martti Karvonen (Jul 19 2020 at 15:56):

Amar Hadzihasanovic said:

Could this be it?

I'm struggling with some of the purported counterexamples. For instance, the Cantor monoid doesn't seem to give a monoidal category: after all, the monoid of scalars of a monoidal cat is always commutative but the Cantor monoid isn't. If you're just working with a semimonoidal category or something, then it's less clear how examples there illustrate what's wrong with the folk understading of coherence. But maybe I'm missing something?

Martti Karvonen (Jul 19 2020 at 16:11):

Amar Hadzihasanovic said:

I agree that the “all diagrams commute” formulation of coherence is misleading.

I'd like to play the devil's advocate in the hopes of learning something new. I've understood that the main reason that "all diagrams built from coherence isos commute" isn't strictly speaking true is because one might have non-trivial equalities between objects that let you compare morally/formally distinct such diagrams (so the correct statement is more like "all formal diagrams commute") i.e. you might be able to compose and compare certain isomorphisms "by accident". For instance, if your monoidal category is skeletal, we do have the equation $(A\otimes B)\otimes C=A\otimes (B\otimes C)$ at the level of objects but the associators might still be nontrivial. In this case it would be false to deduce e.g. that $\alpha^2=\alpha$ or the simpler $\alpha=id$, but in practice I suspect that people rarely feel tempted to do such errors anyway. Similarly, it might happen in some SMC that $A\otimes B=C\otimes D$ with no obvious relationship between the objects A and C and D and B - but I suspect that no one would assume that coherence would say anything of the "immoral composite" of symmetries $B\otimes A\to A\otimes B=C\otimes D\to D\otimes C$. So "all diagrams commute" seems to be instinctively understood as the correct "all formal diagrams commute".

Jules Hedges (Jul 19 2020 at 16:30):

Maybe "all reasonable diagrams commute" is better, then if anyone breaks it you can pull a True Scotsman and tell them their diagram wasn't reasonable

dusko (Jul 20 2020 at 13:20):

I don't think there is any handwaving or folk theorems in using string diagrams. Any monoidal category is equivalent with a monoidal category where the tensor is strictly associative and unitary: just take the category of strong endofunctors. The tensor is the composition. The symmetry or the braiding cannot be made strict without collapsing the whole thing. But the sting language expresses all that. And that is no accident: the geometry of string diagrams does not capture the monoidal structure by some accident. It is dual to the globular geometry, which is the algebra of composition. Joyal was aware of all that when he proposed that Penroses pictures should be taken seriously. It's all in old papers :)

Chad Nester (Jul 22 2020 at 07:39):

A precise development of string diagrams for non-strict monoidal categories is Blute, Cockett, Seely, and Trimble's "Natural Deduction and Coherence for Weakly Distributive Categories" (1996).

Chad Nester (Jul 22 2020 at 07:40):

While it might seem unrelated at first glance, as it deals with linearly distributive categories, these are precisely representable polycategories, which, when $\otimes$ and $\oplus$ coincide, are representable multicategories, which are exactly monoidal categories.

Chad Nester (Jul 22 2020 at 07:42):

There's an essay (available on Robert Seely's website) called "Proof Theory of the Cut Rule" (2017), that explains this, beginning with the representable multicategory / monoidal category case, in a very accessible way.