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.
[…] Qiaochu Yuan, Cartesian closed categories and the Lawvere fixed point theorem […]
[…] 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. […]