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: deprecated: logic

Topic: SupLat as a *-autonomous category

Chris Barrett (Aug 12 2023 at 11:31):

I've heard recently of a couple of non-degenerate models of (multiplicative) Linear Logic -- that is, *-autonomous categories -- which seem especially natural and simple, and which I'm intrigued by. Namely, these are the category SupLat of suplattices and FinBan of finite Banach spaces and contractions. However, I'm finding it hard to find references to detailed discussions of the *-autonomous structure for these categories.

My question stems partially from trying to build an intuition for the structures discussed in the paper Frobenius relations meet linear distributivity" by J M Egger. In it, he defines a notion of Frobenius algebra where the co/multiplication are defined with respect to _distinct_ monoidal structures, which interact via linear distributivity. In the abstract, he tantalizingly says:

"For example, when studying Frobenius algebras in the ∗-autonomous category Sup, the standard concept using only the usual tensor product is less interesting than a similar one in which both the usual tensor product and its de Morgan dual (par) are used."

but (as far as I can see) does not expand on this example. So, I'm looking for natural models of the structure he defines, starting with the suggested one in SupLat. Now, I could work out the details myself, but I was wondering first if anyone had any relevant references regarding these categories' *-autonomous structure, or any intuitions for the categories mentioned, and might be willing to exposit for me?

Cole Comfort (Aug 12 2023 at 12:35):

Chris Barrett said:

I've heard recently of a couple of non-degenerate models of (multiplicative) Linear Logic -- that is, *-autonomous categories -- which seem especially natural and simple, and which I'm intrigued by. Namely, these are the category SupLat of suplattices and FinBan of finite Banach spaces and contractions. However, I'm finding it hard to find references to detailed discussions of the *-autonomous structure for these categories.

My question stems partially from trying to build an intuition for the structures discussed in the paper Frobenius relations meet linear distributivity" by J M Egger. In it, he defines a notion of Frobenius algebra where the co/multiplication are defined with respect to _distinct_ monoidal structures, which interact via linear distributivity. In the abstract, he tantalizingly says:

"For example, when studying Frobenius algebras in the ∗-autonomous category Sup, the standard concept using only the usual tensor product is less interesting than a similar one in which both the usual tensor product and its de Morgan dual (par) are used."

but (as far as I can see) does not expand on this example. So, I'm looking for natural models of the structure he defines, starting with the suggested one in SupLat. Now, I could work out the details myself, but I was wondering first if anyone had any relevant references regarding these categories' *-autonomous structure, or any intuitions for the categories mentioned, and might be willing to exposit for me?

At the beginning of section 4, Jeff asks for what appears to be sup lattices internal to an elementary topos. He cites ``Joyal, A. and Tierney, M. (1984). An extension of the Galoist heory of Grothendieck. Mem. Amer. Math. Soc., 51(309):vii+71'' for a reference to the the *-autonomous structure.

John Baez (Aug 12 2023 at 13:21):

Cole Comfort said:

At the beginning of section 4, Jeff asks for what appears to be sup lattices internal to an elementary topos. He cites "Joyal, A. and Tierney, M. (1984). An extension of the Galois theory of Grothendieck. Mem. Amer. Math. Soc., 51(309):vii+71'' for a reference to the the *-autonomous structure.

Thanks very much! I have been studying "Grothendieck's Galois theory" for some time now and I didn't even know that Joyal and Tierney, two of my favorite mathematicians, wrote a paper about it. @Todd Trimble will probably be interested too, especially if star-autonomous categories get involved.

John Baez (Aug 12 2023 at 13:24):

There's a nice discussion of their paper on MathOverflow.

Todd Trimble (Aug 12 2023 at 14:35):

John Baez said:

Cole Comfort said:

At the beginning of section 4, Jeff asks for what appears to be sup lattices internal to an elementary topos. He cites "Joyal, A. and Tierney, M. (1984). An extension of the Galois theory of Grothendieck. Mem. Amer. Math. Soc., 51(309):vii+71'' for a reference to the the *-autonomous structure.

Thanks very much! I have been studying "Grothendieck's Galois theory" for some time now and I didn't even know that Joyal and Tierney, two of my favorite mathematicians, wrote a paper about it. Todd Trimble will probably be interested too, especially if star-autonomous categories get involved.

Of course I am well aware of this monograph! Not only for the fact that I was a Tierney student -- it has been very influential generally.

Todd Trimble (Aug 12 2023 at 14:36):

Getting back to Chris's question, the duality functor takes a sup-lattice $X$ to its order-theoretic opposite $X^{op}$, and takes a morphism $f: X \to Y$, i.e., a sup-preserving map, to $g^{op}: Y^{op} \to X^{op}$ where $f \dashv g$. (So, we're using the fact that sup-preserving maps between sup-lattices are left adjoints. This could be seen as an application of the adjoint functor theorem, but I want to point out that the calculation of $g$, namely $g(y) = \text{sup}\{x \in X: f(x) \leq y\}$, and the fact this works, is a simple direct argument which can be internalized inside any topos.)

Todd Trimble (Aug 12 2023 at 14:36):

The internal hom for sup-lattices $[X, Y]$ is the sup-lattice whose elements are sup-preserving maps $X \to Y$, which should be intuitively appealing. Notice that that $[X, Y] \cong [Y, X]^{op}$, by the process of taking $f \mapsto g$! Similarly, $[X, Y] \cong [Y^{op}, X^{op}]$, taking $f$ to $g^{op}$.

Todd Trimble (Aug 12 2023 at 14:36):

I'll claim now that $\Omega^{op}$ is the dualizing object for the star-autonomous structure. This stems from the observation that $\Omega$, the subobject classifier, is the free sup-lattice on one generator. This in turn means there is a natural isomorphism $X \cong [\Omega, X]$. Then

$X^{op} \cong [\Omega, X^{op}] \cong [X, \Omega^{op}]$

by the preceding paragraph, which shows that $[-, \Omega^{op}]$ is the dualization at least at the object level, and it also behaves correctly on morphisms (again by the preceding paragraph).

Todd Trimble (Aug 12 2023 at 14:36):

The tensor product of sup-lattices can be constructed by the usual universal methods (maps $X \otimes Y \to Z$ need to correspond to maps $X \times Y \to Z$ that preserve sups in separate variables). But more efficient is to admit straight up that, by star-autonomy, we're going to want

$X \otimes Y \cong [X, Y^{op}]^{op}$

(this is like $x \wedge y = \neg(x \Rightarrow \neg y)$), and so why not use the right-hand side of the last display to define the tensor product and check that works?

Todd Trimble (Aug 12 2023 at 14:37):

So we want to check that sup-lattice maps $[X, Y^{op}]^{op} \to Z$ are in natural bijection with maps $X \to [Y, Z]$. But the former correspond to maps

$Z^{op} \to [X, Y^{op}]$

and one checks directly that these are in bijection with maps $X \to [Z^{op}, Y^{op}] \cong [Y, Z]$, and we are done.

Mike Shulman (Aug 12 2023 at 15:32):

Chris Barrett said:

In the abstract, he tantalizingly says:

"For example, when studying Frobenius algebras in the ∗-autonomous category Sup, the standard concept using only the usual tensor product is less interesting than a similar one in which both the usual tensor product and its de Morgan dual (par) are used."

but (as far as I can see) does not expand on this example.

He does; it's Theorem 4.1:

A Frobenius monoid in [suplattices] amounts to a quantale equipped with a dualizing element; equivalently, a $\ast$-autonomous complete poset.

Thus we have an instance of the microcosm principle: Frobenius monoids can be defined internal to $\ast$-autonomous categories, and an internal Frobenius monoid in the $\ast$-autonomous category of suplattices is a $\ast$-autonomous category (with the additional restrictions of being thin and complete).

Mike Shulman (Aug 12 2023 at 15:44):

What's really tantalizing is the feeling that there ought to be a version of this where the internal Frobenius monoids are arbitrary $\ast$-autonomous categories, without the thinness and completeness restrictions. Unfortunately this doesn't quite work, but there are some approximations of it:

• The construction of $X\otimes Y = [X,Y^{\rm op}]^{\rm op}$ works in the context of locally presentable categories, but unfortunately $Y^{\rm op}$ itself is usually not locally presentable when $Y$, so that doesn't give a $\ast$-autonomous (2-)category.
• A Frobenius monoid in the bicategory [[Prof]] (which is compact closed, hence $\ast$-autonomous) is a "pro-$\ast$-autonomous category". This is due to Day and Street.
• You can generalize the ambient context for defining Frobenius monoids from a $\ast$-autonomous category to a polycategory. Then there is a 2-polycategory consisting of (arbitrary) categories and multivariable adjunctions, and a Frobenius monoid therein is precisely a $\ast$-autonomous category.
• A Frobenius monoid in the $\ast$-autonomous 2-category $\rm Chu(Cat,Set)$ is a sort of "polarized $\ast$-autonomous category".

Chris Barrett (Aug 13 2023 at 09:37):

Thank you all for the swift and helpful replies! Indeed, I missed Jeff's discussion where he addresses the example of Sup in slightly more generality than I expected -- and the reference to Joyal and Tierney's work. The latter looks surprisingly helpful, given the (to me) scary title, but unfortunately I can't find more than a small sample for free online.

Chris Barrett (Aug 13 2023 at 09:41):

I think I'm starting to get a feel for what's going on in this category -- thanks @Todd Trimble for the exposition. I found a link explaining that the category additionally has biproducts, given by the componentwise product of semilattices. I suppose that $\Omega$ and $\Omega^op$ are isomorphic, so that the category is also isomix.

One thing: you write that $[X,Y] \cong [Y,X]^{op}$, but doesn't this force the tensor and parr to coincide, since $[Y,X]^{op} = (Y^{op} \oplus X)^{op} = Y \otimes X^{op}$ and $[X,Y] = X^{op} \oplus Y$, where I write $\oplus$ for parr? I was under the impression that the category was supposed to be non-degenerate as a *-autonomous category.

Chris Barrett (Aug 13 2023 at 09:50):

I am still curious about finding a concrete description of the $\oplus$ connective "on its own terms", in order to compare it to $\otimes$. Part of my interest in this category is wondering if I can build an intuition for linear logic (for example, the sometimes mysterious "parr" connective) by studying naturally occurring examples such as Sup.

John Baez (Aug 13 2023 at 11:25):

I believe the subobject classifier $\Omega$ is not usually isomorphic to $\Omega^{\mathrm{op}}$, although they would be in a boolean topos, with "not" serving as the isomorphism.

Todd Trimble (Aug 13 2023 at 11:25):

Chris Barrett said:

I think I'm starting to get a feel for what's going on in this category -- thanks Todd Trimble for the exposition. I found a link explaining that the category additionally has biproducts, given by the componentwise product of semilattices. I suppose that $\Omega$ and $\Omega^op$ are isomorphic, so that the category is also isomix.

One thing: you write that $[X,Y] \cong [Y,X]^{op}$, but doesn't this force the tensor and parr to coincide, since $[Y,X]^{op} = (Y^{op} \oplus X)^{op} = Y \otimes X^{op}$ and $[X,Y] = X^{op} \oplus Y$, where I write $\oplus$ for parr? I was under the impression that the category was supposed to be non-degenerate as a *-autonomous category.

Oh, sorry, I shouldn't have written $[X,Y] \cong [Y,X]^{op}$, taking $f \mapsto g$, because $g$ is not a left adjoint! Stick to $[X,Y] \cong [Y^{op}, X^{op}]$, taking $f \mapsto g^{op}$.

It's not generally true that $\Omega \cong \Omega^{op}$, so it's not isomix. One generic sort of example is given by considering a topos of sheaves on a topological space. Here the poset of points $1 \to \Omega$ correspond to open subsets ordered by inclusion, but there are examples of topologies which are not isomorphic to their posetal opposites. For example, there is a topology on $\mathbb{N}$ where the open sets correspond to downward closed subsets of $\mathbb{N}$: this looks like the ordered set $\mathbb{N} \sqcup \{\infty\}$, which is not isomorphic to its opposite.

Todd Trimble (Aug 13 2023 at 12:54):

Unfortunately, I don't know of any great way of thinking about the par "independently" of $[X^{op}, Y]$ in the sup-lattice example.

I don't know if it would be of any great use to you, Chris -- I'm guessing probably not -- but seeing that Joyal and Tierney develop descent theory on frames viewed as certain commutative monoids in the star-autonomous category of sup-lattices, where the monoid multiplication is given by meet, it might be useful for somebody to know that Johnstone and Vickers, in their paper on the Tychonoff theorem without choice, take crucial advantage of an alternative description of frames as certain commutative monoids in the smc category of preframes (posets with directed joins and finite meets; the directed join operations and finite meet operations all commute with each other, i.e., are operations of a commutative theory, and the smc structure is derived from that observation). What I'm suggesting at is that the tensor product for preframes might be considered more "par-like", and a frame from this point of view is precisely a commutative monoid in preframes where the monoid multiplication is given by join, giving a sort of DeMorgan dual to the sup-lattice description of frames.

But I'm sort of shooting the shit here. Off-hand I don't know whether the smc category of preframes is star-autonomous. I'm inclined to doubt it, without really knowing why.

Todd Trimble (Aug 13 2023 at 13:14):

(Star-autonomy of preframes: yeah, unless I'm badly confused, I think not, since the initial object (empty) and terminal object are not isomorphic.)

Mike Shulman (Aug 13 2023 at 17:53):

A $\ast$-autonomous category doesn't have to have a zero object.

Mike Shulman (Aug 13 2023 at 17:53):

It's equivalent to its opposite, but that equivalence isn't usually the identity functor.

Mike Shulman (Aug 13 2023 at 17:53):

(Or maybe I misunderstood what you meant?)

Mike Shulman (Aug 13 2023 at 17:56):

As for the ⅋, I think if you have a way to think about $\otimes$ separately from the internal-hom, you can think about ⅋ in a dual way since $X⅋Y = (X^{\rm op} \otimes Y^{\rm op})^{\rm op}$. For instance, if you're willing to think of $X\otimes Y$ as analogous to the tensor product of vector spaces, with elements being "formal joins" of formal pairs $x\otimes y$, then you should be able to dually think of $X ⅋ Y$ as consisting of "formal meets" of formal pairs $x ⅋ y$.

Mike Shulman (Aug 13 2023 at 18:00):

We can also rephrase that in terms of universal properties. Recall that a morphism $X \to Y$ of suplattices is equivalently a join-preserving function $f^* :X\to Y$ or its adjoint meet-preserving map $f_* : Y\to X$. The universal property of $\otimes$ says that a morphism $X\otimes Y\to Z$ is determined by a function $f^* : X\times Y \to Z$ that preserves joins in each variable (which implies that it is part of a two-variable adjunction). Dually, the universal property of ⅋ says that a morphism $X \to Y ⅋ Z$ is determined by a function $f_* : Y \times Z \to X$ that preserves meets in each variable.

Mike Shulman (Aug 13 2023 at 18:04):

I found a link explaining that the category additionally has biproducts, given by the componentwise product of semilattices.

Yes, in fact it even has infinitary biproducts! This means it is an example (indeed, the only real example I know) of a monoidal category over which the [[Cauchy completion]] of a small category may no longer be small.

Todd Trimble (Aug 13 2023 at 18:22):

Mike Shulman said:

We can also rephrase that in terms of universal properties. Recall that a morphism $X \to Y$ of suplattices is equivalently a join-preserving function $f^* :X\to Y$ or its adjoint meet-preserving map $f_* : Y\to X$. The universal property of $\otimes$ says that a morphism $X\otimes Y\to Z$ is determined by a function $f^* : X\times Y \to Z$ that preserves joins in each variable (which implies that it is part of a two-variable adjunction). Dually, the universal property of ⅋ says that a morphism $X \to Y ⅋ Z$ is determined by a function $f_* : Y \times Z \to X$ that preserves meets in each variable.

That's a nice formulation!

Todd Trimble (Aug 13 2023 at 18:25):

Mike Shulman said:

It's equivalent to its opposite, but that equivalence isn't usually the identity functor.

Oh duh. Yeah.

(Of course star-autonomous categories don't have to have a terminal/initial object, but preframes do.)

Chris Barrett (Aug 14 2023 at 13:06):

John Baez said:

I believe the subobject classifier $\Omega$ is not usually isomorphic to $\Omega^{\mathrm{op}}$, although they would be in a boolean topos, with "not" serving as the isomorphism.

Sorry, I suppose I wasn't clear -- I meant only that specifically in the category Sup, where $\Omega$ is the two-element suplattice, that $\Omega$ is isomorphic to its dual. This wouldn't hold for a general subobject classifier, as you say.

Chris Barrett (Aug 14 2023 at 13:11):

Mike Shulman said:

We can also rephrase that in terms of universal properties. Recall that a morphism $X \to Y$ of suplattices is equivalently a join-preserving function $f^* :X\to Y$ or its adjoint meet-preserving map $f_* : Y\to X$. The universal property of $\otimes$ says that a morphism $X\otimes Y\to Z$ is determined by a function $f^* : X\times Y \to Z$ that preserves joins in each variable (which implies that it is part of a two-variable adjunction). Dually, the universal property of ⅋ says that a morphism $X \to Y ⅋ Z$ is determined by a function $f_* : Y \times Z \to X$ that preserves meets in each variable.

Thanks for spelling this out! This is incredibly helpful. I feel I've got a much better intuition for the category, thinking about things this way.

finegeometer (Aug 21 2023 at 18:21):

Am I correct in computing that the tensor product $X \otimes Y$ of suplattices consists of Galois connections between $X$ and $Y$, with $(f_1,g_1) \leq (f_2,g_2) \iff (\forall x. f_1(x) \leq f_2(x)) \iff (\forall y. g_1(y) \leq g_2(y))$?

I imagine the elements of $X ⅋ Y$ would then be some sort of "dual Galois connection", where we have $a \geq g(f(a))$ and $b \geq f(g(b))$ instead of $a \leq g(f(a))$ and $b \leq f(g(b))$.

John Baez (Aug 21 2023 at 19:27):

finegeometer said:

Am I correct in computing that the tensor product $X \otimes Y$ of suplattices consists of Galois connections between $X$ and $Y$, with $(f_1,g_1) \leq (f_2,g_2) \iff (\forall x. f_1(x) \leq f_2(x)) \iff (\forall y. g_1(y) \leq g_2(y))$?

That's hard to believe. It would mean that given an element of $X \otimes Y$ and and an element of $X$ we can get an element of $Y$. How does that work?

Mike Shulman (Aug 21 2023 at 19:42):

I think this is correct, from the characterization that Todd gave, $X\otimes Y = [X, Y^{\rm op}]^{\rm op}$. This means that an element of $X\otimes Y$ is a sup-preserving map $X \to Y^{\rm op}$, which by the adjoint functor theorem has a right adjoint, giving a contravariant "right adjunction" a.k.a. Galois connection.

Mike Shulman (Aug 21 2023 at 19:44):

I admit I don't immediately see how to extract an element of $Y$ from an element of $X\otimes Y$ and an element of $X$ without using this characterization. It's tricky because the operation is contravariant in the element of $X$.

John Baez (Aug 21 2023 at 20:39):

Okay, that's cool. For some silly reason I was thinking "Galois connection" here meant covariant Galois connection, and thus sup-preserving map $X \to Y$ , which made it all seem all the more wrong. But okay: a sup-preserving map $X \to Y^{\rm op}$.

John Baez (Aug 21 2023 at 20:40):

It would still be fun to see explicitly how we extract an element of $Y$ from an element of $X \otimes Y$ and an element of $X$. That too seems terribly wrong if we're used to tensor products of vector spaces, or of abelian groups!

Mike Shulman (Aug 21 2023 at 21:14):

Maybe this is it? Fixing $x\in X$ gives a map $x : I \to X$. Tensoring with $Y$ gives a map $Y \cong I\otimes Y \xrightarrow{x \otimes 1_Y} X\otimes Y$. This map is sup-preserving and thus has a right adjoint; applying that adjoint to an element of $X\otimes Y$ gives an element of $Y$.

John Baez (Aug 21 2023 at 22:10):

So in lowbrow terms maybe we do something like this?

1) Given $x \in X$ and $a \in X \otimes Y$, we get an element of $Y$ that's the inf of the set of $y \in Y$ such that $a \le x \otimes y$ .

or

2) Given $x \in X$ and $a \in X \otimes Y$, we get an element of $Y$ that's the sup of the set of $y \in Y$ such that $x \otimes y \le a$.

Both these elements exist, since suplattices have infs, but I need to think about which one is right.

John Baez (Aug 21 2023 at 22:19):

Okay, let me figure it out. I hate this stuff.

Mike Shulman said:

Maybe this is it? Fixing $x\in X$ gives a map $x : I \to X$. Tensoring with $Y$ gives a map $Y \cong I\otimes Y \xrightarrow{x \otimes 1_Y} X\otimes Y$. This map is sup-preserving and thus has a right adjoint; applying that adjoint to an element of $X\otimes Y$ gives an element of $Y$.

If we call the right adjoint $g : X \otimes Y \to Y$ we have

$x \otimes y \le a \iff y \le g(a)$

John Baez (Aug 21 2023 at 22:27):

So it looks like 2) is right: $g(a)$ is the sup of all $y \in Y$ such that $x \otimes y \le a$.

Mike Shulman (Aug 21 2023 at 23:07):

Yes, that sounds right. I always remember that the construction in the adjoint functor theorem is "backwards": right adjoints are "limity" but when you construct them using AFT you use a colimit, and dually.

Mike Shulman (Aug 21 2023 at 23:08):

Anyway, I think Galois connections are kind of a neat way to think about the tensor product of suplattices. I don't think it occurred to me before to say it that way.

Mike Shulman (Aug 21 2023 at 23:08):

And it does make it clear why there are two tensor products, because as finegeometer said you can have both "right" and "left" Galois connections.

John Baez (Aug 21 2023 at 23:13):

Mike Shulman said:

I always remember that the construction in the adjoint functor theorem is "backwards": right adjoints are "limity" but when you construct them using AFT you use a colimit, and dually.

This backwardsness, and various other possible "sign errors" that I can make around here, are why I said "I hate this stuff".

John Baez (Aug 21 2023 at 23:15):

But anyway, @finegeometer's description of the tensor product of suplattices in terms of Galois connections is really cool! I was so surprised by it that I couldn't believe it!