Previously we saw that Cantor’s theorem, the halting problem, and Russell’s paradox all employ the same diagonalization argument, which takes the following form. Let be a set and let

be a function. Then we can write down a function such that . If we **curry** to obtain a function

it now follows that there cannot exist such that , since .

Currying is a fundamental notion. In mathematics, it is constantly implicitly used to talk about function spaces. In computer science, it is how some programming languages like Haskell describe functions which take multiple arguments: such a function is modeled as taking one argument and returning a function which takes further arguments. In type theory, it reproduces function types. In logic, it reproduces material implication.

Today we will discuss the appropriate categorical setting for understanding currying, namely that of cartesian closed categories. As an application of the formalism, we will prove the Lawvere fixed point theorem, which generalizes the argument behind Cantor’s theorem to cartesian closed categories.

**Some examples of mathematical currying**

*Example.* A group action on a set is often described using a function . Currying gives a function ; in other words, it associates to every element a function . It seems more natural to define a group action in this way, but what works in may work less well in other categories; for example, when defining actions of Lie groups on manifolds, we talk about smooth functions because it is unclear in this setting in what sense the space of smooth functions is a smooth manifold (hence in what sense we should be asking for smooth functions from into this space).

*Example.* A vector space is equipped with a dual pairing . Currying gives a function , and the corresponding functions are in fact linear, so we can associate to every an element of the double dual space . In other words, currying gives us the double dual map . There is a similar map in the setting of Pontrjagin duality.

*Example.* A topological space is equipped with an evaluation map , where here denotes the space of continuous complex-valued functions . Currying gives a function which associates to every an evaluation map . When is compact Hausdorff, every homomorphism of complex algebras has this form.

**Cartesian closed categories**

A **cartesian closed category** is a category with finite products in which the product functor has a right adjoint, the **exponential** . In other words, there is a natural identification

.

The notation is nonstandard; a more conventional notation is , but the notation (which is sometimes used for the more general notion of internal hom) emphasizes the fact that a Cartesian closed category is in particular a closed monoidal category, and in particular is enriched over itself.

Letting be the terminal object, we get that there is a natural identification

.

In other words, the **global points** (morphisms from , also just called **points**) of are naturally identified with the set of morphisms from to .

More generally, the -points of , which by definition are naturally identified with , should be thought of as “-parameterized families of morphisms from to .”

Uncurrying the identity map , we obtain the **evaluation map**

describing, internally, how to evaluate functions on arguments. In computer science, this function is also called **apply**.

*Example.* is cartesian closed, and is the basic example. Here the internal hom is the set of functions from to and the global points of a set are its set of points in the ordinary sense. The same applies to .

*Example.* The category of (small) categories is cartesian closed. Here the product is the usual product of catgories and the internal hom is the category of functors from to , with morphisms given by natural transformations. The global points of a category are its objects.

*Subexample.* In , the subcategory of groupoids is cartesian closed, since the product of groupoids and the functor category between two groupoids both remain groupoids. If are two groups regarded as one-object categories, the functor category is the groupoid whose objects are the morphisms and whose morphisms are given by pointwise conjugation by elements of . Note that the category of groups is not cartesian closed.

*Subexample.* In , the subcategory of posets is cartesian closed, since the product of posets and the functor category between two posets both remain posets. If are two posets, then is the poset of order-preserving functions with iff for all .

*Example.* Let be a group. The category is cartesian closed; it has a product inherited from , and exponential objects are given by the set of all functions from to together with the -action

.

The global points of a -set are its fixed points, and in particular the global points of are the set of -morphisms .

*Example.* Any Boolean algebra, regarded as a poset and then regarded as a category, is cartesian closed. The product of two propositions is their logical “and” , and the exponential object is the material implication . The currying adjunction

simply says that implies if and only if implies . The terminal object is the proposition “true,” and a proposition has a global point if and only if it is a tautology. The evaluation map is an internal description of modus ponens.

*Non-example.* It is an unfortunate fact about point-set topology that is not cartesian closed (see, for example, this math.SE question). When it exists, the exponential is often given the compact-open topology. This problem is fixed by working instead with a convenient category of topological spaces, such as the category of compactly generated spaces.

*Non-example.* Suppose a cartesian closed category has a zero object . Since there is a unique morphism from to any other object, it follows that every exponential has a unique global point, hence that there is a unique morphism from any object to any other object (necessarily the zero morphism). Conversely, if has a zero object and a nonzero morphism, then cannot be cartesian closed.

**Proposition:** In a cartesian closed category, products distribute over colimits in both variables, and exponentials send colimits in to limits and preserves limits in .

**Corollary:** If is a cartesian closed category with finite coproducts (a **bicartesian closed category**), then letting denote the coproduct, we have the following natural identifications:

- (so is a distributive category),
- .

*Proof.* These all follow from the natural identifications

.

In more detail, is a left adjoint and hence preserves arbitrary colimits, is a right adjoint and hence preserves arbitrary limits, and is a (contravariant) right adjoint (to itself!) and hence, as a contravariant functor on , sends colimits to limits.

Specialized to the cartesian closed category of finite sets, the above result explains from a categorical point of view the algebraic axioms satisfied by addition, multiplication, and exponentiation of non-negative integers.

**Corollary:** Let be a category. Then the category of presheaves on is cartesian closed.

This greatly generalizes the example of ; we get, for example, a version of the category of graphs and the category of simplicial sets as special cases.

*Proof.* Products are easy to construct, since limits are computed pointwise. To construct exponentials, suppose that are two presheaves whose exponential exists. The universal property and the Yoneda lemma together imply that

which uniquely defines a presheaf. It remains to check that this presheaf really satisfies the universal property, but this follows from the fact that every presheaf is a colimit of representable presheaves and from the fact that products distribute over colimits, which is true because it is true pointwise; that is, in .

The terminal object in is the presheaf sending every object to and sending every morphism to the unique morphism . If itself has a terminal object , then it represents the terminal presheaf, hence a global point of a presheaf is just an element of , so we can explicitly verify that . In general, a global point of a presheaf is a choice of element for each which is compatible with every morphism in in the sense that if is any morphism, then ; in other words, it is an element of the limit .

In particular, if is the category of open subsets of a topological space (so that a presheaf on is a presheaf on in the usual sense), then a global point of a presheaf is a **global section**. Note that this is equivalently an element of (since is the terminal object) or a choice of element for each open which is compatible with inclusions in the sense that if then restricts to .

The category of sheaves on a topological space is also a cartesian closed category, and moreover is a topos.

**Presheaves on a monoid**

We showed earlier that is cartesian closed for a group, but the explicit description we gave of the exponential requires talking about inverses in . On the other hand, the above theorem implies in particular that is cartesian closed for a monoid which is not necessarily a group. What does the exponential look like in this case?

Let be a category with one object with endomorphism monoid . Then is the category of right -sets, and the unique representable presheaf is as a right -module over itself. If are two -sets, then the above description of the exponential gives

with right -action induced from the left -action of on itself. If is a group, this is naturally isomorphic to , since a morphism of right -sets is freely and uniquely determined by what it does to (where is the identity). This can fail if is not a group, since the value of such a morphism on may not be determined by the value on an element of the form if is not of the form for any , and also since the value of a morphism on may be constrained by the value on two elements of the form if there exists an such that .

*Example.* Let be the free monoid on an idempotent, so that . This is the smallest monoid which is not a group. The category of right -sets is the category of sets equipped with idempotent endomorphisms. The subcategory of such sets such that is constant (equivalently, such that has a unique fixed point) is equivalent to the category of pointed sets: a morphism between such -sets is precisely a map of sets which preserves the unique fixed point. Thus if are such -sets of cardinalities respectively, then is again such a set of cardinality , and so there are morphisms . On the other hand, there are maps of sets.

**The Lawvere fixed point theorem**

To motivate the Lawvere fixed point theorem, let’s write the diagonalization argument above in somewhat greater generality. If is any function, then we can find a function such that iff . Now we curry to obtain a function . If there exists such that , then as before and cannot be in the image of , hence is not surjective.

The crucial step is the step where we write down the function such that . A systematic way to do this is to compose with a function with no fixed points. Lawvere realized that, by taking contrapositives, this means the basic argument behind Cantor’s theorem can be recast as the following fixed point theorem.

**Theorem (Lawvere):** Let be objects in a category with finite products such that the exponential exists (in particular, this is true for any pair of objects in a cartesian closed category). Let and suppose that is **surjective on points** in the sense that the induced map is surjective. Then every morphism has a **fixed point** in the sense that the induced map has a fixed point; that is, has the **fixed point property**.

*Proof.* Let be any morphism and let

where is the diagonal map; see, for example, this blog post. ( specializes to the paradoxical subset constructed in the usual proof of Cantor’s theorem.) By hypothesis, there exists a point such that (where, if are two morphisms in a category with finite products, denotes the product morphism .) But then

whereas by definition , from which it follows that is a fixed point of .

**Taking the contrapositive**

Taking the contrapositive, we conclude that if is an object in a cartesian closed category such that there exists a function with no fixed points, then no morphism can be surjective on points. When in we immediately reproduce Cantor’s theorem, and morally we reproduce Russell’s paradox as well. The proof of the Lawvere fixed point theorem actually provides a particular morphism not in the image of any morphism ; this particular morphism generalizes CantorBot and also gives us the unsolvability of the halting problem.

on December 10, 2013 at 8:55 pm |How to invent intuitionistic logic | Annoying Precision[…] Propositional logic should have an “internal” notion of implication. In other words, should not only just be true or false but should itself be a proposition. This would allow us to state inference rules like modus ponens (). The corresponding universal property is that if and only if . This is precisely the universal property of exponential objects, which we encountered when talking about the Lawvere fixed point theorem. […]