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: String diagrams and coherence

Patrick Nicodemus (Feb 16 2025 at 11:42):

Lately I have been wondering "Why are the zig-zag identities the equations we choose to impose for the definition of an adjunction, and not some other equations?"

The only answer I could come up with is "because those equations guarantee that, in the string diagram calculus for adjunctions, any two homotopy-equivalent diagrams are equal." This seems like a satisfactory answer to me - we could still write down the string diagram calculus without the zig-zag identities, we would just have to be very pedantic about the exact positions of the bends and natural transformations.

This raises the follow-up question, for me: Are there other examples of categorical theories where the basic coherence result can be characterized as "any homotopic diagrams are equal"? Another example is the theory of a monoid, where any two morphisms $M^{\otimes m}\to M^{\otimes n}$ are equal if they are "homotopic" as string diagrams.

Are there papers which have explored other coherence theorems in category theory along these lines? I am especially interested in theories like the two I have just described, where coherence is more complicated than the coherence result for monoidal categories that "all diagrams commute", necessitating this additional structuring for string diagrams.

Mike Shulman (Feb 16 2025 at 15:08):

This is not an answer to your follow-up question, but I think a better answer to your original question is "because that's what makes the unit+counit definition of adjunction equivalent to the bijection-of-hom-sets definition".

Riley Shahar (Feb 16 2025 at 16:44):

Patrick Nicodemus said:

Are there papers which have explored other coherence theorems in category theory along these lines? I am especially interested in theories like the two I have just described, where coherence is more complicated than the coherence result for monoidal categories that "all diagrams commute", necessitating this additional structuring for string diagrams.

Braided monoidal categories, I guess? Here the theorem is that maps in a free strict BMC are equal if and only if their string diagrams are related by an isotopy in $\mathbb{R}^3$. (By comparison, you can phrase the symmetric monoidal categories one as isotopy in $\mathbb{R}^4$.)

Peter Selinger has a giant survey of various kinds of monoidal categories, the associated string diagrammatic calculus, and the appropriate kind of automorphism of the space under which those diagrams should be preserved: https://arxiv.org/pdf/0908.3347.

Patrick Nicodemus (Feb 16 2025 at 16:50):

Mike Shulman said:

This is not an answer to your follow-up question, but I think a better answer to your original question is "because that's what makes the unit+counit definition of adjunction equivalent to the bijection-of-hom-sets definition".

I agree that's a good answer. Let me share my motivating question. Consider the following theorem from the theory of preorders, which could be formalized in a simple dependent type theory such as lambda Pi.

Let C, D be preorders. Let G : D -> C be monotonic, and let F0 : C -> D be a set function between the underlying sets. Suppose that we have x <= G F0 x for all x in C and (x <= G y)->(F0 x <= y) for all x in C and y in D. Then F0 is monotonic.

We can then talk about "categorifications" of this theorem, which extend/subsume this theorem by adding new assumptions at higher dimensions and derive new conclusions at higher dimensions. One such categorification is the theorem that if C and D are categories, G is a functor, and (F0, eta : x -> G F0 x, alpha : (x -> G y) -> (F0 x <= y)) is a family of universal arrows, then F0 extends to a functor.

Another, slightly more general categorification at the same dimension would be to say that if C, D are "truncated bicategories" ( bicategories with no coherence equations), G: D -> C is a truncated lax functor, and (F, eta, alpha) are a family of 2-universal arrows in the right sense, then F is a truncated colax functor.

But there are probably very many 2-dimensional "categorifications" of the original theorem about preorders - given any arbitrary set of unmotivated equations between the natural transformations of an adjunction we could impose these equations and get some 2-dimensional structure whose 1-dimensional truncation models the original theorem.

I'm asking why some 2-dimensional theorems seem more natural and important than others. The coherence assumptions for a category and a functor feel easy to motivate, because they're of the form "all terms are equal". But the coherence relations which relate eta : x <= G F0 x to alpha: (x <= G y)-> (F0 x <= y), it feels harder to identify robust principles of "coherence" which justify them, principles which could also be used to justify coherence conditions for other categorical structures.

Patrick Nicodemus (Feb 16 2025 at 17:05):

The mental picture I have is that working in some appropriate CwF model, we have this original theorem about preorders I stated, as a term living over a context: $\Gamma \vdash A : M$.

Let $\Gamma_0 = C : Preorder, D: Preorder, G: Monotone(D,C)$. There is a projection morphism of contexts $\pi: \Gamma\to \Gamma_0$ that discards $F, \eta, \alpha$.

Let $\Gamma'_0 = C : Cat, D: Cat, G: Functor(D,C)$ and let $\pi_0 : \Gamma'_0 \to \Gamma_0$ discard the higher dimensional information in the context.

I am wondering whether there is any sense in which the context $\Gamma' = C : Cat, D: Cat, G: Functor(D,C), F : \forall x. UnivArrow(x, G)$ is privileged among spans making this square commute, like being "terminal among coherent spans", whatever that means.

Amar Hadzihasanovic (Feb 16 2025 at 18:43):

In my own hierarchy of concepts, I would consider Kan extensions (as in formal 2-category theory) to be most natural and fundamental, since they have pretty much the simplest non-trivial universal property that one can consider in a 2-category, involving unique factorisations of diagrams that consist of a single 2-cell.

Amar Hadzihasanovic (Feb 16 2025 at 18:45):

If you accept Kan extensions as a natural concept, then you should also accept that it is natural to ask when does, e.g., the right Kan extension of an identity 1-cell exist along another 1-cell, since that is another question that you can always ask at any 0-cell inside any 2-category.

Amar Hadzihasanovic (Feb 16 2025 at 18:47):

And then it is not a stretch to wonder, when is the universal property of a Kan extension preserved by whiskering with other 1-cells --- that is, the universal 2-cell is (in a certain sense) “universal in every context”? That's what is called an absolute Kan extension.

Amar Hadzihasanovic (Feb 16 2025 at 18:49):

But “an absolute right Kan extension of an identity 1-cell along another 1-cell” is the same thing as the counit of an adjunction.

Amar Hadzihasanovic (Feb 16 2025 at 18:54):

So I would say that arguably adjunctions are “just” a particularly nice kind of Kan extension!

As evidence towards this, I'd also give the fact that, if you see monoidal category theory as a special case of 2-category theory (by passing to “deloopings”), then right Kan extensions correspond to internal homs, while adjunctions to dualities; and, for example, symmetric monoidal closed categories seem way more common than compact closed categories.

Amar Hadzihasanovic (Feb 16 2025 at 18:54):

I don't think it is a stretch to say that compact closure is “just” a particularly nice kind of monoidal closure.

Amar Hadzihasanovic (Feb 16 2025 at 18:55):

(Where, in particular, the universal property of an internal hom happens to be expressible in algebraic form... by the zig-zag identities)