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: adjunctions between functors into Cat

Nathaniel Virgo (Apr 28 2024 at 06:54):

A common situation (it seems to me) is that you have functors $F:\mathcal{C}^{op}\to\mathbf{Cat}$ and $G:\mathcal{C}\to\mathbf{Cat}$ such that (i) $F(X) = G(X)$ for each object $X$ in $\mathcal{C}$ and (ii) for each morphism $f:X\to Y$ in $\mathcal{C}$, $F(f)$ is left adjoint to $G(f)$. (Perhaps there should be some kind of naturality condition here as well.) Often there are multiple functors of each type, forming a chain of adjoints.

What is this situation called, and where can I read about it? I feel like it would be productive to think about it from a fibred rather than an indexed perspective, but I'm having trouble wrapping my head around what the fibred version looks like. It seems like it should be a case of asking a functor $\mathcal{E}\to\mathcal{B}$ to have some property, but then when we have a chain of adjoints there must be more than one functor involved somehow.

As an example, let $\mathcal{C} = \mathbf{Set}$ and for a set $X$, let $F(X) = G(X) = H(X) = \mathcal{P}(X)$, the preorder of subsets of $X$, ordered by inclusion. Then for a function $f:X\to Y$, let

• $F(f): \mathcal{P}(X)\to \mathcal{P}(Y)$ map $S\subseteq X \mapsto \{y\in Y\mid \exists x\in S: f(x) = y\}$
• $G(f): \mathcal{P}(Y)\to \mathcal{P}(X)$ map $T\subseteq Y \mapsto \{x\in X\mid f(x)\in T\}$
• $H(f): \mathcal{P}(X)\to \mathcal{P}(Y)$ map $S\subseteq X \mapsto \{y\in Y\mid \forall x\in S: f(x) = y\}$.

Then we have a chain of adjoints $F(f)\dashv G(f) \dashv H(f)$. This kind of situation seems to be common whenever things have a "predicate-like" nature.

Notification Bot (Apr 28 2024 at 07:26):

This topic was moved here from #learning: questions > Adjunction between fibration and opfibration by Nathaniel Virgo.

Dylan Braithwaite (Apr 28 2024 at 07:58):

There are lots of instances of this, typically under the name of "quantifiers as adjoints", or "adjoints to change of base functors". Typically instead of starting with two indexed categories you have one, and you just ask that its reindexing functors each have adjoints.

I like the exposition of this in Sheaves in Geometry and Logic (section 1.9), although it doesn't specifically mention indexed categories or fibrations but works specifically in the case of the subobjects and slice categories. And I think Jacobs book on categorical logic uses this fact to define when a fibration (viewed as a model of type theory) models quantifiers.

The basic idea is if you think of the base category of a fibration as a category of variable contexts for a logic/type theory, and you have projection maps that "throw away variables", $p : A \times B \to A$ then the reindexing functor you get from the indexed category $F(p) : F(A) \to F(A\times B)$ implements the weakening rule from type theory: it maps terms with a free variable of type A to terms with free variables of type A and B (i.e. where B is in its list of free variables but doesn't actually get used).

Now if this functor has a left adjoint $\Sigma : F(A \times B) \to F(A)$ this behaves like existential quantification or dependent-sum type formation: it takes a term with free variables of types A and B, and removes B from its list of free variables by binding it in a quantifier.

Similarly a right adjoint behaves like universal quantification, or dependent product types

Nathaniel Virgo (Apr 28 2024 at 09:23):

It seems kind of strange to me to take such an asymmetric perspective - is there a reason for it?

It seems to me that all those adjoint reindexing functors ought to organise into an opfibration, so we're really looking at a functor that's a fibration and an opfibration at the same time, in a certain way. I guess I'm sort of hopeful that someone knows the right way to think about it from that perspective.

Dylan Braithwaite (Apr 28 2024 at 09:53):

Nathaniel Virgo said:

It seems to me that all those adjoint reindexing functors ought to organise into an opfibration, so we're really looking at a functor that's a fibration and an opfibration at the same time, in a certain way. I guess I'm sort of hopeful that someone knows the right way to think about it from that perspective.

Ah I see. Yeah, I think having all such adjoints is equivalent to having a [[bifibration]], or if you want both left and right adjoints, a [[trifibration]].

Nathaniel Virgo (Apr 28 2024 at 10:19):

Great, that looks like exactly what I'm looking for.