Definitions into mathematical objects 9

7 November 2009 — Charles Wells

This is the ninth post in a series, continuing TDMO1, TDMO2, TDMO3, TDMO4, TDMO5, TDMO6, TDMO7 and TDMO8. This series builds up to an explanation of the concept of form in the paper Graph-Based Logic and Sketches by Atish Bagchi and me. This post tells how to sketch cartesian closed categories and gives an example of a form.

Cartesian closed categories

A Cartesian closed category is a category $\mathcal{C}$ with the following structure:

$\mathcal{C}$ has binary products.
For each pair of objects $A$ and $B$ of $\mathcal{C}$ , there is an object $B^A$ and an arrow $\text{eval}:B^A\times A\to B$ . $B^A$ is an exponential object.
For each triple of objects $A$ , $B$ and $C$ of $\mathcal{C}$ , there is a map $\lambda:\text{Hom}(B\times A, C)\to \text{Hom}(B,C^A)$ such that for every arrow $f:B\times A\to C$ , the diagram below commutes:

CCCDiagrams1 (lameval)

For any arrow $g:B\to C^A$ , $\lambda(\text{eval}\circ(g\times\text{Id}[A]))=g$ .

It follows that $\lambda$ is a natural isomorphism of homsets.

Going from $f:B\times A\to C$ to $\lambda f$ is called currying or partial application. You can curry a multivariable function all the way down to a constant. The inverse process is usually called uncurrying. It constitutes getting rid of entries in the codomain of a function that are function spaces by adding variables to the function. I suggest using blanding instead of “uncurrying”.

The FL sketch for cartesian closed categories

The FL sketch for CCC’s (which I will call CCCSk) is spelled out in detail in GBLS. I will mention some of the constructions here. I will use many of them in the next section to give an example of a form.

Objects and arrows

The arrows needed are spelled out in Sections 7.2 and 7.6 of GBLS. Here I mention

$\text{unit}:\text{ob}\to\text{ar}$ that formally picks out the identity arrow of an object.
$\text{twovf}$ , the formal set of functions of two variables, in other words arrows of the form $f:B\times A\to C$ .
$\text{arrow}:\text{twovf}\to\text{ob}^f$ that picks out the arrow $f$ itself.
$\text{tsource}:\text{twovf}\to\text{ob}$ that picks out the source $B\times A$ of a two-variable function $f:B\times A\to C$ .
$\text{curry}$ , the formal set of curried functions from $B \to C^A$ .
$\text{csource}:\text{curry}\to\text{ob}^B$ and $\text{ctarget}:\text{curry}\to\text{ob}^{C^A}$ that pick out the source and target of a curried function $g:B\to C^A$ .
$\text{fs}:\text{ob}^B\times\text{ob}^A\to\text{ob}^{B^A}$ that picks out the function space $B^A$ of two objects $B$ and $A$ .
$\text{ar}_2$ , the formal set of composable pairs of arrows in the FL sketch for categories, defined by this pullback diagram:

CatAr2Def (Ar2Def)

For the purposes of the example below, I need $\text{bsource}:\text{twovf}\to\text{ob}^B\times\text{ob}^A$ as defined by this diagram: CCCTSourceDef (Bsource)

In an object-oriented program built on this work, this would be a derived method..

One of the limit cones in CCCSk defines $\text{curry}$ and in particular gives $\text{fs}$ the properties it needs:

CCCurryDiagram (Curry)

The commutative diagram below should have been included in the FL sketch for categories in Section 7.2 of GLBS. It gives the composite of a composable pair the right source and target.

CatCompCompat (Compreq)

Representing reflexive function spaces

An object $A$ of a cartesian closed category is reflexive if there are arrows $I:A^A\to A$ and $J:A\to A^A$ such that

ReflexiveFSRetractDiagram (ret)

commutes. That means $A^A$ is a retract of $A$ . $A^A$ is called a reflexive function space. RFS’s are the theoretical basis for programming languages which have “functions as first class objects”.

So a sketch for RFS’s would be defined by a limit cone over the diagram below. I have always shown the cones in blue before, but GBLS does not show cones at all, and it isn’t necessary to show them.

ReflexiveConeBase (ReflFSConeBase)

To specify a reflexive function space you would have to give an object $A$ and two arrows $I:A^A\to A, J:A\to A^A$ that satisfies Diagram (lameval) above, so the mandatory projections would be to $\text{ob}^A$ , $\text{ar}^I$ and $\text{ar}^J$ . The projection to $\text{ob}^{A^A}$ is induced by Diagram (Curry) above, the projection to $\text{ar}^{<J,I>}$ by Diagram (Ar2Def), and the projection to $\text{ob}^A\times \text{ob}^A$ follows from the fact that it is the vertex of the product cone shown. The other projections exist by composition.

Let’s call the vertex of this cone $\text{rfs}$ for “reflexive function space”. Note that all the objects and arrows in this diagram exist in the FL sketch for cartesian closed categories.

Now you can check (or forget all the constructions above and just Put Your Hands On The Monitor And Believe) that in a model $M$ of the FL sketch for CCC’s, $M(\text{rfs})$ would be the set of reflexive function spaces together with specified inclusion $I:A^A\to A$ and retraction $J:A\to A^A$ .

Non-surprise: In any model of the FL sketch for CCC’s in the category of sets, $M(\text{rfs})$ will be the empty set. It is well known that for any set $A$ the function space $A^A$ has cardinality properly bigger that the cardinality of $A$ , so there can be no inclusion of $A^A$ into $A$ .

Nevertheless, $M(\text{rfs})$ is a perfectly well defined set. It just turns out to be empty.

Forms

Forms are defined formally in GBLS. This series of posts is supposed to give you an intuitive idea or understanding of form. Well, we can make a form for reflexive function spaces out of the work done above. Some terminology:

Constructor space

The sketch CCCSk for cartesian closed categories is a constructor space. A constructor space must be an FL-sketch that “contains” and is “generated” (see GBLS, Chapter 6.1) by the FL sketch for categories, and indeed CCCSk is built from the FL sketch for categories by adjoining some objects and arrows, cones and commutative diagrams that all exist already in the FL Cattheory for categories (see TDMO6). So a constructor space $\text{C}$ has models we can call C-categories. In particular a model for CCCSk in sets is a cartesian closed category. In previous posts I have constructed constructor spaces for categories with finite products and categories with finite limits.

Constructor spaces construct doctrines, in the one-dimensional case and with restrictions I will mention in a later post.

For any constructor space $\text{C}$ , take an object $F$ in the FL Cattheory of $\text{C}$ and adjoin a new arrow $f:1\to F$ where 1 is the terminal object. $f$ is what we call a C-form and $\text{C}$ with $f$ as a freely adjoined arrow is called $\text{C}_f$ .

A model of a $\text{C}$ -form “in a C-category $\cal{K}$ “ means that $\cal{K}$ is a model of $\text{C}_f$ This means that in $\cal{K}$ , $M(F)$ is nonempty.

The CCC-form for reflexive function spaces is then a global element of the node $\text{rfs}$ of CCCSk as constructed above for some CCC. There are no models in the category of sets, but there are many toposes (and many other CCC’s) that do have models, such as the realizability topos.

I have lots of miscellaneous comments and explanations to make about the idea of form which must wait for another post.

References

[1] Charles Wells (1990), A generalization of the concept of sketch.

(see TDMO6) (see TDMO6)

Posted in Sketches and forms, category theory, computer science, math. Tags: cartesian closed, evaluation, function space, object oriented programming, sketch. 1 Comment »

Gyre&Gimble

Recent posts

Categories

Archives