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: "general position", linearity in category theory

Patrick Nicodemus (Jan 06 2025 at 18:08):

Hi folks. Recently I have been thinking about coherence conditions in category theory. I want to extend a well known theorem about Grothendieck fibrations to fibrations between bicategories. This should be straightforward and boring, so my mind drifted to the question of whether there was a way to get it easily by appealing to general coherence principles in categories and bicategories.

I noticed that many coherence conditions in category theory concern terms which are in "general position", i.e., they have the maximal number of free variables possible. For example, over the typing context
$x_0,x_1,x_2,x_3, x_4: Ob , f : x_0 \to x_1, g : x_1 \to x_2, h : x_2 \to x_3, k : x_3\to x_4$, all words in the language of category theory using each of $f,g,h,k$ are provably equal. However, over the context
$x : Ob, f : x \to x, g : x\to x$, there are many words which are not provably equal, such as $f^2$, $f^3$, $fg$ and $gf$.
One way we can explain this is that the context is not fully general: $f\circ g$ is well defined over the context $f : x\to y, g : y \to z$. We could also conjecture a linearity requirement - $f\circ f$ is not linear (the variable occurs twice) so it shouldn't appear in coherence conditions.

Similarly, in a symmetric monoidal category, not all diagrams commute, because do not require the coherence law
$sym_{a,a} = id_{a \otimes a } : a \otimes a \cong a \otimes a$, because this is not in "most general position" (the symmetry isomorphism can be stated more generally) or alternatively because $a \otimes a$ is not linear.

This seems closely related to the observation that many algebraic theories can be presented using operads, which are more narrow/restrictive than Lawvere theories, and don't allow duplication or deletion of variables from a context. Even stronger are the theories presented by finitary Cartesian monads, in which variables cannot even be permuted.

Some questions:

1. Broadly speaking, why do you think categorical coherence conditions tend to be of this form? Why does so much of category theory seem to fit in this "operad" fragment of algebra rather than the "Lawvere theory" fragment?
2. Is there a satisfying explanation for why symmetric monoidal categories are the "right" notion of categorified commutative monoid and not a stronger one with $sym_{a,a} = id_{a \otimes a }$?
3. Is there a satisfying explanation for why a category is the "right" notion of a vertically categorified preorder, and we don't consider vertically categorified preorders with laws like $fg=gf$ when this is valid?
4. Can someone point me to a precise general definition of coherence for categorical structures along the lines of "all diagrams in general position commute" that is sufficiently general that it includes the coherence conditions for, say, a bicategory and a lax pseudofunctor between bicategories

Todd Trimble (Jan 06 2025 at 21:13):

Your first two paragraphs prompt the question: have you read the work of Max Kelly in this area? To start with, he and Eilenberg developed a graphical calculus for tracking compositions of extranatural transformations, and this calculus is an early precursor of the proof nets of linear logic. The paper by Kelly and Mac Lane, Coherence in Closed Categories, JPAA 1) refers this graphical calculus to state coherence theorems in their paper.

A coherence problem is formalized as the problem of deciding equality of morphisms in free structures, in this case, in free smc categories on categories $C$ (relative to being able to decide equality of morphisms in $C$). A first result is that the free structure $F(C)$ can be constructed as a certain "wreath product" $F(1) \wr C$ (along the lines of Max Kelly's [[clubs]], which were invented around the same time), so that it suffices to decide equality in $F(1)$. The coherence theorem of Kelly and Mac Lane is a partial solution, which says that as long as objects $X, Y$ in $F(1)$ are isomorphic to objects that do not involve the monoidal unit $I$ in their syntactic construction, two morphisms from $X$ to $Y$ are equal if and only if they have the same extranaturality graph.

Anyway, for anyone new to this area, I would recommend reading, in addition to these two papers, the early papers of Lambek

• J.Lambek, Deductive systems and categories I. Syntactic calculus of residuated categories, Math. Systems Theory 2 (1968) 287-318

and

• J.Lambek, Deductive systems and categories II. Standard constructions and closed categories, in: Lecture Notes in Mathematics 86 (Springer-Verlag 1969) pp 76- 122

which inaugurated these attacks on non-trivial coherence problems, in particular showing how to adapt Gentzen cut elimination techniques to study coherence problems. For me, these papers were the real eye-opener; I found his description of the essential technique a lot clearer than the account given by Kelly and Mac Lane (who acknowledge his influence). There's also a book by Lambek's student Manfred Szabo, titled Algebra of Proofs, which unfortunately got a bad reputation because some of his technical claims about solutions to coherence problems were found to be overreaching and incorrect, but I think it's just fine in terms of laying out some basic ideas and strategies.

By the way, Lambek uses terminology very similar to yours, Patrick: he refers to proofs or morphisms [morphisms in a free smc structure, for instance, where these morphisms are viewed as equivalence classes of proofs] as being of "maximal generality". The Eilenberg-Kelly-Mac Lane graphs are a way of visualizing such maximally general morphisms, where caps and cups and lines connect variables ("atomic types", syntactically speaking) that are linked through instances of extranaturality or naturality of definable maps.

Not sure how followable this is, but I'm happy to discuss (this is the same area that I did my thesis on).

Patrick Nicodemus (Jan 06 2025 at 22:03):

Thanks very much, Todd. I really appreciate it. The term "general position" also occurs in a phd thesis on coherence in 2-categorical rewriting problems by Jonathan Asher Cohen. However I think Cohen slips up in a few instances and forgets this requirement and so his main result characterizing coherent rewriting systems appears to be incorrect.

I'll check out the sources you linked. Right now I'm refreshing myself on Eugenia Cheng's writeup of your "iterative operadic theory of n-categories"

Amar Hadzihasanovic (Jan 07 2025 at 08:43):

My hunch is that the "general position" thing is somewhat of a red herring:

• in higher categories and higher groupoids, the composable diagrams --- for which a coherence theorem stipulates "an essentially unique composite exists" --- have a geometric interpretation as certain contractible topological spaces, typically closed balls or wedges of balls;
• most structures for which one encounters coherence theorems are 2-dimensional, or "functionally" 2-dimensional (i.e. higher-dim phenomena can be encoded by 2-dimensional data, as in the case of braidings or symmetric braidings);
• in two dimensions, the composable diagrams happen to satisfy certain extra acyclicity conditions, which no longer hold in higher dimensions---the "contractibility" aspect appears to be way more stable and important than the "acyclicity" aspect, see the discussion in this paper or chapter 8 of my book

Now I think that the "general position" is a shadow of "acyclicity", since acyclicity prevents a variable from appearing twice in a chain of compositions, just as a vertex cannot appear twice in a path in an acyclic graph.
So I'd believe that a characterisation of diagrams to which coherence applies that is based on "general position" would also fail to generalise to higher-dimensional coherence theorems.

Patrick Nicodemus (Jan 07 2025 at 23:40):

@Amar Hadzihasanovic I think I understand the gist of your comments. I am wondering if the alternate approach you suggest in your book is applicable to symmetric monoidal categories. I can imagine formally adjoining an edge from $m \cdot m$, where $m$ is a 1-cell from a $0$-cell $\bullet$ to itself, but would this be appropriately "contractible?"