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: learning: questions

Topic: (Locally) internal categories and internal logic

Chris Grossack (they/them) (Apr 07 2024 at 21:36):

Say we're interested in the category of groups in a topos $\mathcal{E}$ . Moreover, say we have access to a universe $\mathcal{U}$ . Then there's two things we can do:

We can look at the indexed category $\mathsf{Grp}_\mathcal{E}$ with $\mathsf{Grp}_\mathcal{E}^X = \mathsf{Grp}(\mathcal{E}/X)$ of group objects internal to $\mathcal{E}/X$ .
We can look at the internal category in $\mathcal{E}$ carried by a type $\mathtt{Grp}$ that looks like $\sum_{G : \mathcal{U}} \ulcorner G \text{ is a group} \urcorner$

Is there a way to relate (internal) theorems proven in the type theory of $\mathcal{E}$ about (2) to (external) theorems about the indexed category in (1)? I suspect this has something to do with "Stack Semantics", but I can't find anything concrete written in any of the usual references (or, indeed, after looking through unusual ones). I'm hoping we can use the universe to sidestep this and work with the usual internal logic instead, but of course I'm also interested in a direct stack-logic-y way to understand things if that machinery exists.

Chris Grossack (they/them) (Apr 07 2024 at 21:38):

Of course, I'm interested in more things than just groups, so I would love to hear how this story works more generally for (infinitary, essentially) algebraic theories $\mathbb{T}$ . I'm currently less interested personally in "internal algebraic theories", but if the answer is best phrased in that language I'm happy to work in that generality too

Chris Grossack (they/them) (Apr 07 2024 at 21:52):

And, of course, what I'm really interested in is locales in $\mathcal{E}$ .

El Mehdi Cherradi (Apr 09 2024 at 11:14):

I don't know if this is completely relevant, but I don't expect anything else than Yoneda to relate internal theorems to external ones. $\mathsf{Grp}_\mathcal{E}$ and $\mathtt{Grp}$ should induce the same category representably provided $\mathcal{U}$ classifies propositions. I believe this should hold for any projectively sketch-able theory.

Mike Shulman (Apr 09 2024 at 12:22):

There are two differences. The first is that (at least if by "topos" you mean "1-topos"), $\mathtt{Grp}$ has a notion of equality of objects, albeit an accidental one, while $\mathsf{Grp}_{\mathcal{E}}$ may technically have one but it is easier to ignore. But if your theorems about group theory are proven in a dependently typed language that has no notion of equality of sets/types/groups, then this difference is invisible.

Mike Shulman (Apr 09 2024 at 12:22):

The second difference is that $\mathtt{Grp}$ doesn't classify all group objects, only some collection of "small" ones.

Chris Grossack (they/them) (Apr 10 2024 at 06:26):

Thanks @El Mehdi Cherradi and @Mike Shulman for taking a look at this! What I'm really interested in is whether there's a mechanical way to take a theorem about the "category of groups" internal to a (1-)topos $\mathcal{E}$ and learn a theorem about the external category of group objects in $\mathcal{E}$ .

For instance, if we can constructively prove the category of groups is complete, that tells us something about the (internal) category of groups in $\mathcal{E}$ . Is there a mechanical way to externalize this to conclude that the (external) category of group objects in $\mathcal{E}$ is complete? My strategy was to write this as some kind of global sections of a stack, but maybe there's a better way

Mike Shulman (Apr 10 2024 at 06:59):

The issue you run into is size. Your theorem about the category of groups internal to E only talks about the collection of group objects that belong (fiberwise) to the fixed universe. And it presumably also uses "complete" to mean having limits indexed by other objects in that universe.

Mike Shulman (Apr 10 2024 at 07:00):

If your topos has "enough universes", so that every object belongs to some universe, and your theorem is "universe-polymorphic", then you could expect to get an external theorem about all group objects. But I don't think this is written down anywhere.