With braiding
With duals for objects
category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
With duals for morphisms
monoidal dagger-category?
With traces
Closed structure
Special sorts of products
Semisimplicity
Morphisms
Internal monoids
Examples
Theorems
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.
Any topos or quasitopos, such as Set, is cartesian closed.
See also closed monoidal structure on presheaves.
Cat is also cartesian closed. (Cf. e.g. p. 98 of Mac Lane, 2nd ed., or the remark below Definition 4.3.9 in Riehl.)
Many nice categories of topological spaces are also cartesian closed, particularly the convenient categories of spaces.
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 .
We have
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
In a cartesian closed category, the product functors have right adjoints, so they preserve all colimits. In particular, a cartesian closed category that has finite coproducts is a distributive category.
The internal logic of cartesian closed categories is minimal logic or the typed lambda-calculus.
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.
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
and is reproduced in the setting of closed monoidal categories at closed monoidal category.
Let be a cartesian closed category, and an object of . Then the Kleisli category of the comonad , denoted , is also a cartesian closed category.
The Kleisli category of the comonad on is canonically equivalent to the Kleisli category of the monad on .
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 .
(Functional completeness)
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 .
cartesian closed category, locally cartesian closed category
cartesian closed model category, locally cartesian closed model category
cartesian closed (∞,1)-category, locally cartesian closed (∞,1)-category
cartesian closed enriched category, locally cartesian closed enriched category
Textbook accounts:
Saunders MacLane, §IV.6 of: Categories for the Working Mathematician, Graduate Texts in Mathematics 5 Springer (1971, second ed. 1997) [doi:10.1007/978-1-4757-4721-8]
Francis Borceux, Def. 6.1.5 in: Categories and Structures, Vol. 2 of: Handbook of Categorical Algebra, Encyclopedia of Mathematics and its Applications 50 Cambridge University Press (1994) (doi:10.1017/CBO9780511525865)
Discussion with focus on mapping spaces (compact-open topology) in topological spaces and compactly generated topological spaces:
Susan Niefield, Cartesianness, PhD thesis, Rutgers 1978 (proquest:302920643)
Susan Niefield, Cartesianness: topological spaces, uniform spaces and affine schemes, J. Pure Appl. Algebra 23 (1982) 147-167 (doi:10.1016/0022-4049(82)90004-4)
See also the references at exponential object.
Establishing the syntax/semantics relation between cartesian closed categories and simply-typed lambda calculi:
A proof that a cartesian closed category is posetal if it satisfies an equality of morphisms not satisfied in a free cartesian closed category:
Last revised on October 7, 2023 at 21:48:53. See the history of this page for a list of all contributions to it.