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: event: ACT@UCR

Topic: April 22nd: Michael Shulman

John Baez (Apr 21 2020 at 16:08):

In the fourth talk of the ACT@UCR seminar, Michael Shulman will tell us how to create nice string diagams for any closed symmetric monoidal category.

His talk will take place on Wednesday April 22nd at 5 pm UTC, which is 10 am in California, or 1 pm on the east coast of the United States, or 6 pm in England. It will be held online via Zoom, here:

https://ucr.zoom.us/j/607160601

He needs to teach right after his talk - but he will join our discussions here at 8pm UTC, which is 1 pm in California or 4 pm on the east coast of the US, or 9 pm in England.

John Baez (Apr 21 2020 at 16:09):

• Michael Shulman, Star-autonomous envelopes.

Abstract. Symmetric monoidal categories with duals, a.k.a. compact monoidal categories, have a pleasing string diagram calculus. In particular, any compact monoidal category is closed with [A,B] = (A* ⊗ B), and the transpose of A ⊗ B → C to A → [B,C] is represented by simply bending a string. Unfortunately, a closed symmetric monoidal category cannot even be embedded fully-faithfully into a compact one unless it is traced; and while string diagram calculi for closed monoidal categories have been proposed, they are more complicated, e.g. with "clasps" and "bubbles". In this talk we obtain a string diagram calculus for closed symmetric monoidal categories that looks almost like the compact case, by fully embedding any such category in a star-autonomous one (via a functor that preserves the closed structure) and using the known string diagram calculus for star-autonomous categories. No knowledge of star-autonomous categories will be assumed.

John Baez (Apr 21 2020 at 16:11):

$\;$

This is especially interesting to me since Mike Stay and I introduced string diagrams for monoidal closed categories in a somewhat ad hoc way in our Rosetta Stone paper - but the resulting diagrams required clasps and bubbles. Shulman's new approach sounds attractive.

John Baez (Apr 21 2020 at 16:18):

Here's our string reduction for beta reduction in the cartesian closed category coming from the lambda calculus, for example:

Sam Tenka (Apr 21 2020 at 21:41):

This sounds awesome. But I have a regular conflict at that time. Are the UCR talks recorded?

sarahzrf (Apr 21 2020 at 21:43):

they are!

Joe Moeller (Apr 21 2020 at 21:52):

Here's our YT channel:
https://www.youtube.com/channel/UCUQlS-R4O094jP0sGHDnrjA

John Baez (Apr 22 2020 at 02:39):

Michael Shulman's talk is based on this paper:

• Michael Shulman, Star-autonomous envelopes.

Mike Shulman (Apr 22 2020 at 02:46):

I don't expect I'll make it through the entire paper, and I'll certainly be skimming lightly over the proofs. But after the talk everyone should be better-equipped to go read the paper.

Mike Shulman (Apr 22 2020 at 02:47):

BTW, in John's example string diagram, the conclusion is that you can just omit the clasps and bubbles and it still works!

sarahzrf (Apr 22 2020 at 04:09):

John Baez said:

Here's our string reduction for beta reduction in the cartesian closed category coming from the lambda calculus, for example:

$\qquad$ beta reduction

hmmmmmmm havent i seen something suspiciously like this on joe's twitter

Christian Williams (Apr 22 2020 at 06:23):

Wow, this paper looks great. Looking forward to the talk.

sarahzrf (Apr 22 2020 at 17:17):

ooh, proof net stuff?

sarahzrf (Apr 22 2020 at 17:19):

yesss, proof nets

John Baez (Apr 22 2020 at 18:07):

Among other things this talk somehow made proof nets seem more approachable than ever before, to me at least!

Robin Piedeleu (Apr 22 2020 at 18:07):

I wonder what is the star-autonomous envelope of a Cartesian closed category? A category that is Cartesian and star autonomous is necessarily a poset, right? I wonder what comes out of the construction then.

John Baez (Apr 22 2020 at 18:08):

So I guess you get a cartesian closed category embedded in a star-autonomous one that can't itself typically be cartesian closed....

John Baez (Apr 22 2020 at 18:09):

This would be a great question for @Mike Shulman.

John Baez (Apr 22 2020 at 18:09):

It would be fun for me to see what you get when you start with Set.

Todd Trimble (Apr 22 2020 at 18:10):

John Baez said:

So I guess you get a cartesian closed category embedded in a star-autonomous one that can't itself typically be cartesian closed....

It might be spiritually akin to embedding Cat into Prof, where the cartesian product is no longer the "cartesian" product in Prof.

John Baez (Apr 22 2020 at 18:10):

:+1:

Nicolas Blanco (Apr 22 2020 at 18:11):

I wonder what is the envelop of Vect (where objects are vector spaces that may be infinite dimensional).

Aleks Kissinger (Apr 22 2020 at 18:12):

organisers: any chance of having the video of Mike's talk uploaded w/ enough time to watch before Mike comes back online?

Robin Piedeleu (Apr 22 2020 at 18:12):

Todd Trimble said:

John Baez said:

So I guess you get a cartesian closed category embedded in a star-autonomous one that can't itself typically be cartesian closed....

It might be spiritually akin to embedding Cat into Prof, where the cartesian product is no longer the "cartesian" product in Prof.

You somehow flatten the higher-order structure when you embed Cat in Prof, or Set in Rel in that way. The embedding is not closed monoidal, or am I confused?

Cole Comfort (Apr 22 2020 at 18:15):

Robin Piedeleu said:

Todd Trimble said:

John Baez said:

So I guess you get a cartesian closed category embedded in a star-autonomous one that can't itself typically be cartesian closed....

It might be spiritually akin to embedding Cat into Prof, where the cartesian product is no longer the "cartesian" product in Prof.

You somehow flatten the higher-order structure when you embed Cat in Prof, or Set in Rel in that way. The embedding is not closed monoidal, or am I confused?

Embedding sets into spans or jointly monic spans rel, the cartesian product no longer is even a categorical product.

Bartosz Milewski (Apr 22 2020 at 18:15):

So what's the relation between Chu(Cat, Set) and Prof?

Todd Trimble (Apr 22 2020 at 18:15):

You're right about that. Prof (for small cats) is compact closed.

Todd Trimble (Apr 22 2020 at 18:16):

The Chu construction won't be compact closed.

John Baez (Apr 22 2020 at 18:16):

Aleks Kissinger said:

organisers: any chance of having the video of Mike's talk uploaded w/ enough time to watch before Mike comes back online?

All depends on how hard I work. I'll try it.

John Baez (Apr 22 2020 at 18:18):

It's taking Zoom a while to process the recording. I can make a crappy unedited version available pretty soon though.

Todd Trimble (Apr 22 2020 at 18:20):

Yeah, I didn't mean to throw people off with my remark about Prof. I tried to hedge that before with the word "spiritually", just referring to the fact that the cartesian product will no longer be cartesian in this or that envelope. Seems everyone understood that.

John Baez (Apr 22 2020 at 18:20):

Anyway, I'd like to see what happens when we do this game to Set. I guess one way to think about it is to learn how to draw valid string diagrams with caps and cups in (the star-autonomous envelope of) Set, and learn to work with them, and get some intuition for them.

sarahzrf (Apr 22 2020 at 18:20):

it would be amusing if this just produces Rel

sarahzrf (Apr 22 2020 at 18:21):

oh wait, i guess he said it was fully faithful

sarahzrf (Apr 22 2020 at 18:21):

oh, and the thing about compact closure >.<

John Baez (Apr 22 2020 at 18:21):

Yeah, it can't be Rel.

Nicolas Blanco (Apr 22 2020 at 18:21):

I think that in Chu(Cat,Set) the profunctors are the objects.

Christian Williams (Apr 22 2020 at 18:23):

So I believe we're defining a 2-functor from SMCC to *Auto, but I'm having trouble finding this in the paper.
Does this seem right; would this be a left 2-adjoint?

John Baez (Apr 22 2020 at 18:24):

Not SMC - symmetric monoidal closed categories, right?

Cole Comfort (Apr 22 2020 at 18:25):

John Baez said:

Anyway, I'd like to see what happens when we do this game to Set. I guess one way to think about it is to learn how to draw valid string diagrams with caps and cups in (the star-autonomous envelope of) Set, and learn to work with them, and get some intuition for them.

In a *-autonomous category (or more generally, a linearly distributive category) there is a tractable algorithm for checking the validity of proof nets. I wonder if there is such a way to check if a net in the envelope is in the image of the embedding.

eric brunner (Apr 22 2020 at 18:26):

i've homological algebra at 1 so i'll miss the follow-up. i'll re-watch and take notes. nicely done talk. glad to see the multicategory bits towards the 11:00 mark. thanks!

Robin Piedeleu (Apr 22 2020 at 18:26):

Cole Comfort said:

John Baez said:

Anyway, I'd like to see what happens when we do this game to Set. I guess one way to think about it is to learn how to draw valid string diagrams with caps and cups in (the star-autonomous envelope of) Set, and learn to work with them, and get some intuition for them.

In a *-autonomous category (or more generally, a linearly distributive category) there is a tractable algorithm for checking the validity of proof nets. I wonder if there is such a way to check if a net in the envelope is in the image of the embedding.

There are correctness criteria for intuitionistic proof nets, by Lamarche, I believe.

sarahzrf (Apr 22 2020 at 18:28):

@Nicolas Blanco looks like a morphism (P : C ⇸ D) → (Q : C' ⇸ D') will be a functor F : C → C' and a functor G : D' → D such that G^* ∘ P = Q ∘ F_*

John Baez (Apr 22 2020 at 18:28):

Christian Williams said:

So I believe we're defining a 2-functor from SMCC to *Auto, but I'm having trouble finding this in the paper.
Does this seem right; would this be a left 2-adjoint?

It definitely has the flavor of a left 2-adjoint. Maybe Mike or someone can prove that.

Reid Barton (Apr 22 2020 at 18:29):

The name "envelope" would suggest this as well.

sarahzrf (Apr 22 2020 at 18:29):

i bet in a 2-chu construction thats a ≅ instead

Nathanael Arkor (Apr 22 2020 at 18:29):

Christian Williams said:

So I believe we're defining a 2-functor from SMCC to *Auto, but I'm having trouble finding this in the paper.
Does this seem right; would this be a left 2-adjoint?

It looks like the definition of $*P$ at the bottom of page 2, except that SMCCs are being considered as symmetric multicategories and hence polycategories.
(Edit: this only gives *-polycategories, not *-autonomous categories.)

sarahzrf (Apr 22 2020 at 18:29):

if P and Q are hom functors for 2 categories, then the morphisms between them are gonna be adjunctions :o

Cole Comfort (Apr 22 2020 at 18:30):

Robin Piedeleu said:

Cole Comfort said:

John Baez said:

Anyway, I'd like to see what happens when we do this game to Set. I guess one way to think about it is to learn how to draw valid string diagrams with caps and cups in (the star-autonomous envelope of) Set, and learn to work with them, and get some intuition for them.

In a *-autonomous category (or more generally, a linearly distributive category) there is a tractable algorithm for checking the validity of proof nets. I wonder if there is such a way to check if a net in the envelope is in the image of the embedding.

There are correctness criteria for intuitionistic proof nets, by Lamarche, I believe.

If mean a correctness result for monoidal closed categories using the string diagrams of intuitionistic proof nets, if I understood the talk correctly. Could one not form a proof net in the envelope which does not correspond to a morphism in the monoidal closed category.

sarahzrf (Apr 22 2020 at 18:31):

it does seem like the chu construction might naturally lend itself to double categories—anyone know about that?

sarahzrf (Apr 22 2020 at 18:32):

@Cole Comfort mike said that the embedding was fully faithful, so it just comes down to whether the domain & codomain are objects in the image of the embedding

John Baez (Apr 22 2020 at 18:32):

Hey, I was gonna say that. :upside_down:

Nicolas Blanco (Apr 22 2020 at 18:32):

sarahzrf said:

it does seem like the chu construction might naturally lend itself to double categories—anyone know about that?

Mike Shulman did that (even poly double category) ^_^
https://arxiv.org/pdf/1806.06082.pdf

sarahzrf (Apr 22 2020 at 18:33):

yeah lol i was ctrl+f'ing "double" on the nlab page for chu construction while typing that in here and i found a thing but i couldnt tell if it was what i was looking for :thinking:

sarahzrf (Apr 22 2020 at 18:34):

wait omg i remember googling a while back about whether multivariable adjunctions were a thing and i think i almost landed on an ncatcafe page about something related to this o_o

sarahzrf (Apr 22 2020 at 18:34):

neat

sarahzrf (Apr 22 2020 at 18:35):

oh jeez this looks like a rabbit hole

Nicolas Blanco (Apr 22 2020 at 18:39):

sarahzrf said:

wait omg i remember googling a while back about whether multivariable adjunctions were a thing and i think i almost landed on an ncatcafe page about something related to this o_o

Indeed multivariable adjunctions are important for polycategories. The 2-polycategory MVAdj is analogous to the 2-category Adj. In particular multivariable adjunctions are profunctors representable in each variables.

sarahzrf (Apr 22 2020 at 18:40):

i should learn about polycategories sometime

sarahzrf (Apr 22 2020 at 18:40):

they seem pleasant

Martti Karvonen (Apr 22 2020 at 18:42):

Cole Comfort said:

John Baez said:

Anyway, I'd like to see what happens when we do this game to Set. I guess one way to think about it is to learn how to draw valid string diagrams with caps and cups in (the star-autonomous envelope of) Set, and learn to work with them, and get some intuition for them.

In a *-autonomous category (or more generally, a linearly distributive category) there is a tractable algorithm for checking the validity of proof nets. I wonder if there is such a way to check if a net in the envelope is in the image of the embedding.

The embedding given by the result is full, so as long as the net depicts a morphism between objects in the image, it's in the image too, no?

Aleks Kissinger (Apr 22 2020 at 18:42):

@John Baez thanks!

Cole Comfort (Apr 22 2020 at 18:42):

Martti Karvonen said:

Cole Comfort said:

John Baez said:

Anyway, I'd like to see what happens when we do this game to Set. I guess one way to think about it is to learn how to draw valid string diagrams with caps and cups in (the star-autonomous envelope of) Set, and learn to work with them, and get some intuition for them.

In a *-autonomous category (or more generally, a linearly distributive category) there is a tractable algorithm for checking the validity of proof nets. I wonder if there is such a way to check if a net in the envelope is in the image of the embedding.

The embedding given by the result is full, so as long as the net depicts a morphism between objects in the image, it's in the image too, no?

Yes, I realize, this now

John Baez (Apr 22 2020 at 18:43):

@Aleks Kissinger - sorry, that was the wrong talk. Zoom is still "processing".

Aleks Kissinger (Apr 22 2020 at 18:45):

haha, okay. i was confused when your message vanished. :)

i think there is a way you can live-stream on youtube in parallel w Zoom, then once the stream is over it stays as a normal video. however i'm not (yet) in possession of the techical know-how to do this

John Baez (Apr 22 2020 at 18:46):

According to @Paolo Perrone YouTube allows this when your channel has at least 1000 subscribers.

John Baez (Apr 22 2020 at 18:46):

He's doing it for the MIT seminar.

John Baez (Apr 22 2020 at 18:47):

Maybe I should tell everyone on Twitter to subscribe to our channel.... I hadn't thought it was worthwhile, but maybe now I do.

sarahzrf (Apr 22 2020 at 18:49):

John Baez said:

Among other things this talk somehow made proof nets seem more approachable than ever before, to me at least!

how much sequent calculus do you know?

John Baez (Apr 22 2020 at 18:49):

No more than strictly necessary, I guess.

sarahzrf (Apr 22 2020 at 18:49):

because if you know your sequent calculus, proof nets should be very appealing once you get the idea

Todd Trimble (Apr 22 2020 at 18:51):

John, you and I ought to talk about proof nets some time.

John Baez (Apr 22 2020 at 18:51):

I would be really happy if I could understand Gentzen's proof of the consistency of Peano arithmetic using "cut elimination" and other things. (Induction up to $\epsilon_0$ is the only part I really get!)

sarahzrf (Apr 22 2020 at 18:51):

cut elimination is cool :)

John Baez (Apr 22 2020 at 18:52):

Okay, @Todd Trimble. That sounds vaguely threatening. :upside_down: But I know it's not.

John Baez (Apr 22 2020 at 18:52):

I get the vague idea of cut elimination.

John Baez (Apr 22 2020 at 18:52):

That is, I vaguely get the idea of cut elimination.

sarahzrf (Apr 22 2020 at 18:53):

although personally, i only really appreciated it once i grasped the sort of organizational principles of natural deduction, of sequent calculus, and how they were different and related

John Baez (Apr 22 2020 at 18:53):

Somehow sources that talk about Gentzen's proof of the consistency of PA often shy away from laying out the whole proof... I get the feeling that it's really complicated.

sarahzrf (Apr 22 2020 at 18:54):

i think gentzen's proof of cut eliminiation goes through a mix rule to account for contraction

sarahzrf (Apr 22 2020 at 18:54):

you can't really do that in, say, linear logic, and it gets considerably trickier

John Baez (Apr 22 2020 at 18:54):

I get the basic idea of the sequent calculus and how it's different from natural deduction.

John Baez (Apr 22 2020 at 18:55):

Anyway, yes, I'd someday like a slow and patient explanation of proof nets, with tons of pictures - this thing Mike said is better than anything I'd seen so far, or at least it felt better.

John Baez (Apr 22 2020 at 18:56):

But it would really "clinch the deal" if after a lot of work I understood Gentzen's proof of the consistency of PA.

sarahzrf (Apr 22 2020 at 18:56):

:thumbs_up:

sarahzrf (Apr 22 2020 at 18:58):

oh, by the way—theres a thing called logitext you can use to do sequent calculus derivations in your browser, but it doesnt support linear logic or gentzen's LJ/LK, so i made my own version https://github.com/sarahzrf/sequents

ive found it super useful for doing derivations when i need to develop my intuition

John Baez (Apr 22 2020 at 19:00):

Okay, @Aleks Kissinger , I think this one is for real:

https://ucr.zoom.us/rec/share/2uJ2JJX53GdJYLeW8maCfv8_HNzXeaa8g3AYq_AMy0fmnGVIynGw4BEb_UzBX6c6?startTime=1587573842000

John Baez (Apr 22 2020 at 19:01):

The show starts around 20 minutes or so...

Aleks Kissinger (Apr 22 2020 at 19:10):

do i need a password?

John Baez (Apr 22 2020 at 19:12):

You shouldn't - are you stuck?

John Baez (Apr 22 2020 at 19:13):

I guess this plan to do things quicker than usual isn't much quicker...

John Baez (Apr 22 2020 at 19:18):

The next approach is to get the video here:

http://math.ucr.edu/home/baez/mathematical/ACTUCR/Shulman_Star-Autonomous_Envelopes_original.mp4

Aleks Kissinger (Apr 22 2020 at 19:18):

Screenshot-from-2020-04-22-20-17-45.png

looks like this ^^

Oscar Cunningham (Apr 22 2020 at 19:19):

That last link works for me

Aleks Kissinger (Apr 22 2020 at 19:19):

second link works!

John Baez (Apr 22 2020 at 19:19):

Oh, this seems to be the password:

5p!*u3$@

John Baez (Apr 22 2020 at 19:19):

That should let you livestream it, maybe more easily than the version on my website.

John Baez (Apr 22 2020 at 19:20):

(I never do things this way... I usually take my time and put the videos on YouTube...)

Mike Shulman (Apr 22 2020 at 19:30):

Just finished teaching, now going to each lunch. Will be back in half an hour to chat. In the meantime I've posted my "slides" at http://home.sandiego.edu/~shulman/papers/clsaut-act-ucr.pdf .

John Baez (Apr 22 2020 at 19:31):

Thanks!

Mike Shulman (Apr 22 2020 at 20:01):

Hello everyone!

John Baez (Apr 22 2020 at 20:05):

Hi!

John Baez (Apr 22 2020 at 20:05):

So there were a bunch of questions already in this thread...

John Baez (Apr 22 2020 at 20:05):

it does seem like the chu construction might naturally lend itself to double categories—anyone know about that?

John Baez (Apr 22 2020 at 20:06):

Also:

So I believe we're defining a 2-functor from [symmetric monoidal closed categories] to [star-autonomous categories, but I'm having trouble finding this in the paper.

Does this seem right; would this be a left 2-adjoint?

Mike Shulman (Apr 22 2020 at 20:07):

I see there was one question about cartesian closed categories. John is right that when you start with a cartesian closed category, you end up embedding it in a *-autonomous one whose tensor is no longer cartesian. However, you can do a bit better than this: although I didn't mention it in the talk, in the paper I also proved that you can choose the embedding to preserve any given set of nonempty limits and colimits that exist in C. So if you start from a cartesian closed category and choose the embedding to also preserve binary products, then for objects A and B in the image of the embedding, the tensor $A \boxtimes B$ will still be a cartesian product in the envelope. But it won't be the case for objects that aren't in the image of the embedding, and the unit $\top$ won't generally be terminal in the envelope.

John Baez (Apr 22 2020 at 20:08):

That's nice! I was wondering what your construction would give in the case of (Set, x), and now I'm wondering that about this new "improved" version too.

Mike Shulman (Apr 22 2020 at 20:08):

Yes, it's interesting to see explicitly what happens in Set, or more generally to a cartesian closed category. I worked this out in some more detail at one point, let me see if I can reconstruct it.

Mike Shulman (Apr 22 2020 at 20:10):

But first to reply to the other questions: as was pointed out by someone else, the Chu construction is indeed naturally a double category, in which the other kind of morphism is covariant in both components. This is sketched (and used!) in the paper; more details (along with the 2-Chu construction) are in my other paper http://tac.mta.ca/tac/volumes/35/4/35-04abs.html .

Cody Roux (Apr 22 2020 at 20:13):

It's very finicky, since the association between derivations and ordinals is a bit wrong: you get some "off by 2" errors at places. Obviously it's spelled out in all its gory in Troelstra & Schwichtenberg poorly named "Basic Proof Theory"

John Baez (Apr 22 2020 at 20:14):

I have a feeling Cody's comment is a response to some earlier stuff about Gentzen's proof, not Mike's latest comment! (I always make this sort of slip myself.)

Mike Shulman (Apr 22 2020 at 20:15):

As for functoriality, the envelope is not the left 2-adjoint from closed symmetric monoidal categories to *-autonomous ones. I believe it is a functor, but the pieces it's put together from have different universal properties. First, the construction of $\ast\mathcal{C}$ from $\mathcal{C}$ is the left adjoint from multicategories to *-polycategories (polycategories equipped with strictly involutive duals). Next we forget the *-structure to get a polycategory, then apply Hyland's "modules" functor -- I'm not sure what sort of universal property that has. Finally we apply the Chu construction, which is a right adjoint from csmc's with specified objects (or more generally "sub-unary polycategories") to *-autonomous categories (or more generally *-polycategories). So the envelope is a composite of left adjoints, right adjoints, and functors without any obvious adjoint.

Mike Shulman (Apr 22 2020 at 20:18):

However, we can use the envelope to show that the unit of the free-forgetful adjunction between closed symmetric monoidal categories and *-autonomous ones is also fully faithful. This is sometimes called a "full completeness" result. This is also in the paper: we use an idea of Lafont involving Artin gluing, combined with the double gluing construction for *-autonomous categories.

Mike Shulman (Apr 22 2020 at 20:20):

(Hmm, looks like maybe the 2-hour delay lost most of the audience? Sorry.)

Aleks Kissinger (Apr 22 2020 at 20:20):

i've got a question :)

Mike Shulman (Apr 22 2020 at 20:20):

Please!

Reid Barton (Apr 22 2020 at 20:20):

By the way, is this double gluing construction the same as the one that appears in your paper on Reedy model category structures?

Aleks Kissinger (Apr 22 2020 at 20:20):

(just finished you talk, in recorded form. thanks for the nice talk btw)

Aleks Kissinger (Apr 22 2020 at 20:22):

if you do this for some concrete category (people already discussed Set), does the co-tensor in the *-autonomous envelope tell you something, or is it just a purely formal thing?

Cole Comfort (Apr 22 2020 at 20:23):

I think someone previously asked what the envelope looks like for vector spaces over a field, I would be interested in knowing this.

Mike Shulman (Apr 22 2020 at 20:23):

@Reid Barton No, it's different.

Martti Karvonen (Apr 22 2020 at 20:23):

Mike Shulman said:

However, we can use the envelope to show that the unit of the free-forgetful adjunction between closed symmetric monoidal categories and *-autonomous ones is also fully faithful. This is sometimes called a "full completeness" result. This is also in the paper: we use an idea of Lafont involving Artin gluing, combined with the double gluing construction for *-autonomous categories.

How does one see that such an adjunction exists in the first place?

Aleks Kissinger (Apr 22 2020 at 20:25):

maybe "tell you something" is a bit vague. i guess what i'm getting at is the par is always hard to get some kind of "computational" interpretation for, so i'm wondering if there is some hope coming from doing your construction to familiar categories

Mike Shulman (Apr 22 2020 at 20:25):

Martti Karvonen said:

How does one see that such an adjunction exists in the first place?

By 2-categorical abstract nonsense. (-: Because closedness and *-autonomy involve contravariant operations, the 2-categories involved have to be restricted to have only invertible 2-cells. But then both are described by finitary 2-monads on $\mathrm{Cat}_g$ (the 2-category of categories, functors, and natural isomorphisms), and 2-monad theory implies that the forgetful functor between the categories of algebras and pseudomorphisms has a left biadjoint.

Rui Soares Barbosa (Apr 22 2020 at 20:25):

Mike Shulman said:

However, we can use the envelope to show that the unit of the free-forgetful adjunction between closed symmetric monoidal categories and *-autonomous ones is also fully faithful. This is sometimes called a "full completeness" result. This is also in the paper: we use an idea of Lafont involving Artin gluing, combined with the double gluing construction for *-autonomous categories.

Hi. Thanks for the really nice talk! Could you elaborate on this quoted point, please? Are your saying that you can use the envelope construction to show that another construction of a *autonomous category from a csmc (namely, the adjoint to the forgetful functor) is also an embedding? Could you give some brief outline of how this proof goes, please?

Mike Shulman (Apr 22 2020 at 20:28):

It sounds like a lot of people would like to see the the construction compiled out more concretely. First let's look at the two representable $\ast\mathcal{C}$-modules associated to an object $A\in \mathcal{C}$. We have $よ_A(\Gamma;\Delta) = \ast\mathcal{C}(\Gamma; \Delta,A)$ and ${}_Aよ(\Gamma;\Delta) = \ast\mathcal{C}(\Gamma,A; \Delta)$.

Martti Karvonen (Apr 22 2020 at 20:30):

Mike Shulman said:

Martti Karvonen said:

How does one see that such an adjunction exists in the first place?

By 2-categorical abstract nonsense. (-: Because closedness and *-autonomy involve contravariant operations, the 2-categories involved have to be restricted to have only invertible 2-cells. But then both are described by finitary 2-monads on $\mathrm{Cat}_g$ (the 2-category of categories, functors, and natural isomorphisms), and 2-monad theory implies that the forgetful functor between the categories of algebras and pseudomorphisms has a left biadjoint.

So the same reasoning should imply that there's a similar adjunction between closed SMCS and compact one's, right? It's just that the unit isn't full and faithful, unlike here.

Mike Shulman (Apr 22 2020 at 20:30):

Because of the definition of $\ast\mathcal{C}$, the homset $\ast\mathcal{C}(\Gamma;\Delta,A)$ is nonempty only when $\Gamma$ contains no formal duals and $\Delta$ consists entirely of formal duals, in which case we are just looking at morphisms into $A$ out of some tensor product of objects in $\mathcal{C}$. That is, $よ_A$ is essentially just the presheaf represented by $A$ on $\mathcal{C}$ as a multicategory.

Mike Shulman (Apr 22 2020 at 20:30):

(@Martti Karvonen Yes.)

Mike Shulman (Apr 22 2020 at 20:34):

On the other hand, the homset $\ast\mathcal{C}(\Gamma,A; \Delta)$ is nonempty only when $\Gamma,\Delta^*$ contains exactly one formal dual, say $B^*$, in which case it reduces to a homset $\mathcal{C}(\Phi,A ; B)$ in $\mathcal{C}$ as a multicategory. So ${}_Aよ$ is the "covariant representable at $A$ on $\mathcal{C}$ as a multicategory". And since $\mathcal{C}$ is closed, a morphism $\Phi \otimes A \to B$ is equivalently a morphism $A \to [\Phi,B]$. So just as $よ_A$ knows about morphisms with codomain $A$ and with domain decomposed as a tensor product, ${}_Aよ$ knows about morphisms with domain $A$ and with codomain decomposed as an iterated internal-hom.

Mike Shulman (Apr 22 2020 at 20:36):

The image of $A$ in the envelope consists of $よ_A$ and ${}_Aよ$ together with the obvious pairing between them. So intuitively, it consists of both "representable functors" at $A$, in a multi/poly-categorical sense. This is reminiscent of the https://ncatlab.org/nlab/show/Isbell+envelope (the reuse of the term "envelope" is presumably not a coincidence!) in which $A$ embeds via its ordinary pair of representable functors and the pairing between them.

Cody Roux (Apr 22 2020 at 20:37):

John Baez said:

I have a feeling Cody's comment is a response to some earlier stuff about Gentzen's proof, not Mike's latest comment! (I always make this sort of slip myself.)

Yes I forgot to quote your earlier comment, I'm embarrassed to say. Also when I started writing it, it was less high up, but then I got distracted by a phone call...

Mike Shulman (Apr 22 2020 at 20:41):

A general object of the envelope of a polycategory $\mathcal{P}$ consists of a pair of modules $M^+,M^-$ and a pairing $(M^+,M^-) \to \mathcal{P}$. I like to think of the sets $M^+(A_1,\dots,A_m;B_1,\dots,B_n)$ as encoding all the ways to "produce $M$" while consuming some specified inputs $A_i$ and parallely producing some other specified outputs $B_j$, and similarly $M^-$ encodes all the ways to "consume $M$". For the representable pair $(よ_A, {}_Aよ)$, we interpret "producing" and "consuming" in the obvious way in $\mathcal{P}$ itself.

Mike Shulman (Apr 22 2020 at 20:42):

The pairing $(M^+,M^-)\to\mathcal{P}$ tells you what happens if you "produce $M$" and then "consume" what was produced.

Mike Shulman (Apr 22 2020 at 20:45):

Saying that $M$ respects the tensor in $\mathcal{P}$ says that when producing or consuming $M$, having an input of $A\boxtimes B$ is the same as having two inputs of $A$ and $B$, and similarly for the cotensor. In particular, saying that $M$ respects the formal cotensors $[A,B] = A^* ⅋ B$ in $\ast\mathcal{C}$ says that when producing or consuming $M$, having an output of $[A,B]$ is the same as having an input of $A$ and an output of $B$.

Mike Shulman (Apr 22 2020 at 20:46):

(I'm building up to trying to answer @Aleks Kissinger 's question about cotensors in the envelope here.)

Mike Shulman (Apr 22 2020 at 20:47):

The formula for cotensors in a Chu construction is $(M^+,M^-) ⅋ (N^+,N^-) = ([M^-,N^+] \times_{[M^-\otimes N^-,d]} [N^-,M^+] , M^- \otimes N^-)$.

Aleks Kissinger (Apr 22 2020 at 20:52):

(....digesting....)

Mike Shulman (Apr 22 2020 at 20:52):

If we compile that out for modules, using the definitions of the internal-hom for modules (which I didn't mention in the talk), we see that to produce $(M^+,M^-)⅋(N^+,N^-)$ using inputs $\Gamma$ and outputs $\Delta$, we have to give, for every way of consuming $M$ using inputs $\Phi$ and outputs $\Psi$, a way of producing $N$ using inputs $\Phi,\Gamma$ and outputs $\Delta,\Psi$, and dually, that are natural and compatible.

Mike Shulman (Apr 22 2020 at 20:54):

This is quite a mouthful, but I think it has a sort of dialoguey flavor: we're trying to produce $M$ and $N$ in "parallel", so whenever in the $M$-thread we encounter a "user" who claims to be able to consume an $M$, we can turn around and use that consumption as a way to produce an $N$ for any user of the $N$-thread. Of course that much is true in any Chu construction; Hyland's envelope enhances it by carrying around the inputs and outputs.

Aleks Kissinger (Apr 22 2020 at 20:56):

i guess you can say the same thing about representables, replacing "producing/consuming M/N" with objects in the category we started with?

Mike Shulman (Apr 22 2020 at 20:58):

Exactly, But I believe it's not very interesting when applied to representables $(よ_A,{}_A よ)$ in the envelope of $\ast \mathcal{C}$. Because the only way to consume the representable at $A$ is to have an output object, say $X$, and a morphism $A\to X$. But there is no way in $\ast\mathcal{C}$ to produce the representable at $B$ that also has another output object $X$. So it seems that there is no way of producing $(よ_A,{}_A よ) ⅋ (よ_B,{}_B よ)$. I'm not sure whether that's exactly right, but I do remember from the last time I thought about it that ⅋s of representables were not very interesting.

Mike Shulman (Apr 22 2020 at 21:00):

However, it seems that there are nontrivial ways to consume ⅋s of representables as long as we are willing to produce multiple outputs, say $X$ and $Y$, by giving a pair of morphisms $A\to X$ and $B\to Y$ (or vice versa). (This uses the tensor product of modules, which again I didn't describe in the talk.) This sort of makes sense to me if I think of $\mathcal{C}$ as a "sequential language" that's being "imported" into a world with parallelism.

Nathanael Arkor (Apr 22 2020 at 21:03):

What was the original inspiration for this development, if you don't mind my asking a soft question? Was the motivation originally string diagrams, or had you spotted that Hyland's construction could be modified in this way beforehand, or something else entirely?

Mike Shulman (Apr 22 2020 at 21:07):

And now to come back to an earlier question:
Rui Soares Barbosa said:

Are you saying that you can use the envelope construction to show that another construction of a *autonomous category from a csmc (namely, the adjoint to the forgetful functor) is also an embedding? Could you give some brief outline of how this proof goes, please?

Yes, that's right. Since $\mathrm{Env}_{\mathcal{C}}$ is *-autonomous, the embedding $\mathcal{C} \hookrightarrow \mathrm{Env}_{\mathcal{C}}$ factors through the free *-autonomous category $\mathcal{D}$ generated by $\mathcal{C}$. Now we do a version of Artin gluing along this induced functor of *-autonomous categories, and show that the functor from $\mathcal{C}$ to $\mathcal{D}$ lifts to the gluing category. Therefore, the universal property of $\mathcal{D}$ gives a section of the projection from the gluing category, from which we can extract full-faithfulness of the map $\mathcal{C}\to\mathcal{D}$. This general idea of using gluing is due to Lafont (perhaps in an unpublished thesis?), and was applied to "double gluing" for *-autonomous categories by Hyland-Schalk and Hassei.

Mike Shulman (Apr 22 2020 at 21:09):

@Nathanael Arkor Personally, my original motivation was actually string diagrams! I asked a MathOverflow question https://mathoverflow.net/q/343167/49 about embeding csmc's in *-autonomous categories and didn't get any answers, and started thinking about how to do it.

Mike Shulman (Apr 22 2020 at 21:12):

In fact I was motivated by one particular kind of "string diagram", the "sharing graphs" used in "optimal evaluations" for lambda-calculus, which are closely related to linear logic and *-autonomous categories. I wanted to know whether they could be interpreted semantically in some *-autonomous category that would directly yield results about the original lambda-calculus for CCCs. (I asked about this too at CStheory SE https://cstheory.stackexchange.com/q/45628/28847.) Unfortunately this result isn't enough for what I really wanted, which is for each step of the sharing-graph evaluation to have a semantic meaning: in addition to involving the exponentials , these graph manipulations seem to produce things that are not even proof nets, so there is still something to understand better there.

Mike Shulman (Apr 22 2020 at 21:13):

But I think having a nice string diagram calculus for csmc's should be useful in practice too.

Christian Williams (Apr 22 2020 at 21:15):

Absolutely. Exponentially more expressive than smc's.

Mike Stay (Apr 22 2020 at 21:20):

exponentially

I see what you did there! :D

Nathanael Arkor (Apr 22 2020 at 21:20):

That's really interesting, thank you! It would be beautiful to be able to describe these sorts of results about optimal evaluations entirely categorically.

Mike Shulman (Apr 22 2020 at 21:23):

I have to go to a department meeting in a few minutes, but feel free to ask further questions; I'll come back to this thread later.

John Baez (Apr 22 2020 at 22:06):

Thanks!

Mike Shulman (Apr 23 2020 at 03:24):

Actually, I have a question for you all. How did the handwritten "slides" compare to slides made with LaTeX/beamer? They were certainly much faster for me to make, especially with all the string diagram pictures, and if I'd had another hour to prepare I could easily have finished preparing them for the entire talk. Plus it was nice to be able to easily write on them during the talk for emphasis. So I'm tempted to go the same route in future e-seminars as well. But I wonder how the experience was for the audience?

sarahzrf (Apr 23 2020 at 03:29):

they were fairly nice

Alexander Kurz (Apr 23 2020 at 03:47):

I also liked your slides, Mike. In some ways the part were you drew them on the fly was even easier to follow ...

Todd Trimble (Apr 23 2020 at 03:51):

Your slides written on the fly worked well for me.

Mike Shulman (Apr 23 2020 at 04:09):

Yes, writing things on the fly has at least one notable benefit, namely that of slowing things down to the pace of writing. (-:

eric brunner (Apr 23 2020 at 04:31):

slowing you down is good. doodling and commenting is good too. i prefer to watch the strings draw themselves.

Aleks Kissinger (Apr 23 2020 at 08:23):

Mike Shulman said:

Actually, I have a question for you all. How did the handwritten "slides" compare to slides made with LaTeX/beamer?

I liked them too. It's a nice compromise between a whiteboard talk, where it becomes a bit tedious if the speaker needs to draw something fairly elaborate, and slides.

Aleks Kissinger (Apr 23 2020 at 08:34):

sarahzrf said:

so i made my own version https://github.com/sarahzrf/sequents

This is great!

Jules Hedges (Apr 23 2020 at 11:10):

@Mike Shulman I have a question on your question: What setup did you use to write directly onto Zoom while also having a webcam facing you? Was it PC + graphics tablet? (I did manage to mirror an iPad to a projector once, but it involved a lot of metaphorical string and duck tape)

Nathanael Arkor (Apr 23 2020 at 12:22):

I think that hand-written slides are typically better than beamer slides, especially written or annotated on the fly: I liked them.

Mike Shulman (Apr 23 2020 at 13:59):

Thanks for the feedback everyone. @Jules Hedges I used a Wacom One tablet, with the software xournal under ubuntu. I got the Wacom back when we were all preparing for remote teaching, and have liked it very much for my zoom lectures; my impression is that it works much better than an iPad/Android tablet.

Fabrizio Genovese (Apr 23 2020 at 14:18):

Mike Shulman said:

Actually, I have a question for you all. How did the handwritten "slides" compare to slides made with LaTeX/beamer? They were certainly much faster for me to make, especially with all the string diagram pictures, and if I'd had another hour to prepare I could easily have finished preparing them for the entire talk. Plus it was nice to be able to easily write on them during the talk for emphasis. So I'm tempted to go the same route in future e-seminars as well. But I wonder how the experience was for the audience?

Handwriting is much better than slides imho. Slides always taste like canned material for me, and make me super sleepy. Witnessing a process in real time is definitely more engaging.

Fabrizio Genovese (Apr 23 2020 at 14:19):

Mike Shulman said:

Thanks for the feedback everyone. Jules Hedges I used a Wacom One tablet, with the software xournal under ubuntu. I got the Wacom back when we were all preparing for remote teaching, and have liked it very much for my zoom lectures; my impression is that it works much better than an iPad/Android tablet.

A thing I recently set up consists in a webcam being placed above my desk, so you can see my hands and the surface. Then I just use a bunch of A3 paper and coloured markers to draw :D (I tried with a graphic tablet but it felt absolutely painful to use, so I resorted to more analog alternatives :P )

sarahzrf (Apr 23 2020 at 14:51):

Fabrizio Genovese said:

Mike Shulman said:

Actually, I have a question for you all. How did the handwritten "slides" compare to slides made with LaTeX/beamer? They were certainly much faster for me to make, especially with all the string diagram pictures, and if I'd had another hour to prepare I could easily have finished preparing them for the entire talk. Plus it was nice to be able to easily write on them during the talk for emphasis. So I'm tempted to go the same route in future e-seminars as well. But I wonder how the experience was for the audience?

Handwriting is much better than slides imho. Slides always taste like canned material for me, and make me super sleepy. Witnessing a process in real time is definitely more engaging.

hmm... maybe i should live-code for my talk then ;)

sarahzrf (Apr 23 2020 at 14:53):

/s

Fabrizio Genovese (Apr 23 2020 at 14:54):

Live coding is amazing! Btw we are livecoding on idris right now

John Baez (Apr 23 2020 at 18:21):

I liked the approach of writing as you talked, @Mike Shulman. It's the social-distancing version of the mathematician's old-style chalk talk, which I've always liked better than slides when done competently.

sarahzrf (Apr 23 2020 at 18:21):

there's the rub

John Baez (Apr 23 2020 at 18:22):

The only problem was that you seemed to be running out of time near the end, @Mike Shulman, and since you had to rush off there wasn't time for discussions out loud on Zoom. The written discussions here were great, but there's something fun (in my opinion) about hearing people talk about math.

Mike Shulman (Apr 23 2020 at 19:10):

@John Baez Thanks for the feedback! I would probably have done better time-wise if I'd had a chance to practice the talk in advance. And I was sad to have to rush off afterwards too.

Mike Shulman (Apr 23 2020 at 19:11):

By the way, I'm scheduled to talk in the MIT categories seminar in a few weeks, and trying to decide what to talk about. I suppose probably there is large overlap in the audiences for these two online seminars?

John Baez (Apr 23 2020 at 19:13):

I think there's a very large overlap, though I must sadly admit I only have the energy to attend the ACT@UCR one, so I haven't been in that overlap.

John Baez (Apr 23 2020 at 19:16):

Also, everything is recorded and put on YouTube, so everyone who wants to see your first talk will. For example, @Jules Hedges missed your talk but now he's excited about the video. So, you should probably only talk about the same thing if you plan to do better or highlight some other aspects.

I'm only 1/3 of the way through Mike Shulman's ACT@UCR seminar and my mind has already been extremely thoroughly blown by string diagrams for linearly distributive categories... I don't even know whether this is new or if it already existed and I missed it https://www.youtube.com/watch?v=5CjSu5hLtcw

- julesh (@_julesh_)

Mike Shulman (Apr 23 2020 at 19:46):

Well, I could certainly plan to do better; you can always do something better the second time around. But it probably wouldn't be that interesting to everyone who already saw or watched this talk if I just give a better version of it. However, there's a lot in the paper that I didn't even mention this time, so I might consider coming at it from a different direction. Thanks!

John Baez (Apr 23 2020 at 19:48):

Yes, I think doing something a bit new would be great. I think a lot of people (like me) loved your talk but didn't fully grasp all of it, so coming at the same material from a different angle would be interesting to a lot of us.

Simon Burton (Apr 23 2020 at 23:03):

@Mike Shulman At times during your talk it seemed like you were "pointing" at some notation on your slides, but I couldn't work out where you were pointing. Some times I could see a "pointing" dot, but sometimes not. I don't know if anyone else had this problem...

Mike Shulman (Apr 24 2020 at 02:00):

@Simon Burton Thanks for that feedback. I realized at the time that I was probably creating that issue, but didn't have the spare brainpower to solve it. The software I'm using doesn't have a "cursor" other than a tiny dot -- although perhaps that may be configurable, I can look into it. Of course one thing to do is to just circle or underline things, but when I was on the pre-prepared "slides" I somehow felt reluctant to do that; I'm not sure why. (-:

Mike Shulman (Apr 24 2020 at 02:02):

Speaking of software, what I would really like is a sketchpad/whiteboard program much like xournal, but augmented with beamer-like selective display features. That is, I'd like to be able to draw a slide by hand, then select part of it and say "hide this part first and display it on the second appearance" and so on, and then "compile" such a thing to a PDF for the presentation. I don't suppose anyone knows of such a piece of software?

Mike Shulman (Apr 24 2020 at 04:48):

Hmm, maybe I could get something like that with xournal's "layer" feature.

Aleks Kissinger (Apr 24 2020 at 10:52):

Mike Shulman said:

Speaking of software, what I would really like is a sketchpad/whiteboard program much like xournal, but augmented with beamer-like selective display features. That is, I'd like to be able to draw a slide by hand, then select part of it and say "hide this part first and display it on the second appearance" and so on, and then "compile" such a thing to a PDF for the presentation. I don't suppose anyone knows of such a piece of software?

I've achieved something like this with powerpoint, but its handwriting (aka "Windows Ink") support is a bit clunky and I prefer to stick in Linux during my workday.

Aleks Kissinger (Apr 24 2020 at 10:54):

What I end up doing in practice is duplicating a page lots of times when I'm done with it, and start erasing stuff off earlier pages. But this is very brittle if you want change something on the slide

Valeria de Paiva (Apr 24 2020 at 14:09):

Mike Shulman said:

The formula for cotensors in a Chu construction is $(M^+,M^-) ⅋ (N^+,N^-) = ([M^-,N^+] \times_{[M^-\otimes N^-,d]} [N^-,M^+] , M^- \otimes N^-)$.

Can I point out that this actually comes from Dialectica? the Chu version can get away with the trick of only considering co-extensional objects, so it does not need the pullback to be explicitly described.

Mike Shulman (Apr 24 2020 at 14:57):

I'm not sure what you mean. The Chu construction is not a special case of the Dialectica construction; as I explained in my paper comparing them, at the polycategorical level they're both instances of a general thing, but their representability conditions are different.

Valeria de Paiva (Apr 24 2020 at 17:01):

Mike Shulman said:

I'm not sure what you mean. The Chu construction is not a special case of the Dialectica construction; as I explained in my paper comparing them, at the polycategorical level they're both instances of a general thing, but their representability conditions are different.

Yes, of course the Chu construction is not a special case of the Dialectica construction. But as I wrote in the paper http://www.tac.mta.ca/tac/volumes/17/7/17-07.pdf individual constructions can be compared. the 'par' of the Chu construction is obtained by a pullback of the corresponding par in Dialectica in the first component. However, because Chu is more symmetric than Dialectica, you do not need to use the pullback in your message above, you can simply use the other component, as while Dialectica maps as (f,F) and they don't need to be the same, Chu maps are (f,f*) and one determines the other.

Mike Shulman (Apr 24 2020 at 17:34):

But if you're explaining the Chu construction to someone who doesn't already know about the Dialectica construction, saying that the Chu formula "actually" comes from (or more precisely, can be constructed from) the Dialectica construction is not, I think, helpful. (-:

Valeria de Paiva (Apr 24 2020 at 18:23):

Mike Shulman said:

But if you're explaining the Chu construction to someone who doesn't already know about the Dialectica construction, saying that the Chu formula "actually" comes from (or more precisely, can be constructed from) the Dialectica construction is not, I think, helpful. (-:

Well, I did enjoy the historic reconstruction of the Chu internal-hom!
Just watched your talk, very nice indeed! Many thanks! I have two complaints though:

1. why don't you say smcc (symmetric monoidal closed category) like all the old people?
2. You could/should have given the reference to Martin's envelope, right?
   More seriously, if I was giving a similar talk, I'd start from the logic and say that the reason I want to compute (string diagrams or not) with smccs is that they are the kernel of all intuitionistic-like logic systems. and there (because A* is the internal-hom into \bot, <A, \bot> , the natural iso A\times A--> \bot is obviously true, it's just evaluation. But the natural iso \top-->A\times A corresponds to some sort of Law of Excludded Middle (A or not A) which is very debatable!

Mike Shulman (Apr 24 2020 at 19:13):

1. Because I generally think of the monoidal structure as given first and closedness as a property of it. You can do it the other way of course, but I find that way easier to think about.

Mike Shulman (Apr 24 2020 at 19:15):

2. Yes, I forgot to write down the name of the paper in which Martin defined the envelope; IIRC it's "Proof theory in the abstract". I did attribute it to him though.

Mike Shulman (Apr 24 2020 at 19:17):

One can of course motivate things in many different ways. I think there are a lot of people who may care about using string diagrams to reason about csmcs (or smccs :smile:) but who aren't interesting in intuitionstic and/or linear logics at all. (Maybe they should be interested in those logics, but even if so, to convince them of that we have to start from where they are.)

Reid Barton (Apr 24 2020 at 21:15):

I have two questions related more broadly to the Chu construction:

1. The theory of model categories is self-dual. Is there some useful way to embed {model categories + Quillen adjunctions} in Chu(something) (similarly to how Adj embeds in Chu(Cat, Set))? Where "something" would be some flavor of "half a model category structure", e.g., a cofibration category?

Reid Barton (Apr 24 2020 at 21:29):

2. If $C$ and $D$ are locally presentable categories then they have a tensor product $C \otimes D$ which is the universal category equipped with a bivariate adjunction $C \times D \to C \otimes D$, and $C \otimes D$ can be constructed by the formula $C \otimes D = \mathrm{Hom}^{R}(C^{\mathrm{op}}, D)$ (where $\mathrm{Hom}^{R}(-, -)$ denotes the category of right adjoints). In this case $C^\mathrm{op}$ is almost never itself locally presentable, but it still formally appears to make sense to compute
   $C^\mathrm{op} \otimes D = \mathrm{Hom}^R(C, D) = \mathrm{Hom}^L(D, C)^\mathrm{op} = [D, C]^\mathrm{op}$
   where $[D, C] = \mathrm{Hom}^L(D, C)$ is the internal Hom, the category of left adjoints. On the other hand I could not find any use for $C^\mathrm{op} \otimes D^\mathrm{op}$.
   This feels similar to the formula for the tensor product in the Chu construction, but I don't see quite how they are related.

Reid Barton (Apr 24 2020 at 21:34):

One thing that always bugged me a bit is that the definition of a model category is self-dual, but in practice we can say a lot more about, for example, combinatorial model categories, and this condition breaks the symmetry. It might be nice to have a framework which restores the duality.

Reid Barton (Apr 24 2020 at 21:49):

Reid Barton said:

This feels similar to the formula for the tensor product in the Chu construction, but I don't see quite how they are related.

I guess we just identify $C$ with $(C, 0)$ and $C^\mathrm{op}$ with $(0, C)$ and then the formulas for $C \otimes D$ and $C^\mathrm{op} \otimes D$ work out correctly, and we get $C^\mathrm{op} \otimes D^\mathrm{op} = 0$. This last definition never occurred to me, probably because I did not imagine that the $-^\mathrm{op}$ duality should relate two different tensor products.

Mike Shulman (Apr 24 2020 at 23:10):

Regarding (2), things get much nicer if you drop down to posets where the local-presentability issues go away. Then you can say that the category Sup is $\ast$-autonomous, with an analogous tensor product that represents maps that preserve joins in each variable separately, and the duality $C^{\mathrm{op}}$ which isn't a problem since we dropped local presentability.

Mike Shulman (Apr 24 2020 at 23:20):

Thinking about this example, and how it fails to generalize from 0-categories to 1-categories due to annoying size issues, is what led me to the polycategory of multivariable adjunctions. The underlying polycategory of the $\ast$-autonomous category Sup is in fact a full sub-polycategory of $\mathrm{MAdj}_0$, the polycategory of posets and multivariable adjunctions. So $\mathrm{MAdj}_1$, the polycategory of 1-categories and multivariable adjunctions, is a natural replacement for the nonexistent $\ast$-autonomous analogue of Sup for 1-categories.

Mike Shulman (Apr 24 2020 at 23:34):

Now if a 2-variable functor between locally presentable categories is cocontinuous in each variable, it has both right adjoints by the adjoint functor theorem. Thus, the underlying multicategory of the monoidal category of locally presentable categories is a full sub-multicategory of the underlying multicategory of $\mathrm{MAdj}_1$ -- but, as you said, since locally presentable categories aren't closed under the duality of $\mathrm{MAdj}_1$, the multiple-codomain morphisms in the polycategory structure aren't visible to them.

Mike Shulman (Apr 25 2020 at 00:01):

On the other hand, $\mathrm{MAdj}_1$ embeds as a full sub-polycategory of $\mathrm{Chu}(\mathrm{Cat},\mathrm{Set})$, which is $\ast$-autonomous, and I think its structure comes close to reflecting the tensor product of locally presentable categories as you mentioned. The formula for the tensor product in a Chu construction is $(A^+,A^-)\boxtimes (B^+,B^-) = (A^+ \otimes B^+, [A^+,B^-] \times_{[A^-\otimes B^-, d]} [B^+,A^-])$. If we apply this to objects in the image of $\mathrm{Adj}\hookrightarrow \mathrm{Chu}(\mathrm{Cat},\mathrm{Set})$, i.e. of the form $(C^{\mathrm{op}},C)$, we get $(C^{\mathrm{op}}\times D^{\mathrm{op}}, [C^{\mathrm{op}},D] \times_{[C^{\mathrm{op}}\times D^{\mathrm{op}},\mathrm{Set}]} [D^{\mathrm{op}},C])$. And the second component of this is just $\mathrm{Hom}^R(C^{\mathrm{op}},D)$ -- but the first component is not $\mathrm{Hom}^R(C^{\mathrm{op}},D)^{\mathrm{op}}$. So it feels like the monoidal structure on locally presentable categories should be some kind of (co)reflection of this, but I'm not sure off the top of my head exactly how.

Mike Shulman (Apr 25 2020 at 00:09):

That was a long answer to question (2). I wish I had as much to say about question (1), which sounds like an interesting idea. To start with, there should be an analogue of the polycategory $\mathrm{MAdj}$ in which the categories are equipped with wfs (or a pair of wfs, or full model structures) and the morphisms are multivariable wfs/Quillen adjunctions. But can we embed it in a Chu construction?

Reid Barton (Apr 25 2020 at 00:18):

The Hom(-, -) of a model category is a sort of right Quillen bifunctor--that's what the lifting properties say.

Reid Barton (Apr 25 2020 at 00:19):

Maybe to be safer we can take simplicial model categories, so that the Hom objects take values in a genuine model category, but we shouldn't really need this.

Mike Shulman (Apr 25 2020 at 00:23):

Yeah, anything that works should probably work for ordinary model categories with a set-valued homfunctor and relating to the wfs (mono,epi) on Set. However, I don't see yet how to make anything work: how does the functor $C^{\mathrm{op}}\times C \to \mathrm{Set}$ encode the lifting properties by combining some structures on $C$ and $C^{\mathrm{op}}$ and mapping that structure to (mono,epI) in Set? The pullback corner that appears in the lifting property is a pullback in Set, and I don't see how to make that happen.

Reid Barton (Apr 25 2020 at 00:34):

Well, you could regard Hom as taking values in Set^op, or more specifically the opposite of the structure with (C = monos, AF = epis, AC = isos, F = all). The problem though is that you would need to put the structure of both wfses into the original category that we apply the Chu construction to, so it doesn't seem to gain very much.

Mike Shulman (Apr 25 2020 at 00:36):

I don't see how to make it work even if we do that. Do you?

Reid Barton (Apr 25 2020 at 00:39):

Start with VMod = V-enriched model categories and left Quillen functors, and embed VMod in Chu(VMod, V^op) via $C$ maps to $(C, C^{\mathrm{op}}, \mathrm{Map} : C \otimes C^{\mathrm{op}} \to V^{\mathrm{op}})$

Reid Barton (Apr 25 2020 at 00:40):

Perhaps I should write $\mathrm{Map}^{\mathrm{op}}$

Reid Barton (Apr 25 2020 at 00:41):

where $\otimes$ is just notation for a multimorphism of V-model categories

Mike Shulman (Apr 25 2020 at 00:42):

How can $\otimes$ be "just notation for" a morphism?

Mike Shulman (Apr 25 2020 at 00:43):

What is the closed symmetric monoidal structure on VMod?

Reid Barton (Apr 25 2020 at 00:44):

Sorry, I mean $F : C \otimes D \to E$ is just notation for a multimorphism $F \in \mathrm{VMod}(C, D; E)$.

Reid Barton (Apr 25 2020 at 00:44):

i.e. a Quillen V-bifunctor or whatever order the adjectives go in.

Reid Barton (Apr 25 2020 at 00:46):

I think VMod is usually not a closed symmetric monoidal category but I assume it's also okay to start with a multicategory--does it need to be more than that?

Reid Barton (Apr 25 2020 at 00:46):

A polycategory?

Mike Shulman (Apr 25 2020 at 00:49):

Yes, you can do the Chu construction to a multicategory, but you'll only get a polycategory out rather than a $\ast$-autonomous category. So it's unclear that we'd be gaining very much that way versus just directly defining a polycategory of model categories.

Reid Barton (Apr 25 2020 at 00:50):

Particularly as I needed to define the whole multicategory VMod first before even applying the Chu construction. :upside_down:

Valeria de Paiva (Apr 25 2020 at 00:51):

(deleted)

Mike Shulman (Apr 25 2020 at 01:08):

Yeah -- I was hoping that the lifting properties could be encoded somehow in the "pairings" appearing in the Chu construction, which would have made it more nontrivial. But as I said, I don't see how.

Reid Barton (Apr 25 2020 at 01:16):

Well, they are encoded in the fact that the pairing is a Quillen V-bifunctor. If you have a cofibration in C and a cofibration in C^op (i.e. a fibration in C) and you pair them, you get a cofibration in V^op (i.e. a fibration in V) which is acyclic if one of the original ones is--then you can lift the (cofibrant) unit of V into this acyclic fibration of V to produce lifts for squares in C.

Reid Barton (Apr 25 2020 at 01:17):

The problem is to "unencode" it from the original data.

Reid Barton (Apr 25 2020 at 01:26):

For example, suppose I define a "left V-semimodel category" to be a V-cocomplete V-category (or V-module category) with a class of weak equivalences that satisfies 2-out-of-3 and any old class of cofibrations. Let's look for V-categories M equipped with three classes (C, W, F) such that (M, W, C) and (M^op, W^op, F^op) are left V-semimodel categories and Map^op is a Quillen V-bifunctor (defined using cofibrations and acyclic cofibrations).

Reid Barton (Apr 25 2020 at 01:26):

Then I claim the pairing tells me I have lifts.

Reid Barton (Apr 25 2020 at 01:26):

However, I totally lost the factorizations.

Reid Barton (Apr 25 2020 at 01:37):

Maybe an algebraic WFS would fare better? It's easier to imagine having half of one of those.

Mike Shulman (Apr 25 2020 at 02:43):

Yes of course, what I meant was to encode them in a notion of morphism in a category, not morphism in a multicategory.

Mike Shulman (Apr 25 2020 at 03:46):

I think I've got it! But I'm not sure how well I can explain it in the rudimentary TeX available here. Maybe I'll make it a blog post or something.

Mike Shulman (Apr 25 2020 at 03:47):

(Where "it" = a Chu construction of a closed symmetric monoidal category that contains model categories and Quillen multifunctors as a full sub-polycategory. The objects of the Chu construction have a generalized form of lifting, but not factorizations or weak equivalences.)

Aleks Kissinger (Apr 26 2020 at 13:51):

Mike Shulman said:

Speaking of software, what I would really like is a sketchpad/whiteboard program much like xournal, but augmented with beamer-like selective display features. That is, I'd like to be able to draw a slide by hand, then select part of it and say "hide this part first and display it on the second appearance" and so on, and then "compile" such a thing to a PDF for the presentation. I don't suppose anyone knows of such a piece of software?

I came across Xournal++ today (https://github.com/xournalpp/xournalpp), which after messing with it for a bit seems to be much-improved over Xournal (and is being actively developed, unlike the latter). It seems to have reasonable layer support and a scripting/plugin interface, so maybe this is hackable into a nice platform for presentations.

Mike Shulman (Apr 26 2020 at 14:12):

Coincidentally I was just experimenting with xournal++ yesterday. I like its added features, but unfortunately it seems rather buggy. For instance, at least in the linux version, if more than one layer is displayed, then the selection tool doesn't work on objects in the top layer, but it does allow you to select objects in the bottom layer with the effect of duplicating them into the top layer. Also It crashes frequently.

Mike Shulman (Apr 26 2020 at 14:14):

Original xournal also has some bugs I've found, but none as annoying / dangerous as total crashes. Sometimes it loses its ability to get pen input correctly until a restart, but I can still save my work and quit normally.

Fabrizio Genovese (Apr 26 2020 at 14:29):

How do you guys deal with wacom tablets + ubuntu? I tried to configure mine but basically my wacom tablet is treated as a pointer, with absolute positioning. Clearly the writing experience is nightmarish in this way

Fabrizio Genovese (Apr 26 2020 at 14:30):

As i mentioned before, I then opted to have a webcam pointed at my desk surface. Still, I'd be happy to have a decent way to draw with a graphic tablet :slight_smile:

Mike Shulman (Apr 26 2020 at 14:46):

Sorry, what do you mean by "absolute positioning"?

Mike Shulman (Apr 26 2020 at 14:50):

My wacom tablet acts as a display too, so I just touch on the display where I want to write and it shows up under my pen. I haven't tried using one that isn't also a display; I think I would have a lot of trouble writing on one surface but only seeing what I'm writing appear on a totally separate screen.

Mike Shulman (Apr 26 2020 at 14:51):

But I know a couple of people who are doing it without a problem, so YMMV (and I haven't tried, so maybe it would work fine for me too).

Fabrizio Genovese (Apr 26 2020 at 14:52):

I mean that there is a bijective function between the surface of the screen and the surface of the tablet. So if i put my pen, say, at the extreme top left corner, that's where my mouse ends up being. Instead, I'd like a bijective mapping between the surface of my tablet and a window on my screen, which would allow me to use all the available space on the tablet to draw

Fabrizio Genovese (Apr 26 2020 at 14:53):

Mike Shulman said:

My wacom tablet acts as a display too, so I just touch on the display where I want to write and it shows up under my pen. I haven't tried using one that isn't also a display; I think I would have a lot of trouble writing on one surface but only seeing what I'm writing appear on a totally separate screen.

This is a huge plus. I'm considering the idea of buying a remarkable mainly for this

Mike Shulman (Apr 26 2020 at 15:38):

Ah. Well, just maximize the window. (-:

Mike Shulman (Apr 27 2020 at 23:19):

Mike Shulman said:

(Where "it" = a Chu construction of a closed symmetric monoidal category that contains model categories and Quillen multifunctors as a full sub-polycategory. The objects of the Chu construction have a generalized form of lifting, but not factorizations or weak equivalences.)

Here it is: https://golem.ph.utexas.edu/category/2020/04/model_categories_as_a_chu_cons.html

Paolo Perrone (Jun 04 2020 at 13:27):

John Baez said:

According to Paolo Perrone YouTube allows this when your channel has at least 1000 subscribers.

Hey guys, I discovered that this limit exists only if you stream from your phone or tablet. If you use a laptop, there is no limit! :)

John Baez (Jun 04 2020 at 16:28):

Oh, cool!

Paolo Perrone (Jan 26 2021 at 15:39):

I come somewhat late for this talk, but here is a question, if anyone is still there: how would you represent this nested internal hom, $[[X,Y],[A,B]]$, using Mike's string diagrams? Somehow I'm struggling.

John Baez (Jan 26 2021 at 16:02):

Ask @Mike Shulman!

Mike Shulman (Jan 26 2021 at 17:38):

In a $\ast$-autonomous category, $[[X,Y],[A,B]] \cong (X \otimes Y^*) ⅋ (A^* ⅋ B)$. So this would be represented by four strings labeled $X,Y,A,B$, with the middle two strings pointing up and the outer two strings pointing down.

Mike Shulman (Jan 26 2021 at 17:41):

Of course that alone doesn't have enough information to distinguish it from, say, $X ⅋ (Y^* \otimes A^*) ⅋ B$ or any other way of putting together the objects. Relatedly, it's also not a valid complete $\ast$-autonomous string diagram (i.e. it doesn't represent the identity morphism of $[[X,Y],[A,B]]$), because for such a thing all the strings coming in at the top have to be $\otimes$'ed together and those coming out the bottom have to be ⅋'ed together. Whenever such a configuration of four strings occurs inside a valid complete string diagram, the algorithm for checking validity will automatically tell you how the strings are to be combined with the two tensor products.

Paolo Perrone (Jan 26 2021 at 18:07):

I see, thank you. But if I understood your talk correctly, while there are many ways of interpreting that string diagram in a *-autonomous category, there's only one way to make sense of that in a closed category, is that correct?