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: subobject functor colax closed

Christian Williams (May 22 2020 at 18:47):

For a topos $\mathrm{T}$, the subobject functor $\mathscr{P}:= [-,\Omega]: \mathrm{T^{op}\to Pos}$ is lax cartesian, and this implies that it is lax closed: there's a canonical map $\mathscr{P}([A,B])\to [\mathscr{P}(A),\mathscr{P}(B)]$ given by currying of evaluation.

In the case of sets or presheaves, we can also go back: given a map $F:\mathscr{P}(A)\to \mathscr{P}(B)$, we can form the subobject $\{f:A\to B\; |\; \forall U\in \mathscr{P}(A).\; f_!(U)\subseteq F(U)\} \rightarrowtail [A,B]$ -- all maps which "respect" $F$. This gives that $\mathscr{P}$ is also "colax closed".

How can this "colaxor" be constructed in a general topos? I think it will always look basically like the one above.

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

Maybe you can use the Mitchell-Benabou language to write down that subobject in any topos, more or less like how you just did in Set.

Christian Williams (May 22 2020 at 18:53):

Thanks, that's just what I was about to say. That "set" formula might actually be right in general.

Christian Williams (May 22 2020 at 18:54):

For some reason I haven't yet gotten comfortable enough with Mitchell-Benabou to think "oh, I can just write it like this and it works".

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

You can probably say

$f_! (U) = \{b \in B | \exists a \in A . f(a) = b \}$

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

You never need to use the Mitchell-Benabou language to describe things; the whole point is that it just captures all the stuff you can already do in a topos. But sometimes it can be more convenient.

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

At the very least this would be a good excuse to learn more about the Mitchell-Benabou language and what you can and cannot say in it.

Christian Williams (May 22 2020 at 18:57):

Wait, why do I want to re-express $f_!(U)$? Can't we just reference that adjoint directly?

John Baez (May 22 2020 at 18:57):

Since you have a very specific thing you're trying to express, you'll be highly motivated to learn the precise limitations of the Mitchell-Benabou language!

Christian Williams (May 22 2020 at 18:57):

So yeah, you're suggesting that we can probably use that formula above as a guide for how to actually construct the map in a general topos.

John Baez (May 22 2020 at 18:58):

Yes, you can reference that adjoint directly, but if you're trying to work with it in the Mitchell-Benabou language, it's good to know how to express it in that language. It's like if you're talking about a dog in Spanish, it's good to know the Spanish word for "dog".

John Baez (May 22 2020 at 18:59):

I'm all for Spanglish but...

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

There are probably people here (maybe not right this second) who understand this stuff a lot better than me. But I found that Sheaves in Geometry and Logic and McLarty's Elementary Categories, Elementary Toposes have pretty user-friendly intros to the Mitchell-Benabou language. My own study of it was limited by not having anything I wanted to do with it!

Christian Williams (May 22 2020 at 19:02):

Yes, I just thought that $f_! = \exists_f$ was a part of the language.

Christian Williams (May 22 2020 at 19:02):

It's hard to find a canonical presentation of the language as a type theory. A somewhat relaxed explanation like in the Sheaves book doesn't make me feel secure in exactly what the language is.

John Baez (May 22 2020 at 19:02):

Oh-oh, you're turning into a logician! Nervous if you're not surrounded by a protective layer of symbols.

Christian Williams (May 22 2020 at 19:02):

I think the one in Borceux is a bit more thorough, but still not exactly what I might consider formal.

John Baez (May 22 2020 at 19:03):

Okay, I guess you want exactly what I don't. So take my recommendations and don't read those.

Christian Williams (May 22 2020 at 19:03):

If you haven't heard, we are now required to wear a protective layer of symbols when we go out.

John Baez (May 22 2020 at 19:04):

I should design some sort of face mask with mathematical symbols on it.

John Baez (May 22 2020 at 19:05):

Anyway, yeah, some sort of $\exists_f$ thing should be in the M-B language, though I'm still more comfortable with good old quantification over variables $\exists x \in X$.

John Baez (May 22 2020 at 19:06):

Yeah, I see Mac Lane and Moerdijk use just old-fashioned things like $\exists x \in X$ in their version of the M-B language.

John Baez (May 22 2020 at 19:06):

But it doesn't really matter ultimately, I bet.

John Baez (May 22 2020 at 19:06):

It must be just a choice of conventions.

Christian Williams (May 22 2020 at 19:08):

Yeah, so they have an example of using $\mathrm{Epi}(X,Y) = \{f\in Y^X\; |\; \forall y\in Y\; \exists x\in X\; f(x)=y\}$ to derive the "subobject of epimorphisms". I'll study that, and try to do the same for the "$f$ respects $F$" formula above.

Nathanael Arkor (May 22 2020 at 19:09):

John Baez said:

Anyway, yeah, some sort of $\exists_f$ thing should be in the M-B language, though I'm still more comfortable with good old quantification over variables $\exists x \in X$.

In MLTT, you quantify over variables with $\Sigma_{x : A}$, even though in the category theory the dependent sum is interpreted as $\Sigma_f$, so I'd imagine it's the same with the MB language. The language isn't meant to look exactly like the categorical structure, or you could just as well not use the language.

John Baez (May 22 2020 at 19:15):

Good, that was my impression! Christian is wanting to say "mi dog esta caliente", which is perfectly clear but not quite Spanish.

John Baez (May 22 2020 at 19:17):

(Now everyone sees the abuse my students need to put up with.)