Friday, April 25, 2014

Cartesian closed categories

This is not intended to give an introduction to cartesian closed categories (“cccs”), which are discussed in many places, e.g. Wikipedia, nlab.
Rather, the aim of this document is simply to compare two extremely significant cccs: $\bftwo$ which is basic to Boolean logic, and $\Set$ which is, of course, basic to set theory.
More precisely, we wish to compare the notations which are used to express the ccc operations, and how several of the simple but significant theorems valid in these cccs are expressed.
In fact, both $\bftwo$ and $\Set$ are, as well as being cartesian closed, are also cocomplete.
So the names of the operators relevant to cocompletion are also shown, with their related simple theorems.

Description ccc Comment
$\bftwo$ $\Set$
initial object $\bot$ $\emptyset$
terminal object $\top$ $1$
binary cartesian product $\wedge$ $\times$
internal hom $\Rightarrow$ $[,]$
formulae involving the binary product $\bot\wedge\objA = \bot$ $\emptyset\times\objA \cong \emptyset$ absorption
$\top\wedge\objA = \objA$ $1\times\objA \cong \objA$ identity or unit
formulae involving the internal hom $\bot\Rightarrow\objA = \top$ $[\emptyset,\objA] \cong 1$
$\top\Rightarrow\objA = \objA$ $[1,\objA] \cong \objA$
the product of $\functionA:\setX\to \text{ccc}$ (where $\setX\in\Set$) $ \left\{ \begin{array}{}(\forall \eltx\in\setX)\functionA_\eltx\\ \displaystyle\bigwedge_{\eltx\in\setX}\objA_\eltx\\ \end{array} \right\} $ $\displaystyle\prod_{\eltx\in\setX}\functionA_\eltx$
binary coproduct $\vee$ $+$ or $\coprod$
formulae involving the binary coproduct $\bot\vee\objA = \objA$ $\emptyset+\objA \cong \objA$ identity or unit
$\top\vee\objA = \top$ $1+\objA$
the coproduct of $\functionA:\setX\to \text{ccc}$ (where $\setX\in\Set$) $ \left\{\begin{array}{}(\exists\eltx\in\setX)\functionA_\eltx\\ \displaystyle\bigvee_{\eltx\in\setX}\objA_\eltx\\ \end{array} \right\} $ $\displaystyle\sum_{\eltx\in\setX}\functionA_\eltx$

No comments:

Post a Comment