Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
2  
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
3  
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
3  
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
2  
J.B.: You made a mistake in stating the universal property for the exponent: we have to show that for any $A$, $B$ and every $C$ your equivalence holds. –  Michal R. Przybylek Dec 30 '12 at 0:21
3  
@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

2 Answers 2

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

share|improve this answer

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$.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.