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: topos theory

Topic: Freely Adjoining A Subobject Classifier


view this post on Zulip Chris Grossack (they/them) (Jul 15 2023 at 02:34):

If I understand correctly, the elementary topoi are algebras for a 2-monad on Cat (enriched in groupoids, for technical reasons). This is basically because an elementary topos is a category with ~bonus structure~ (finite limits, cartesian closed, and a subobject classifier) in much the same way that rings are algebras for a monad on Set, since a ring is a set with ~bonus structure~ (0,1,sums,products).

Then there is a forgetful functor from elementary topoi to finitely complete cartesian closed categories (forget the subobject classifier), which by abstract nonsense must have a left biadjoint (freely add a subobject classifier).

Does anyone know if this biadjoint has been studied? For instance, do we know which elementary topoi are free in this sense? I have to imagine the biadjoint is difficult to describe explicitly, which probably makes it quite hard to study. But I'd be excited to be proven wrong

view this post on Zulip John Baez (Jul 15 2023 at 09:44):

Hi! It's great to see you here! And now, before I make some comments: in case anyone thinks I'm being tough on Chris, I should mention that they're a grad student at UCR, we're friends, and we joke around a fair amount.

I'll just say a bit until the people who actually know topos theory show up.

Then there is a forgetful functor from elementary topoi to finitely complete cartesian closed categories (forget the subobject classifier), which by abstract nonsense must have a left biadjoint (freely add a subobject classifier).

Unless you used some sort of categorified adjoint functor theorem to prove this left biajdoint exists, I'm guessing this "must" is of the moral sort, i.e. it should happen, or else I will be sad:

view this post on Zulip John Baez (Jul 15 2023 at 09:45):

Anyway, it's a neat idea. If you take the finitely complete cartesian closed category of finite sets, FinSet\mathsf{FinSet}, and "freely throw in a subobject classifier", what are you expecting to get?

view this post on Zulip John Baez (Jul 15 2023 at 09:46):

Are you expecting to get FinSet\mathsf{FinSet}, with its usual subobject classifer, or some strange thing with a new subobject classifier?

view this post on Zulip John Baez (Jul 15 2023 at 10:17):

Another fun example to ponder is the 1-category Cat\mathsf{Cat} of small categories. This finitely complete and cartesian closed but has no subobject classifier. If we try to freely give it a subobject classifier, what happens?

(Or you could use FinCat\mathsf{FinCat} here.)

view this post on Zulip Matteo Capucci (he/him) (Jul 15 2023 at 11:40):

I'd expect having a subobject classifier to be property-like structure, since any two choice of s.c. are necessarily isomorphic up to unique iso

view this post on Zulip Matteo Capucci (he/him) (Jul 15 2023 at 11:40):

Hence if Chris' left biadjoint exists, then applying it to a topos like FinSet\sf FinSet should yield back something equivalent to it

view this post on Zulip John Baez (Jul 15 2023 at 11:58):

Perhaps! But one might falsely argue that since the presheaf category on a category is a way to [[freely cocomplete]] it, and being cocomplete is a property-like structure of a category, taking the category of presheaves on a category that's already cocomplete would give you back an equivalent category.

view this post on Zulip John Baez (Jul 15 2023 at 11:59):

It doesn't.

view this post on Zulip John Baez (Jul 15 2023 at 12:00):

The point, I guess, is that property-like structures on categories give pseudomonads on Cat that are laxly idempotent:

view this post on Zulip Mike Shulman (Jul 15 2023 at 15:23):

Right, property-like structure doesn't make the completion idempotent; only mere properties do that.

view this post on Zulip Mike Shulman (Jul 15 2023 at 15:25):

Another thing to note is that there isn't really a good notion of "cartesian closed natural transformation" that isn't invertible, since cartesian closure involves a mixed-variance operation. So "the 2-category of cartesian closed categories" is probably only a (2,1)-category, and the same for that of elementary toposes. (Chris mentioned this already, but I wanted to emphasize it.)

view this post on Zulip Mike Shulman (Jul 15 2023 at 15:29):

I think the existence of adjoints like this has been studied more in the 1-categorical case, where the categories have structure specified up to equality rather than isomorphism and the morphisms have to preserve them on the nose. E.g. there is Lambek's theorem that the 1-category of elementary toposes is monadic over that of categories. Perhaps one can apply abstract 2-monad theory nonsense to try to boost this up to the 2-category.

view this post on Zulip Mike Shulman (Jul 15 2023 at 15:30):

As you say, I doubt there is any explicit description of the toposes you get. They might be related to the [[free topos]] however.

view this post on Zulip Chris Grossack (they/them) (Jul 15 2023 at 15:38):

Mike Shulman said:

I think the existence of adjoints like this has been studied more in the 1-categorical case, where the categories have structure specified up to equality rather than isomorphism and the morphisms have to preserve them on the nose. E.g. there is Lambek's theorem that the 1-category of elementary toposes is monadic over that of categories. Perhaps one can apply abstract 2-monad theory nonsense to try to boost this up to the 2-category.

Yeah, I haven't thought super hard about this, but I think if you want everything to be STRICT (there's a fixed choice of limit and the functors preserve this choice on the nose, etc) then elementary topoi should be locally finitely presentable in the Gpd-enriched sense (and maybe even the Cat-enriched sense, if you want to be this strict?). In this case, @John Baez, we have abstract nonsense saying that a (Gpd-enriched) left adjoint MUST exist. It's given by left kan extension just like in the usual case of essentially algebraic theories.

view this post on Zulip Chris Grossack (they/them) (Jul 15 2023 at 15:41):

This theory is beautiful, and solves lots of problems in 2-category theory.... the issue is that they're problems nobody cares about, because everything is too strict! And there's no getting around this -- we have theorems saying that the "right" 2-category of finite limit categories (for instance) is merely accessible, and is NOT LFP.

Of course, there's lots of theorems saying that this still morally works out, and we can pass from strict things to weak things in a fairly predictable way. See, for instance, Kelly and Blackwell's Two-Dimensional Monad Theory

view this post on Zulip Chris Grossack (they/them) (Jul 15 2023 at 15:42):

All this to say that I haven't worked out the details, but I'm confident that such a biadjoint does exist (in, as Mike emphasizes, the (2,1)-cateory case)

view this post on Zulip Chris Grossack (they/them) (Jul 15 2023 at 15:45):

John Baez said:

Anyway, it's a neat idea. If you take the finitely complete cartesian closed category of finite sets, FinSet\mathsf{FinSet}, and "freely throw in a subobject classifier", what are you expecting to get?

This is a great question, that I haven't thought about at all.... I might think about it later this afternoon, though, because I'd love to have an answer for you. I'll tell you this, though: It won't get it usual subobject classifier back!

After all, there are certainly cartesian closed maps from FinSet to a topos that don't preserve the subobject classifier. Such a map would still need to extend to a logical functor from the topos where we've freely adjoint a subobject classifier

view this post on Zulip Mike Shulman (Jul 15 2023 at 15:46):

I think "morally works out" is understating the case a bit. In many cases, the machinery of 2-monad theory allows us to pass very precisely from the "problems nobody cares about" to the ones that we do care about.

view this post on Zulip Chris Grossack (they/them) (Jul 15 2023 at 15:47):

I think John knows that, and he's just giving me a hard time bc he's been trying to get me on zulip for three years now :P

view this post on Zulip John Baez (Jul 15 2023 at 15:52):

I just figure it's good to push back a little when someone says something "must" be true, to see how good of a reason they can muster. Plus I wanted to greet you. :upside_down:

view this post on Zulip Leopold Schlicht (Jul 15 2023 at 17:30):

John Baez said:

they're a grad student at UCR

Chris is several people? :grinning_face_with_smiling_eyes:

view this post on Zulip Chris Grossack (they/them) (Jul 15 2023 at 19:07):

Leopold Schlicht said:

John Baez said:

they're a grad student at UCR

Chris is several people? :grinning_face_with_smiling_eyes:

I use they/them pronouns. I'm sure you meant this as a joke, but I'd appreciate it if you respected that

view this post on Zulip Leopold Schlicht (Jul 15 2023 at 19:30):

Oh, I thought it was just a funny typo! I'm not a native speaker -- didn't mean to offend them!

view this post on Zulip Chris Grossack (they/them) (Jul 15 2023 at 19:38):

Leopold Schlicht said:

Oh, I thought it was just a funny typo! I'm not a native speaker -- didn't mean to offend them!

No worries! It happens a lot ^_^

view this post on Zulip Morgan Rogers (he/him) (Jul 17 2023 at 09:34):

Chris Grossack (they/them) said:

I think John knows that, and he's just giving me a hard time bc he's been trying to get me on zulip for three years now :P

I'm glad I could contribute to getting you here!

view this post on Zulip Morgan Rogers (he/him) (Jul 17 2023 at 09:36):

Mike Shulman said:

Another thing to note is that there isn't really a good notion of "cartesian closed natural transformation" that isn't invertible, since cartesian closure involves a mixed-variance operation. So "the 2-category of cartesian closed categories" is probably only a (2,1)-category, and the same for that of elementary toposes. (Chris mentioned this already, but I wanted to emphasize it.)

Please can you help me understand this comment? Why would the natural transformations be constrained by properties of the categories involved?

view this post on Zulip Chris Grossack (they/them) (Jul 17 2023 at 15:26):

Morgan Rogers (he/him) said:

Please can you help me understand this comment? Why would the natural transformations be constrained by properties of the categories involved?

You can absolutely look at the 2-category of CCCs, CC-functors, and all natural transformations! The issue is that such a category has no chance of being '2-algebraic', in the sense of being 2-algebras for a 2-monad. As Mike said, this is basically because of the mixed-variance of exponentiation.

Concretely, if MM were a 2-monad on the 2-cateogry Cat\mathfrak{Cat}, it has to have an action on categories, functors, and natural transformations. Now look at the categories

the functors

and finally the unique natural transformation

We can explicitly compute what MM must do to the categories and functors involved (since its underlying 1-monad does exist) and one can show that there's no compatible place to send M(α)M(\alpha), so MM can't exist. In particular, it's the mixed variance of the action of [,][-,-] that causes the problem. On closer inspection of the argument, you realize you can sidestep it by only keeping the invertible 2-cells. (Note that our counterexample was just the smallest noninvertible 2-cell).

You can read more (but not much more, unfortunately) in section 6.2 of Blackwell and Kelly's Two Dimensional Monad Theory

view this post on Zulip Morgan Rogers (he/him) (Jul 17 2023 at 19:36):

Okay, let's do that! I find the language of the Blackwell and Kelly paper hard to follow since it relies on a bunch of previously established details, so explicit calculation would be good; that said, I note that B&K seem to talk about free monoidal closed categories, which might be less well behaved than CCCs? We'll see.

This message took some time to write, because the interaction between the products and exponentials means that you can't generate one structure and then the other, you really need to do both at once!

Suppose we are given a category C\mathcal{C}. Let's inductively define categories, as follows.

We have functors CkCkCk+1\mathcal{C}_k \to \mathcal{C}'_k \to \mathcal{C}_{k+1} given by sending objects to singleton towers (resp. lists), and I think one could prove that these are full and faithful, so that we can take a union of these categories to get the completion we're after. I haven't done this, it would be too much effort for this exercise!

The variance obstacle already rears its head in the construction of C0\mathcal{C}'_0. Applying it to 11, we get an N\N-indexed discrete category, while applying it to 22 we get a category whose objects can be identified with finite strings of bits, with morphisms determined by a funny alternating order. The induced functors take nn to the string of length nn on 00 or 11, respectively. And there is no morphism between these as soon as nn is greater than or equal to 22, hence no natural transformation!

On the other hand, once we get to C1\mathcal{C}_1, we have a morphism (00)(11)(0 \wedge 0) \to (1 \wedge 1) corresponding to the projection map (00,1)(1)(0 \wedge 0, 1) \to (1). But there are no maps (000)(111)(0 \wedge 0 \wedge 0) \to (1 \wedge 1 \wedge 1) (I think!)

view this post on Zulip Morgan Rogers (he/him) (Jul 17 2023 at 19:38):

Having written that I think I should have started with constructing products, since I'm missing the isomorphisms (XT)TX(T,T)(X \wedge T) \wedge T' \cong X \wedge (T,T'), but I think the variance obstacle is still clear enough.