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: learning: questions

Topic: Using monoidal coherence effectively for enriched cats

Fernando Chu (Oct 02 2024 at 11:07):

The following is in a monoidal category $(C,\otimes, I)$. When establishing some basic properties of enriched categories, the following setting is common: We have some morphisms $f_i: I \to A_i$, and we want to show that two different ways of getting from $I \to A_1 \otimes \cdots \otimes A_n$ are equal. This involves many applications of naturality of the coherence data.

For a particular example, if we want to show that the two following two maps are equal:

$$I \otimes A \to (I \otimes I) \otimes A \to (C \otimes B) \otimes A \to C \otimes (B \otimes A) \\ I \otimes A \to B \otimes A \to I \otimes (B \otimes A) \to C \otimes (B \otimes A)$$

We need to use four naturality squares, despite being "obvious".

Is there a better way to do this? Clearly, the two morphisms above should be "equal" to the morphism $I \otimes I \otimes I \to C \otimes B \otimes A$. But coherence gets in the way of stating this as it is. On the other hand, the monoidal coherence theorem that I know (CWM) does not apply since it requires that the edges of the diagram are all coherence data. Do I need a new coherence theorem for this?

Jean-Baptiste Vienney (Oct 02 2024 at 11:18):

That’s a good question! Indeed MacLane coherence theorem doesn’t talk about this as far as I understand.

Such a coherence theorem is what we need to establish the correctness of string diagrams for monoidal categories with special strings with no input (like for the unit of a monoid) representing the morphisms $f_i$ from $I$ to $A_i$.

These kind of coherence theorems are covered in the paper « A survey of graphical languages for monoidal categories ». Just look at the subsection on monoidal categories. It is formalized in terms of a « monoidal signature » which encodes the generating objects and morphisms that you can use.

Jean-Baptiste Vienney (Oct 02 2024 at 11:22):

(I guess this theorem was first proved in « The geometry of tensor calculus I » by Joyal and Street, 1991.)

Fernando Chu (Oct 02 2024 at 11:53):

This seems to be precisely what I was looking for, thanks!