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: construction of left adjoint by generators and symm. topos

Jonas Frey (Aug 30 2025 at 18:11):

Is the following principle stated anywhere? Or am I confused?

Let $U : B \to A$ be a functor between cocomplete categories. An object $a\in A$ is called $U$-adjointable, if $\hom(a,U-)$ is representable. Then the class of $U$-adjointable objects is closed under colimits in $A$. In particular, to prove that $U$ has a left adjoint, it is sufficient to exhibit "free" objects for a class of objects which generate $A$ under colimits.

Proof: If $a$ is the colimit of a diagram $D$ of $U$-adjointable objects, then $\hom(a,U-)$ is represented by $\mathsf{colim}(FD)$, where $F$ is the partial left adjoint on the category of adjointable objects.

(I'm asking since Johnstone uses something like this to show that the "symmetric monad" exists, and I was wondering why he didn't have to prove well-definedness. But it seems to be a general thing?)

Jonas Frey (Aug 30 2025 at 18:46):

Just for completeness, let me give Johnstone's argument: we want to show that the forgetful 2-functor

$U:\mathsf{Logos}\to\mathsf{Pres}$

has a left biadjoint, where $\mathsf{Logos}$ is the 2-category of Grothendieck toposes and lex cocontinuous functors, ie inverse image parts of geometric morphisms, and $\mathsf{Pres}$ is the 2-category of locally presentable categories and cocontinuous functors. It is easy to see that free logoses over presheaf categories $P(C)$ (viewed as objects of $\mathsf{Pres}$) exist: the free logos on $P(C)$ is $P(\mathsf{Lex}(C))$ -- the category of presheaves on the free finite-limit category on $C$. The existence of the left biadjoint now follows from the above principle since every presentable category is presentable as a coinverter of a $2$-cell between cocontinuous functors between presheaf categories.

Jonas Frey (Aug 30 2025 at 18:49):

Actually the left adjoint to $U:\mathsf{Logos}\to\mathsf{Pres}$ is closely related to (almost and instance of) the use of the adjoint lifting theorem discussed here in the context of distributive laws a while ago. So the above principle seems to be a good way to think about the extension of left adjoints from Kleisli categories to categories of algebras in general.

Patrick Nicodemus (Aug 30 2025 at 18:51):

Seems like valid reasoning to me. I've never observed that principle before.

Mike Shulman (Aug 30 2025 at 18:54):

Makes sense to me, and I don't remember seeing it written down abstractly anywhere.

Nathanael Arkor (Aug 31 2025 at 06:11):

I believe this is an instance of the following result (which appears in my thesis), which gives necessary and sufficient conditions for a relative adjunction to extend to an adjunction. (Note that, if $A$ is small, and $B$ is cocomplete, then the pointwise left extension is guaranteed to exist.)
image.png

This holds in any proarrow equipment (and more generally any [[virtual equipment]]), so in particular holds for 2-functors between 2-categories. The same argument works mutatis mutandis to extend relative pseudoadjunctions to pseudoadjunctions.

Ivan Di Liberti (Aug 31 2025 at 10:28):

Nathanael Arkor said:

The same argument works mutatis mutandis to extend relative pseudoadjunctions to pseudoadjunctions.

How do you feel about this statement of yours and our policy in citing these kind of results? Should Jonas just say that the theorem follow from a pseudo-version of Prop 5.4.7 in Arkor? Or this is not acceptable.

My personal answer is that this is a very valid argument, but I can see many referees rejecting a paper based on such justification (this actually happened to me several times).

Ivan Di Liberti (Aug 31 2025 at 10:30):

Most importantly, if we think that this is not a valid argument, are we envisaging -- almost suggesting -- that there should be a Pseudo-Arkor, writing a pseudo-version of his PhD thesis to fill the gap in the literature?

Ivan Di Liberti (Aug 31 2025 at 10:32):

(Maybe I should make my question even more clear: would you, as a referee, be fine with such justification? And if not, what should the author say?)

Nathanael Arkor (Aug 31 2025 at 11:01):

In this specific instance, the proof in the bicategorical case really does just proceed by replacing isomorphisms with equivalences everywhere (and it is clear this works, because the proof is given simply by constructing a chain of isomorphisms). So I don't think I would have a problem with authors simply pointing to the one-dimensional argument. On the other hand, I do not find it reasonable for authors simply to refer to a one-dimensional argument that involves equational reasoning (and hence requires dealing with coherence in two dimensions), because these do not extend from one dimension so evidently.

Nathanael Arkor (Aug 31 2025 at 11:02):

But one can always mollify a reluctant reviewer by including an explicit proof, which is not very long anyway.

fosco (Aug 31 2025 at 14:47):

The famous mollifiers for referees....

Mike Shulman (Aug 31 2025 at 16:57):

Nathanael Arkor said:

In this specific instance, the proof in the bicategorical case really does just proceed by replacing isomorphisms with equivalences everywhere (and it is clear this works, because the proof is given simply by constructing a chain of isomorphisms).

One way to make that more precise is to say that the proof evidently works in a context for formal category theory, like a proarrow equipment, and thus can be specialized directly to the proarrow equipment of bicategories as well (and also to other contexts like $\infty$-categories).

There was a time when I hoped that one day it would become the norm to actually write proofs in a language of formal category theory when possible, saving the reader the trouble of observing that they can be generalized that way.

John Baez (Aug 31 2025 at 17:38):

There was a time when I hoped that one day... - the distant past of the far future, the tense used by old mathematicians. Heck, you might as well still hope that one day it will be the norm.

Nathanael Arkor (Aug 31 2025 at 17:58):

Mike Shulman said:

One way to make that more precise is to say that the proof evidently works in a context for formal category theory, like a proarrow equipment, and thus can be specialized directly to the proarrow equipment of bicategories as well (and also to other contexts like $\infty$-categories).

The proof in my thesis is in the context of a proarrow equipment. But to establish the result for pseudoadjunctions rather than adjunctions, one would need to reason about equivalences of 1-cells, rather than isomorphisms of 1-cells, and it's not clear to me that this is possible without working with a three-dimensional notion of proarrow equipment?

Nathanael Arkor (Aug 31 2025 at 18:00):

Mike Shulman said:

There was a time when I hoped that one day it would become the norm to actually write proofs in a language of formal category theory when possible, saving the reader the trouble of observing that they can be generalized that way.

I still have hope :) One thing that I think would help a lot is having an introductory textbook on formal category theory...

Mike Shulman (Aug 31 2025 at 21:42):

I was thinking of a proarrow equipment of bicategories where the 2-cells are isomorphism classes of pseudonatural transformations.