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

Topic: Functor Comprehension

Max New (Feb 13 2024 at 17:55):

I've recently finished formalizing a theorem in cubical Agda which is very well-known but I don't know of a name for it:

Every profunctor, i.e., $P : C \to Psh(D)$ for which each $P(c)$ is representable, is naturally equivalent to the composition of a unique (up to iso) functor $F : C \to D$ with the Yoneda embedding.

I've been using the name "functor comprehension" for this as I see it as a very direct generalization of the principle of "function comprehension": every relation $P : X \to Pow(Y)$ for which each $P(x)$ is uniquely inhabited, is the graph of a unique function $f : X \to Y$.

However I noticed that @Mike Shulman called a different principle "functor comprehension" on his personal nlab which was somewhat recently copied to nlab: [[functor comprehension principle]]. This is the principle that every fully faithful eso functor has an inverse.

These principles are closely related certainly, e.g., they both require some kind of choice/univalence in the form I stated above and can each be used to prove the other. It seems to me that the former is much directly analogous to function comprehension. I've never heard "any injective surjective function has an inverse" referred to as function comprehension but perhaps it is as well.

I'm going to be adding this to the Agda cubical library soon so I thought I'd ask if y'all know of any existing names for either of these theorems, as in an Agda library we'll give them different names to distinguish them.

Jonas Frey (Feb 13 2024 at 18:28):

Maybe that would be a good thing to ask on the agda zulip/discord? In my experience category theorists don't see the point in naming such "obvious" facts.

Mike Shulman (Feb 13 2024 at 18:54):

If I remember correctly, in my introductory category theory course from Eugenia Cheng she called your theorem "parametrized representability". That is, it says that if you have a family of presheaves depending functorially on a parameter, and each of them is individually representable, then the representing objects also depend functorially on the same parameter.

Mike Shulman (Feb 13 2024 at 18:54):

I can certainly see the argument for calling it "functor comprehension".

Mike Shulman (Feb 13 2024 at 18:56):

The reasoning behind my use of "functor comprehension" goes by an extra step that maybe I didn't write out explicitly. Ordinary function comprehension says that any total functional relation is a function. If you take the tabulation of a relation, you get a span $A \leftarrow R \to B$, and it is total and functional precisely when the map $R\to A$ is injective and surjective. Thus, if injective+surjective implies invertible, we have $A\cong R$ and thus a function $A \xrightarrow{\cong} R \to B$.

Mike Shulman (Feb 13 2024 at 18:56):

So "every injective and surjective function is invertible" isn't exactly the usual statement of function comprehension, but it's equivalent to it.

Mike Shulman (Feb 13 2024 at 18:57):

Similarly, "eso+ff implies invertible" is equivalent to "every anafunctor is a functor".

Mike Shulman (Feb 13 2024 at 18:59):

I like this better as something to call "functor comprehension", among other reasons because it doesn't privilege one variance. Some functors arise by "comprehension" from a pointwise-representable functor $C \to \mathrm{Set}^{D^{\rm op}}$; others arise by comprehension from a pointwise-representable functor $C \to (\mathrm{Set}^D)^{\mathrm{op}}$; and still others arise by comprehension from an anafunctor that doesn't have just one variance.

Max New (Feb 13 2024 at 22:19):

Jonas Frey said:

Maybe that would be a good thing to ask on the agda zulip/discord? In my experience category theorists don't see the point in naming such "obvious" facts.

Yes I'm going to discuss it with the other people who work on the Agda cubical library at least

Max New (Feb 13 2024 at 22:37):

Mike Shulman said:

Similarly, "eso+ff implies invertible" is equivalent to "every anafunctor is a functor".

Gotcha, stated as "every anafunctor is a functor" it is more clearly a kind of functor comprehension.
The variance part is a bit arbitrary I guess but since functors $C \to D$ are the same as functors $C^{op} \to D^{op}$ I don't find it that bad. But there's probably not anything interesting to say.

And (maybe you're aware of this) I'll point out that eso+ff => invertible can be proven directly from the parameterized representability theorem because you can show that if $F : C \to D$ is ff+eso then the functor $F^{-1} : D \to Psh(C)$ defined by $F^{-1}d c = D(F c, d)$ is pointwise representable. If you then use parameterized representability you actually get an adjoint equivalence directly. In this version you would get a right adjoint equivalence, and if you did this all on $F^{op} : C^{op} \to D^{op}$ you would construct a left adjoint equivalence

Mike Shulman (Feb 13 2024 at 22:54):

Yes, I see your point.

Max New (Feb 27 2024 at 04:33):

I've updated the [[functor comprehension]] page based on this discussion

Mike Shulman (Feb 27 2024 at 05:35):

Nice, thanks!

Mike Shulman (Feb 27 2024 at 05:36):

I think the anafunctor version can also be formulated as a generalization of functions-to-powersets: An anafunctor $A\to B$ is equivalently a functor from $A$ to the category of cliques in $B$.

Max New (Feb 27 2024 at 05:43):

Very nice! I hadn't heard of [[cliques]] before. That also makes the relation to the profunctor version much clearer since all of the choices of a representing object form a clique.

Max New (Feb 27 2024 at 05:46):

Now I need to figure out if we should utilize the clique-based version in Agda

Max New (Feb 27 2024 at 05:55):

And I wonder if the profunctor version can probably be reformulated in a more Span-like way: view the profunctor as a two-sided discrete fibration $A \leftarrow P \rightarrow B$ and does representability correspond to the left projection being a fully faithful eso?

Max New (Feb 27 2024 at 06:03):

I see now that a lot of this is already on the anafunctor page: https://ncatlab.org/nlab/show/anafunctor#anafunctors_versus_representable_profunctors . I'll need to clean this up later

Mike Shulman (Feb 27 2024 at 06:24):

Max New said:

And I wonder if the profunctor version can probably be reformulated in a more Span-like way: view the profunctor as a two-sided discrete fibration $A \leftarrow P \rightarrow B$ and does representability correspond to the left projection being a fully faithful eso?

No, if you do that then the fiber of $P$ over $a\in A$ is all the elements of $P(a,b)$ for all $b$, not just the universal ones. I think what you can say is that the fibers of $P$ all have terminal objects, and if you restrict $P$ to the subcategory of objects that are terminal in their fiber, then you get a fully faithful eso.

Max New (Feb 27 2024 at 06:28):

Thanks, a lot of this sounds very similar to how we proved the theorem in Agda, because we formulated some of it in terms of displayed categories

Max New (Feb 27 2024 at 17:40):

I don't see, however, what would be the analog of the presheaf category in this definition, i.e., we can ask for a functor into presheaves, and then ask that each presheaf is representable, but what is the category of "non-contractible" cliques? It should be some category of "diagrams", i.e., functors $J \to D$ for some shape $J$, but the definition of composition/identity of clique morphisms on that page uses the fact the for a clique, $J$ is contractible, so it would need to be generalized.

John Baez (Feb 27 2024 at 17:59):

Btw, Max, you need to use double dollar signs here to get the LaTeX to work. Back when I was a moderator I would have edited your posts to accomplish this. But you can do it.

Morgan Rogers (he/him) (Feb 27 2024 at 19:39):

Wow you had the ability to modify people's messages!? I'm pretty sure moderators don't have that :melting_face:

Nathanael Arkor (Feb 27 2024 at 19:41):

Yes, no-one has the ability to edit other people's messages (unlike MathOverflow, for instance).

John Baez (Feb 27 2024 at 20:41):

Okay, hmm, that's weird, I thought I had that power here once, but maybe not. I often fix people's typos and screwed-up LaTeX on my blog.

Mike Shulman (Feb 27 2024 at 21:43):

I'm not sure there is an analogue of the presheaf category (that's different from the presheaf category).

One way to define the set of morphisms from a diagram $f:J\to D$ to a diagram $g:K\to D$ is as $\hom(f,g) = \lim_{j\in J} \mathrm{colim}_{k\in K} \hom_D(f j, g k)$. This generalizes what people do for [[pro-objects]] regarded as filtered diagrams. But, just as in that case, it turns out to be equivalent to considering morphisms between the formal colimits of $f$ and $g$ in the presheaf category, so the "category of diagrams" you get this way is equivalent to the presheaf category. And of course we had to choose a handedness in defining it (which side to take limits and which colimits), and the other choice would yield the co-presheaf category.

Another definition would be the [[lax slice 2-category]] of Cat over $D$. But that's a 2-category in general, not a 1-category, and in order to find the category of cliques inside it you need the axiom of choice for sets of objects.

Max New (Feb 27 2024 at 21:55):

That makes sense, the definition of composition in the clique category looks a lot like a 2-category that happens to be locally thin because of the contractibility of the shape of the diagram