With duals for objects
With duals for morphisms
Special sorts of products
In higher category theory
A cartesian closed category (sometimes: ccc) is a category with finite products which is closed with respect to its cartesian monoidal structure.
The internal hom in a cartesian closed category is often called exponentiation and is denoted .
A cartesian closed functor between cartesian closed categories , is a functor that is product-preserving and that is also exponential-preserving, meaning that the canonical map
corresponding to the composite
is an isomorphism.
Some basic consequences
A category is cartesian closed if it has finite products and if for any two objects , , there is an object (thought of as a “space of maps from to ”) such that for any object , there is a bijection between the set of maps and the set of maps , and this bijection is natural in .
There is an evaluation map , which by definition is the map corresponding to the identity map under the bijection. Using the naturality, it may be shown that the bijection takes a map to the composite
and the universal property of may be phrased thus: given any , there exists a unique map for which .
Taking (the terminal object), maps (or “points” of ) are in bijection with maps . So the “underlying set” of , namely , is identified with the set of maps from to . Let us denote the point corresponding to by . Then, by definition,
The following lemma says that the internal evaluation map indeed behaves as an evaluation map at the level of underlying sets.
Given a map and a point , the composite
is the point .
where the penultimate equation uses naturality of the projection map .
Internal composition is the unique map such that
One may show that internal composition behaves as the usual composition at the underlying set level, in that given maps , , we have
Inheritance by reflective subcategories
In showing that a given category is cartesian closed, the following theorem is often useful (cf. A4.3.1 in the Elephant):
If is cartesian closed, and is a reflective subcategory, then the reflector preserves finite products if and only if is an exponential ideal (i.e. implies for any ). In particular, if preserves finite products, then is cartesian closed.
Exponentials of cartesian closed categories
The following observation was taken from a post of Mike Shulman at MathOverflow.
If is small and is complete and cartesian closed, then is also complete and cartesian closed. Completeness is clear since limits in are computed pointwise. As for cartesian closure, we can compute exponentials in essentially the same way as for presheaves, motivated by -enriched category theory:
Then we can compute
Here the antepenultimate step uses the co-Yoneda lemma. This appears to involve colimits in as well, but the existence of these colimits is not actually an extra assumption: the co-Yoneda lemma tells us that exists and is isomorphic to .
Similarly, the above argument can be interpreted to say that even if is not complete, then the exponential in exists if and only if the particular limits above exist, and in that case they are isomorphic.
A more abstract argument using comonadicity and the adjoint triangle theorem, which also applies to locally cartesian closed categories, can be found in Theorem 2.12 of
- Street and Verity, The comprehensive factorization and torsors, TAC
and is reproduced in the setting of closed monoidal categories at closed monoidal category.
Functional completeness theorem
of Theorem 2
Let and be objects of . Claim: the product in , considered as an object of , is the product of and in , according to the following series of natural bijections:
Claim: the exponential in , considered as an object of , is the exponential of and in , according to the following series of natural bijections:
where in the last step, we used the prior claim that the product of objects in , when viewed as an object of , gives the product in .
Observe that the object in has an element , corresponding to the canonical isomorphism in . We call this element the “generic element” of in , according to the following theorem. This theorem can be viewed as saying that in the doctrine of cartesian closed categories, is the result of freely adjoining an arrow to .
Let and be cartesian closed categories, and let be a cartesian closed functor. Let be an object of , and let be an element in . Then there exists an extension of to a cartesian closed functor that takes the generic element in to the element , and this extension is unique up to isomorphism.
On objects, . Let be a map of , i.e., let be the corresponding map in , and define to be the composite
It is straightforward to check that is a cartesian closed functor and is, up to isomorphism, the unique cartesian closed functor taking to .