The n-Category Café

(where by “break the example” I meant “present a trivial example breaking the claim”)

I don’t know of good axioms that win other than asking for global sections of internal hom to return the true hom, which is very strong.

Mike wrote:

Are you aware of the Eilenberg–Kelly definition of closed category, which has only an internal-hom but no tensor product?

Yes, thanks.

Our desire was to give a definition of ‘closed monoidal category’ that involves only a category, functors from products of this category and its opposite to products of this category and its opposite, natural isomorphisms between such functors, and equations between such natural isomorphisms. I’m now getting the strong impression that this is impossible.

In particular, it’s against our rules to explicitly mention the hom-functor

$$hom: C^{op} \times C \to Set$$

which would make the job easy, but it’s okay to mention the internal hom

$$\implies: C^{op} \times C \to C$$

Also, while Owen Biesel kindly presents the Eilenberg–Kelly definition of closed monoidal category in a way that comes close to satisfying our rules, he also uses dinatural transformations:

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

So, we may have to bite the bullet and use these.

Thanks for taking the trouble to list those axioms! I remember being awed by Eilenberg and Kelly’s original definition of closed categories that aren’t necessarily monoidal — but I can never remember the definition. Now that I’ve studied the lambda calculus it doesn’t look quite so crazy. When I get time, I’ll try to add it to the $n$Lab page on closed categories. It deserves to be better known!

Thanks! I’ve looked at this paper, but I’ll check it out again.

Do you think you know a general diagrammatic calculus for dinatural transformations? Or could you at least invent one if forced to do so at gunpoint?

Well I’m not sure what you mean by that. But possibly the answer is yes.

Do you think you know a general diagrammatic calculus for dinatural transformations?

I think you know this yourself, at least in certain forms. But your “bite the bullet” comment a while back makes me suspect that there’s something about the concept of dinatural transformation that bothers you. In fact, a lot of people seem to be bothered by this notion.

I am unfortunately not very capable with drawing diagrams in this medium, but let me say that you are surely already familiar with how dinatural transformations work diagrammatically – at least the type of dinatural transformations which are relevant to closed category theory. (Please mark my words here, because a lot of people, who have read the definition of dinatural transformation in say Categories for the Working Mathematician, are put off and develop a mental block about these things, but: the types of dinatural transformations which are relevant to closed category theory are the simplest, most (um) natural thing in the world.)

For these purposes, one should just forget the hexagon identity in Categories Work, and instead keep in mind two basic examples: the evaluation map

$$ev_{x, y}: x^y \otimes y \to x$$

which is dinatural in $y$, and the coevaluation map

$$coev_{x, y}: x \to (x \otimes y)^y,$$

also dinatural in $y$. [I’m using exponential notation for the internal hom, because it’s going to look a lot less cluttered than the notation which uses $\Rightarrow$, and it saves me a lot of typing.]

Let’s look first at evaluation. It is gotten by applying the adjunction $(- \otimes y) \dashv (-)^y$ to the identity

$$x^y \to x^y$$

which is of course natural in $y$. That is, we are “decurrying” the identity, where decurrying shifts the instance of $y$ in an arrow $z \to x^y$ over to the other side: $z \otimes y \to x$. Now: all dinaturality of the evaluation map means is that it is the decurryed analogue of what ordinary naturality means for the identity.

That is, if we stare at the naturality equation

$$(x^z \stackrel{x^g}{\to} x^y \stackrel{id_{x^y}}{\to} x^y) = (x^z \stackrel{id_{x^z}}{\to} x^z \stackrel{x^g}{\to} x^y)$$

and decurry each side of this equation in turn, we arrive at the equation

$$(x^z \otimes y \stackrel{x^g \otimes y}{\to} x^y \otimes y \stackrel{ev_{x, y}}{\to} x) = (x^z \otimes y \stackrel{x^z \otimes g}{\to} x^z \otimes z \stackrel{ev_{x, z}}{\to} x)$$

That’s all dinaturality means here. You can easily write up this equation in the diagrammatic calculus you and Mike have written about.

The general type of dinaturality we’re talking about here is contained in the following definition:

Definition: Let $F: C^{op} \times C \to C$ be a functor, and let $x$ be an object of $C$. A dinatural transformation from $F$ to $x$ consists of a family of morphisms

$$\theta_y: F(y, y) \to x$$

such that for each morphism $g: y \to z$, the following equation holds:

$$(F(z, y) \stackrel{F(g, y)}{\to} F(y, y) \stackrel{\theta_y}{\to} x) = (F(z, y) \stackrel{F(z, g)}{\to} F(z, z) \stackrel{\theta_z}{\to} x)$$

Written string-diagrammatically, this is saying something very simple. Hint: it looks like you are sliding a ‘$g$’ over a hump, from a covariant application of $g$ to a contravariant one.

The general point for closed category theory is that currying or decurrying, by applying an adjunction $(- \otimes y) \dashv (-)^y$, transfers instances of naturality in $y$ over to instances of dinaturality of $y$, and vice-versa. For example, we get the family of morphisms

$$coev_{x, y}: x \to (x \otimes y)^y$$

by currying the identity $x \otimes y \to x \otimes y$. The naturality in $y$ of the identity map is thereby transferred to dinaturality of $coev_{x, y}$ in the variable $y$, in the sense that the following equation holds:

$$(x \stackrel{coev_{x, y}}{\to} (x \otimes y)^y \stackrel{(x \otimes g)^y}{\to} (x \otimes z)^y) = (x \stackrel{coev_{x, z}}{\to} (x \otimes z)^z \stackrel{(x \otimes z)^g}{\to} (x \otimes z)^y)$$

and this leads to a second form of dinaturality:

Definition: Let $x$ be an object of $C$ and let $F: C^{op} \times C \to C$ be a functor. A dinatural transformation from $x$ to $F$ consists of a family of morphisms

$$\eta_y: x \to F(y, y)$$

such that (you fill in the rest).

Giving a diagrammatic presentation of this again makes it look like something very easy and obvious.

The cute thing about the definition of dinatural transformations as given by the hexagon identity in Mac Lane’s book is that it takes care of both these definitions in one fell swoop, without case-splitting. But, that sort of slick definition tends to obscure the true provenance of dinatural transformations, as they occur in nature. In nature, they practically always can be explained in terms of one of the two definitions I gave above. (Aside: that’s even true for the case of ‘Church numerals’.) And that is certainly the case for how they come up in closed category theory.

Moral: dinatural transformations are nothing to be afraid of. And they are perfectly natural (pun intended) from the standpoint of diagrammatic calculus.

The string diagram calculus useful for monoidal categories has a version which is moderately appropriate here, where a term built from object symbols and the hom-functor $[ ,]:C^{op}\times C\to C$ has an associated sequence of strings, each marked by a variable name and oriented up or down depending on the overall co- or contravariantness in that variable.

The idea is to interpret each hom-object $[A,B]$ as if the closed category were monoidal compact, rewriting it as $A^{*} \otimes B$, where $\otimes$ is the fictional tensor product. For example, the term $[[[A,B],C],D]$ becomes $(((A^*\otimes B)^*\otimes C)^*\otimes D) =C^*\otimes A^*\otimes B\otimes D$. Then the ordinary string diagram calculus applies, and in particular the map $I\to[A,A]$ becomes a map $I\to A^*\otimes A$, which we know to denote by a “cup” appropriately labeled and oriented. The Yoneda map $[A,B]\to[[C,A],[C,B]]$ similarly becomes a map $A^*\otimes B\to A^*\otimes C\otimes C^*\otimes B$, which is another “cup” (not a cap!) but oriented the other way and fenced in on either side by an identity string. Dinaturality is then as clear as Todd Trimble has just described it: morphisms on one side of a cup can swoop around to the opposite side.

Unfortunately, this “free compactification” loses a lot of necessary information. For example, $[[[A,B],C],D]$ and $[C,[[B,A],D]$ are in general not isomorphic, but they have the same presentation as $C^*\otimes A^*\otimes B\otimes D$; more description is required to determine which term from the closed, noncompact category is desired. Parentheses will do, but to save clutter these can be stored as a binary tree off to the side, whose leaves represent the variables and whose other nodes the intermediate stages of computation. The unit and Yoneda maps would then require rules for how they transform the trees so that the leaves continue to match the variables in the “compactified” expression.

Now, if you wanted, you could move into a three-dimensional picture, with the compact-style string diagram on a vertical plane running from bottom to top, and for each stage, a horizontal slice would be given by the binary tree, whose leaves are on the vertical plane at their respective locations. Stack all those horizontal slices together, and you’ve got a branching manifold behind the scenes of the original string diagram.

This works out to be what you get when you employ the picture notation developed in the above paper of Simon Willerton’s. As a tool for understanding the basic axioms for closed categories, it’s a bit messy, but it becomes clearer if you view the axioms applied to the vertical slices (the compact-style string diagrams) as being ordinary topological manipulations (which they are), and the branching behind as making sure you don’t accidentally try to compose maps that only appear to match (such as $1_{[[[A,B],C],D]}$ and $1_{[C,[[B,A],D]}$).

Now, when you work out what the string diagrams are for the two sides of the associativity-expressing axiom, you get something that looks coincidentally like dinaturality of Yoneda, only not quite. I think you’ll have to produce the diagrams yourself to see what I mean: one cup follows the orientation of the other until it has bent around completely, thickening the cup (actually thickening one cup and creating another) and adding a contravariant cap to the opposite side. Is there something deep going on here, with the topological motion mimicking the interpretation of dinaturality, or is it just a coincidence that that’s what this motion appears to be?

But presumably there are pseudomonoids in 2-Chu that are not of that form?