# Almost an Adjunction…

The contravariant power-set functor $P:Set^{op} \longrightarrow Set$, together with its dual $P^{op}:Set \longrightarrow Set^{op}$, almost constitute an adjunction: there is natural monomorphism

• $\eta_{X,Y}:hom_{Set^{op}}(P^{op}(X), Y) \longrightarrow hom_{Set}(X, P(Y))$

which maps a $f: P^{op}(X) \longrightarrow Y$ (in $Set^{op}$) to $\tilde{f}:X \longrightarrow P(Y)$, defined by $\tilde{f}:x \longmapsto f^{-1}{x}$. One may readily verify naturality of $\eta$. Unfortunately, this map (of sets) is not surjective. However, if one restricts this pair of functors to the subcategory of all sets with injective maps, then they do constitute an adjunction.

My (quite vague) question is this: is this just a curiosity? Or is this particular $\eta$ part of something else, in some other context?

I'll write only maps that are actual functions to avoid confusion about contravariance. A map $f:Y\to P(X)$ corresponds to a map $f':X\to P(Y)$ by $f'(x)=\{y:x\in f(y)\}$. Then $f''(y)=\{x:y \in f'(x)\}=\{x:y\in \{\hat y: x\in f(\hat y)\}\}=\{x:x\in f(y)\}=f(y)$. Switching $X$ and $Y$, we see that the prime operation is indeed bijective. I don't understand your commentary about injective maps: certainly injections of $Y$ into $P(X)$ don't correspond to injections of $X$ into $P(Y)$, for cardinality reasons.
This natural isomorphism, which I'll call $\eta$ although it's not quite clear whether we've defined the same map, is well known in topos theory. $\eta$ exists and is an isomorphism in an arbitrary elementary topos, and in fact is monadic, as in sets when $P(S)$ is the free complete atomic Boolean algebra on $S$. This gives a way to prove that toposes have finite colimits, since it implies the opposite of a topos has finite limits.
• Just as a sidenote, this is also more generally a special case of the adjunction $[-, X]^\mathrm{op} ⊣ [-, X]$ in symmetric monoidal closed categories, which is immediate from Hom$(A, [B, X]) =$ Hom$(B, [A, X])$ since $P ≅ 2^{(-)}$. Another example is the vector space dualization functor $(-)^* ≅ \mathrm{Hom}_k(-, k)$. – user54748 Jul 19 '16 at 8:26
• Thanks Kevin! We did not define the same map, the definition of $f'$ that I gave is $f'(x) = f^{-1}{x}$ - just the pre-image of the singleton $\{x\}$ under $f$.... This 'prime' operation is indeed a natural monomorphism, which is as I have defined it above.. But your $\eta$ is more interesting, so thanks for that. – Mike Jul 19 '16 at 9:09