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: adjunction with icons

Bruno Gavranović (Sep 26 2022 at 09:17):

It's known that in an arbitrary 2-category an adjunction can only be defined using the unit-counit definition. As I've recently learned this is because 0-cells in general don't have intricate structure that would allow us to define this adjunction using, say, the local hom-set isomorphism.

And then if we set our base to be $\textbf{Cat}$ (the 2-category of categories, functors and natural transformations) we do get back this intricate structure of 0-cells (they're now categories) and we recover the usual notion of a adjoint functors, together with the corresponding hom-set isomorphism.

But $\textbf{Cat}$ is not the only 2-category where 0-cells are at least categories. There's also the option of $\textbf{2-Cat}^{ic}$, the 2-category of 2-categories, lax functors and icons.
This means we should get a corresponding relationship between the local hom-categories here (not mere sets anymore).
Has anyone unpacked what exactly that relationship is?

Mike Shulman (Sep 26 2022 at 15:12):

That 2-category sits inside the 2-category of double categories, lax double functors, and double transformations. Adjunctions in that 2-category include lots of interesting examples, see for instance Grandis-Pare "Adjoints for double categories", or my Framed bicategories and monoidal fibrations . But most of the examples don't sit inside the icons. The problem with adjunctions in icons is that that would mean the two adjoint functors have to be strict inverses on objects, which is rare.

Mike Shulman (Sep 26 2022 at 15:13):

By the way, a general framework for turning internal adjunctions in a 2-category into "hom-set isomorphism" style adjunctions is a [[proarrow equipment]].

Bruno Gavranović (Sep 27 2022 at 10:33):

Ah I see. Functors have to be strict inverses on objects because unit and counit natural transformations have to be identity on objects.
This does make adjunctions here rather specialised. I'm still curious about what happens locally on hom-categories, and whether there's any relationship analogous to the isomorphism for the case of $\textbf{Cat}$.

Do you have any intuitions about what I should be expecting here? I'm imagining the local hom-set iso from $\textbf{Cat}$ might be relaxed in one of two ways: either to become an adjunction, or perhaps to become not strictly natural, but up to a 2-cell?

Mike Shulman (Sep 27 2022 at 15:28):

Yes, you'll just get an adjunction between hom-categories. Look at what the unit and counit do on hom-categories.

Bruno Gavranović (Sep 28 2022 at 11:24):

That's interesting! I'll have to unpack the details of this some other time, since I don't immediately see how this follows from unit and counit's action on hom-categories (icons assign a natural transformation between local functors whose domain is that hom-category, but I don't see how that gives rise to a local adjunction).

What it looks like is that the nlab page on lax adjunctions gives the wrong idea that a local adjunction between hom-categories necessarily has to necessarily come from the weak setting of a lax 2-adjunction.
But here we see that we can both have an adjunction internal to a 2-category and a local adjunction at the same time.

Mike Shulman (Sep 28 2022 at 16:56):

I think an adjunction in the 2-category of icons is a special case of a lax 2-adjunction, just as an icon is a special case of an (op)lax transformation.

Bruno Gavranović (Oct 12 2022 at 02:01):

Of course. What's surprising to me is that having a local adjunction on hom-objects doesn't necessarily imply that globally we can have at most a lax 2-adjunction. We surely have a lax 2-adjunction -- but we also have something much stronger.

In other words -- we locally have a (strict) adjunction, and globally too! I'm not sure if I'm alone in appreciating this, but this feels very "fractal", for the lack of a better word.

Bruno Gavranović (Oct 12 2022 at 02:02):

Another way to say this is that it's surprising that the proof that the hom-set isomorphism following from unit-counit definition depends on the fact that 1-cells are strictly functorial, and not laxly so.

Bruno Gavranović (Jan 07 2023 at 08:06):

I've been thinking about this again, as what appears to be a very restricted setting of icons fits perfectly into the story of a paper on space-time tradeoffs of lenses and optics I've been writing.

I've been trying to prove a general statement: that an adjunction in the 2-category $\mathbf{2Cat}^{ic}$ of 2-categories, lax functors and icons gives rise to a local adjunction of hom-cats.

But I've stumbled upon something interesting: it appears as if this only works if the counit of the adjunction is identity. This is because in order to define the component 2-cell of a lax transformation $\mathcal{C}(-, R(-)) \Rightarrow \mathcal{D}(L(-), -)$ we need to go in the opposite direction of the counit $\epsilon$. That is, if the transformation we're defining is truly lax, then the direction of the 2-cell is up.
Screenshot_20230107_080256.png

Is anything known about this? I spent a while trying to show the counit being identity follows from the fact that we have a an adjunction, but it looks like that's really not the case: we get this constraint only if we try to induce the hom-object adjunction. I'm not sure if this is a peculiar consequence of the setting I'm in, or if I've made a mistake.

Bruno Gavranović (Jan 07 2023 at 08:06):

I'll mention that I've seen the notion of the proarrow equipment that @Mike Shulman linked, although I do have to say it's going over my head at the moment. I'm not sure how to tie it to the concrete setting I'm in.

Mike Shulman (Jan 08 2023 at 00:01):

Maybe the transformation you get is oplax?

Bruno Gavranović (Jan 08 2023 at 07:46):

That's what I thought. But then this would mean the other transformation ($\mathcal{D}(L(-), -) \Rightarrow \mathcal{C}(-, R(-))$) is oplax too, necessitating that the unit is identity, but also that the right adjoint is strict. Which just pushes the problem somewhere else.

Mike Shulman (Jan 08 2023 at 09:13):

Why would it mean that?

Bruno Gavranović (Jan 09 2023 at 00:08):

If an adjunction in $\mathbf{Cat}$ induces an isomorphism between functors $\mathcal{D}(L(-), -)$ and $\mathcal{C}(-, R(-))$ in the category $[\mathcal{C} \times \mathcal{D}^{op}, \mathbf{Set}]$ of functors and natural transformations, then it seems like an adjunction in $\mathbf{2Cat}^{ic}$ should induce an adjunction in the 2-category $[\mathcal{C} \times \mathcal{D}^{op}, \mathbf{Cat}]$ of lax functors, lax transformations and modifications.

This implies the 1-cells of our induced adjunction are lax transformations - both of them. The way I understand it, we could work in the corresponding 2-category where the transformations are oplax, but then both 1-cells would have to be oplax.

Mike Shulman (Jan 09 2023 at 01:38):

It's true that if you insist on an adjunction internal to some 2-category, then both transformations will have to have the same laxness. But it's possible to make sense of an adjunction between two morphisms with different laxnesses, for instance as a [[conjunction]] in some double category; see [[doctrinal adjunction]].