11
$\begingroup$

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?

  • 3
    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?2012-12-29
  • 4
    **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).2012-12-29
  • 0
    Thanks, your comments definitely help. I'll see if I can finish it from there.2012-12-29
  • 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)2012-12-30
  • 1
    For example there is a generic function (the identity) belonging to $A \Rightarrow A$ and one may prove that there is no such a generic function belonging to $\neg A \vee A$. You may say: ha, there is also a variant of Curry-Howard isomorphism for classical logic --- but you know, this isomorphism does not deal with cartesian closed categories.2012-12-30
  • 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.2012-12-30
  • 3
    @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."2012-12-30
  • 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$.2012-12-30
  • 1
    @Mockup: No, actually I _don't_ know the conclusion. My heuristic argument explains how I'd choose the first thing to try if I had the inclination to attempt to verify a solution.2012-12-30
  • 0
    @Andreas: put it another way --- a simply typed lambda calculus with a naive law of excluded middle is necessary degenerated. Therefore, it *is* a classical propositional logic. I do understand that a degenerted cartesian closed category is the same thing as a Heyting algebra, and I do understand that the internal language of any cartesian closed category is a simply typed lambda calculus (this is a part of the Lambek correspondence). What I do not understand is how one could apply the Curry-Howard isomorphism to get the above.2013-01-01
  • 0
    BTW: it is well-known that a cartesian closed category having *isomorphisms* $\neg \neg A \rightarrow A$ for every object $A$ is necessary degenerated. It is not so well-known that it suffices that there exists a *natural* morphism $\neg \neg A \rightarrow A$ to make a cartesian closed category degenerated.2013-01-01
  • 0
    That is indeed not-so-well-known. Do you have a reference?2013-01-05
  • 0
    @Zhen: I used to give it on exams, so it cannot be really hard :-) I mentioned this, because it shows that it is impossible to give a coherent semantics for lambda calculi with double-negation rule in cartesian closed categories; that is: it is easy to find a non-degenerated CCC with $\neg\neg A \rightarrow A$ and $\neg\neg A \leftarrow A$ for every object $A$, so one may wonder if it is possible to find a coherent collection of morphisms $\neg\neg A \rightarrow A$, which are not necessary the inversion of the canonical $\neg\neg A \leftarrow A$ --- it turns out, it is impossible.2013-01-05

2 Answers 2