# Show that the powerset partial order is a cartesian closed category.

I'm trying to get started learning category theory. A problem I'm working on is to show that for a set $S$, the partial order $(\mathcal{P}(S),\subseteq)$ viewed as a category is cartesian closed.

So far, I was thinking that $S$ is the terminal object, and that the product of any two subsets $A \times B$ always exists (the greatest lower bound or intersection of $A$ and $B$), but am having trouble completing the proof by showing that the category has exponentiation.

If I understand right, the goal is to show that for any $A$ and $B$, there is a $C$ such that $C \times A \to B$ (i.e., $(C \cap A) \subseteq B$) if and only if there is a $B^A$ such that $C \subseteq B^A$ and $(B^A \cap A) \subseteq B$. But then this doesn't seem quite right.

I'm sorry for such a beginner question. I'd really appreciate any help pointing me in the right direction or maybe clarifying what/how one would go about showing that this category has exponentiation - or what does "$B^A$" mean in terms of these subsets? Does some sequence of operations construct it?

-
Think in terms of logic. This is the poset of all logical statements you can make about members of the set $S$, where there is a unique morphism $a \to b$ if $a$ entails $b$. The categorical product behaves like logical and. So what logical operation should correspond to exponentiation? – Qiaochu Yuan Dec 29 '12 at 23:41
Heuristically: Exponentiation $B^A$ is "morally" the function space $A\to B$, and trough the Curry-Howard isomorphism, this corresponds to the implication $A\Rightarrow B$, which is the same as $\neg A \lor B$, and since $\mathcal P(S)$ is a Boolean algebra, this suggests that it might work to take $B^A$ to be $(S\setminus A)\cup B$. (Or might not). – Henning Makholm Dec 29 '12 at 23:43
Henning: I think that you are cheating :-) You had known the conclusion in advance, wrote a wrong justification, and then called it a "heuristic". You cannot use the Curry-Howard isomorphism when $A \Rightarrow B$ is logically equvalent to $\neg A \vee B$. Simply because the corresponding types are not equivalent. (cont) – Michal R. Przybylek Dec 30 '12 at 0:17
@Mockup: I don't think Henning's comment is cheating. The power set is a Heyting algebra, so one could get to $A\implies B$ by Curry-Howard, and then use that classical logic is available to get from there to $(\neg A)\lor B$. On the other hand, I'd disagree with Henning's decision to use Curry-Howard in a comment for someone who says (s)he is "trying to get started learning category theory." – Andreas Blass Dec 30 '12 at 1:38
@J.B.: Amplifying Mockup's last comment: You have to show that, for every $A$ and $B$, there exists some $B^A$, such that for every $C$, $C\cap A\subseteq B$ if and only if $C\subseteq B^A$. – Andreas Blass Dec 30 '12 at 1:41

Let's prove something stronger: every infinitary-distributive complete lattice is a complete Heyting algebra (and so cartesian closed as a category).

Recall, a complete lattice is a partial order in which all meets and joins exist. The powerset of a set is certainly a complete lattice, and it moreover satisfies the infinite distributive law: $$\left( \bigcup_{i \in I} A_i \right) \cap B = \bigcup_{i \in I} (A_i \cap B)$$ Now the claim is that such a complete lattice has a Heyting operation, i.e. a binary operation $\to$ such that $A \subseteq (B \to C)$ if and only if $A \cap B \subseteq C$ for all $A$. How do we do this? Let's apply wishful thinking. Suppose we had such a $(B \to C)$; then $(B \to C) \subseteq (B \to C)$, and in particular, $(B \to C)$ must be the greatest $A$ such that $A \cap B \subseteq C$. On the other hand, we are in a complete lattice, so we can certainly define $$(B \to C) = \bigcup \{ A : A \cap B \subseteq C \}$$ and this works: if $A \subseteq (B \to C)$, then $$A \cap B \subseteq (B \to C) \cap B = \left( \bigcup \{ A : A \cap B \subseteq C \} \right) \cap B = \bigcup \{ A \cap B : A \cap B \subseteq C \} \subseteq C$$ by the infinite distributive law; the converse is automatic by construction of $(B \to C)$.

The nice thing about this proof is that it is completely constructive and can be internalised in any topos. But in the classical setting, we can be a little bit more explicit about what $(B \to C)$ is: writing $B^{\mathsf{c}}$ for the complement of $B$, we have $(B \to C) = B^{\mathsf{c}} \cup C$. Clearly, $(B^{\mathsf{c}} \cup C) \cap B = C \cap B \subseteq C$, so $(B^{\mathsf{c}} \cup C) \subseteq (B \to C)$; on the other hand, if $A \cap B \subseteq C$, then $B^{\mathsf{c}} \cup (A \cap B) \subseteq B^{\mathsf{c}} \cup C$, and clearly $$A = A \cap (B^{\mathsf{c}} \cup B) = (A \cap B^{\mathsf{c}}) \cup (A \cap B) \subseteq B^{\mathsf{c}} \cup (A \cap B)$$ so $A \subseteq B^{\mathsf{c}} \cup C$, and therefore $(B \to C) \subseteq B^{\mathsf{c}} \cup C$, as required. (Exercise: Where have I used the law of excluded middle in this argument?)

-

I found this question in Pierce's book and have been working on it today. Here's what I've got:

The Problem: The exponent $B^A$ needs to be a member of the powerset. Moreover it has to satisfy the following constraints:

• There is a map from $B^A \times A$ to $B$.
• in terms of sets, $B^A \times A \subseteq B$
• For every other powerset object $C$ such that $g: C \times A \rightarrow B$ exists, we need a unique map from $C$ to $B$
• again in terms of sets, we must show that for all $C$ such that $C \times A \subseteq B$, the relation $C \subseteq B$ must hold.

Solution: If $B \subset A$ then $B^A = B$. Otherwise $B^A = S$ (the final object in our powerset category).

Justification: If $B \subset A$ then $B^A$ must be a subset of $B$ for $B^A \times A \subseteq B$ to hold. We deduce that $B^A$ must be $B$ exactly because it is the only choice that guarantees $C \subseteq B^A$ for every $C$ such that $C^A \times A \subseteq B$.

If $A \subseteq B$ then $B^A \times A \subseteq B$ holds for any choice of $B^A$. Likewise, we can use any powerset element $C$ to satisfy $C^A \times A \subseteq B$. Because of this, $B^A$ has to be the entire set $S$. It is the only choice that guarantees $C \subseteq B^A$ for every valid choice of $C$.

-