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: Exponential is Automatically Contravariant in Exponent?

Ignat Insarov (Dec 22 2024 at 09:58):

Page 18 of Sheaves in Geometry and Logic says:

${C → B^A \over A × C → B} (16)$

… It follows from the various uniqueness properties that $B^A$ is also a (contravariant!) functor of $A$ (at least on those $A$ which are exponentiable), and that $(16)$ is also natural in $A$ . …

This shocked me. I looked at this adjunction many times times, but it never occurred to me that the exponential is automatically contravariant in the exponent — I always assumed this needs to be postulated on top of the adjunction. Is there a way I could have foreseen this — is there a way this result is to be expected?

I took this as an exercise and figured that we have as the function on arrows $f ↦ A^f$ the operation:

$f: x → y \quad ↦ \quad ε^x ∘ (f × A^y)^x ∘ η: A^y → A^x$

It takes about a hundred arrows to show functoriality and naturality! «It follows from the various uniqueness properties…»

Ignat Insarov (Dec 22 2024 at 09:59):

Following are the illustrations for my proofs.

Ignat Insarov (Dec 22 2024 at 10:00):

I used these two equations freely without proof (because I believe they are widely known to be true):

$F (f, B) ∘ F (A, g) = F (f, g) = F (A, g) ∘ F (f, B)$ where $F$ bifunctor
$ε ∘ S η = id$ and $T ε ∘ η = id$ where $S ⊣ T$

John Baez (Dec 22 2024 at 19:27):

Ignat Insarov said:

Page 18 of Sheaves in Geometry and Logic says:

${C → B^A \over A × C → B} (16)$

… It follows from the various uniqueness properties that $B^A$ is also a (contravariant!) functor of $A$ (at least on those $A$ which are exponentiable), and that $(16)$ is also natural in $A$ . …

This shocked me. I looked at this adjunction many times times, but it never occurred to me that the exponential is automatically contravariant in the exponent — I always assumed this needs to be postulated on top of the adjunction. Is there a way I could have foreseen this — is there a way this result is to be expected?

Right from the start, I'd expect $B^A$ is either covariant or contravariant in $A$ , because it's defined using a universal property. That's just my expectation.

I believe that using the Yoneda lemma we can show $B^A$ is covariant (resp. covariant) in $A$ iff $\text{hom}(C,B^A)$ is covariant (resp. contravariant) in $A$ for each $C$ .

But $\text{hom}(C,B^A)$ is naturally isomorphic to $\text{hom}(A \times C, B)$ , which is clearly contravariant in $A$ .

Ignat Insarov (Jan 03 2025 at 06:45):

But wait…

John Baez said:

But $\text{hom}(C,B^A)$ is naturally isomorphic to $\text{hom}(A \times C, B)$ , which is clearly contravariant in $A$ .

What we are given is actually not one adjunction, but a family of adjunctions $φ_A$ indexed by objects of $\mathcal C$ , right? Each adjunction is $φ_A: \mathcal C [A × x → y] ≅ \mathcal C [x → y^A]$ , naturally in $x$ and $y$ . But there is nothing that relates, for example, $\mathcal C [A × x → y]$ with $\mathcal C [x → y^B]$ , yet. It is our hope to guess, and our task to show, that, given $f: B → A$ , the evident square with these corners commutes. That $φ$ is natural in $x$ and $y$ does not seem at first sight to be of any relevance here.

Mike Shulman (Jan 03 2025 at 17:13):

But we aren't even given that $B^A$ is functorial in $A$ at all. So we can (and do) define that functorial action so as to make that square commute, which is (uniquely) possible by the Yoneda lemma and since the natural components are isomorphisms.

Mike Shulman (Jan 03 2025 at 17:17):

The naturality of those isomorphisms in $x$ is what tells us that when we transport the functoriality of $A\times x$ in $A$ across those isomorphisms, we get a natural transformation and hence can apply the Yoneda lemma.

Their naturality in $y$ then tells us that the resulting functoriality of $B^A$ in $A$ commutes with its given functoriality in $B$ . (Assuming that we were given the latter, which is necessary to talk about naturality in $y$ . Alternatively we could just be given the $B^A$ as objects and define their functorial action on $B$ in the same way.)