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?


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?)