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: Hom-set proof of postcomposition adjunction

Ali Caglayan (Aug 22 2021 at 14:23):

Hi, I'm looking for a proof that postcomposition preserves adjunctions: $F \dashv G \implies F_* \dashv G_*$. I know a few proofs of this, but I am looking for one that only uses the hom-set definition of an adjunction.
Here is what I know:

• Using the unit-counit characterization of an adjunction, you can easily reassemble the parts of the postcomposition adjunction. But I don't want to use the unit-counit definition.
• The postcomposition functor $[X,-] : \mathsf{Cat} \to \mathsf{CAT}$ clearly preserves adjoint morphisms inside a 2-category, but this proof strays from the hom-set definition of an adjunction for the same reason as above.
• The closest I have found uses ends: $[X,C](F \circ x, y) \simeq \int_{i \in X} C(Fxi,yi) \simeq \int_{i \in X} D(xi,Gyi) \simeq [X,D](x,G \circ y)$ but I am not quite sure this gives me anything. It seems to me that it requires the same amount of work as defining the original hom-set bijection directly and showing that is natural.

Does anybody know an easier proof, or do I have to check the naturality by hand?

Mike Shulman (Aug 22 2021 at 15:37):

I'm just curious, why are you making things hard on yourself in this way? (-:

Ali Caglayan (Aug 22 2021 at 17:07):

Here is why I am making things hard: https://github.com/HoTT/HoTT/pull/1571

Nathanael Arkor (Aug 22 2021 at 18:18):

Surely it would be simpler to add the other characterisations of adjunctions, show that they imply one another, and them use the most convenient characterisation for the results you care about?