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: community: general

Topic: indexing over a base

Morgan Rogers (he/him) (May 13 2020 at 10:00):

Matteo Capucci said:

Screenshot_20200513-092002_Drive.jpg

This is an instance of a general theme, that we can internalise set-indexed collections as being indexed by locally constant sheaves, which relativises over an arbitrary base toposes as "things which are in the image of the inverse image functor of a geometric morphism (perhaps up to some limited categorical constructions like finite colimits)".

Mike Shulman (May 13 2020 at 15:53):

Morgan Rogers said:

This is an instance of a general theme, that we can internalise set-indexed collections as being indexed by locally constant sheaves, which relativises over an arbitrary base toposes as "things which are in the image of the inverse image functor of a geometric morphism (perhaps up to some limited categorical constructions like finite colimits)".

That doesn't seem right to me. "Things which are in the image of the inverse image functor of a geometric morphism" is a description of constant sheaves, not locally constant ones, and I don't see how finite colimits fixes that.

Mike Shulman (May 13 2020 at 15:54):

For locally constant sheaves, don't you want to say something like "there exists an object of the base topos such that ..." in the internal logic of the non-base topos? (Which you can do by equipping that topos with a $\flat$ modality.)

Morgan Rogers (he/him) (May 13 2020 at 16:09):

Mike Shulman said:

That doesn't seem right to me. "Things which are in the image of the inverse image functor of a geometric morphism" is a description of constant sheaves, not locally constant ones, and I don't see how finite colimits fixes that.

Hmm indeed, the parenthetical was me realising that what I was saying wasn't quite a generalisation of the locally constant sheaves. Would you mind elaborating on the "flat modality" that you mentioned?

sarahzrf (May 13 2020 at 16:14):

it's the comonad of the unique geometric morphism to Set

sarahzrf (May 13 2020 at 16:14):

so it takes the global sections of an object and assembles them back into a constant sheaf

Morgan Rogers (he/him) (May 13 2020 at 16:15):

Oh okay! Do you always get enough indexing objects that way?

sarahzrf (May 13 2020 at 16:16):

no idea :sweat_smile: i was just answering a question i saw posted, dunno the context

Morgan Rogers (he/him) (May 13 2020 at 16:29):

I'm also now curious how far wrong I am in this context. The locally constant sheaves in that passage of Ingo's thesis come from a direct lifting of the local indexing that precedes it, but how much information is lost if we embed the locally constant indexing sheaves into constant ones and extend the morphisms by pullback? (I can draw a diagram if that's not sufficiently articulate)

Mike Shulman (May 14 2020 at 02:31):

Morgan Rogers said:

Oh okay! Do you always get enough indexing objects that way?

Well, I'm used to thinking about the case where the topos is connected, so that the constant-objects functor is an embedding and the comonad $\flat$ is idempotent. In that case you get all the objects of the base topos as the $\flat$-fixed objects. I guess as long as the topos is inhabited the base topos can be identified with the $\flat$-coalgebras even though $\flat$ isn't idempotent, so at least in the 1-topos case you can recover the entire base topos that way. Is that what you're asking about?

Morgan Rogers (he/him) (May 14 2020 at 10:52):

Mike Shulman said:

I guess as long as the topos is inhabited the base topos can be identified with the $\flat$-coalgebras even though $\flat$ isn't idempotent, so at least in the 1-topos case you can recover the entire base topos that way. Is that what you're asking about?

Over a general base the geometric morphism needn't be a geometric surjection, but let's stay over Set for arguments' sake.
$f: \mathcal{E} \leftrightarrows \mathbf{Set}$
The external 'objects coming from the base' are those in the image of $f^*$, whereas from @sarahzrf's description, those identified by the modal operator are those in the image of $f^$f_, which will be fewer objects in general, even if you can recover $\mathbf{Set}$ as the category of comonads, since $f^$f_ only returns the underlying objects of (co)free things. I wanted to know if that actually results in any loss of indexing objects, or where any misconceptions I'm displaying lie :upside_down:

Mike Shulman (May 14 2020 at 17:43):

Yes, by "the topos is inhabited" I meant the geometric morphism to the base is a surjection. The types of the form $\flat A$ will indeed be those in the image of $f^* f_*$, I was just saying that once you have $\flat$ in the type theory you can define internally what it means for a type to be a $\flat$-coalgebra and that recovers all the objects of the base topos (in the surjective case).

Mike Shulman (May 14 2020 at 17:43):

Although actually, probably an even better approach is to just use a type theory that directly represents the adjunction $f^* \dashv f_*$ with modal operators, with an explicit mode for "base-topos objects". That will work even in the non-surjective case.

sarahzrf (May 14 2020 at 17:44):

oh lol inhabited as in "inhabited object in the internal sense"?

Mike Shulman (May 14 2020 at 17:45):

Inhabited object of the category of toposes. In general an inhabited object is one whose map to the terminal object is a surjection.

Morgan Rogers (he/him) (May 15 2020 at 12:11):

It always seems to be you I ask this of, @Mike Shulman, but what's a good reference which examines the internal logic including this modal operator?

Mike Shulman (May 15 2020 at 16:08):

There aren't a lot yet, unfortunately. My paper https://arxiv.org/abs/1509.07584 studies the internal structure of modal operators like this (plus others), but doesn't discuss the semantics precisely. The paper https://arxiv.org/abs/1801.07664 uses a modal operator like this for a different specific purpose, and I think discusses the semantics a little more. For the general theory of modal operators and their semantics you can look at https://dlicata.wescreates.wesleyan.edu/pubs/lsr17multi/lsr17multi-ex.pdf, although that's only for the simply typed case so far (the dependently typed one is a work in progress).