The category ''C'' is called Iff it satisfies the following three properties:
- it has a Terminal Object
- any two objects ''X'' and ''Y'' of ''C'' have a Product ''X''×''Y'' in ''C''
- any two objects ''Y'' and ''Z'' of ''C'' have an Exponential ''Z''''Y'' in ''C''
For the first two conditions above, it is the same to require that any finite (possibly empty) family of objects of ''C'' admit a Product in ''C'', because of the natural associativity of the categorical product and noticing that the empty product in a category is nothing but the Terminal Object of that category.
For the third condition it is equivalent to ask that the Functor –×''Y'' (i.e. the functor from ''C'' to ''C'' that maps objects ''X'' to ''X''×''Y'' and morphisms φ to φ×id''Y'') has a Right Adjoint , usually denoted –''Y'', for all objects ''Y'' in ''C''. This in turn, is expressed by the existence of a Bijection between the Hom-set s
:
which is Natural in both ''X'' and ''Z''.
Examples of cartesian closed categories include:
- The category of all Set s, with Function s as morphisms, is cartesian closed. The product ''X''×''Y'' is the cartesian product of ''X'' and ''Y'', and ''Z''''Y'' is the set of all functions from ''Y'' to ''Z''. The adjointness is expressed by the following fact: the function ''f'' : ''X''×''Y'' → ''Z'' is naturally identified with the function ''g'' : ''X'' → ''Z''''Y'' defined by ''g''(''x'')(''y'') = ''f''(''x'',''y'') for all ''x'' in ''X'' and ''y'' in ''Y''.
- The category of Finite sets, with functions as morphisms, is cartesian closed for the same reason.
- If ''G'' is a Group , then the category of all ''G''-sets is cartesian closed. If ''Y'' and ''Z'' are two ''G''-sets, then ''Z''''Y'' is the ''G''-set of Equivariant Map s from ''Y'' to ''Z'' with trivial ''G'' action (an ''G''-equivariant map from ''Y'' to ''Z'' is by definition an application ''f'' : ''Y'' → ''Z'' such that ''g''.(''f''(''y'')) = ''f''(''g''.''y'') for every ''g'' in ''G'' and ''y'' in ''Y'').
- The category of finite ''G''-sets is also cartesian closed.
- The category of all small categories (with functors as morphisms) is cartesian closed; the exponential ''C''''D'' is given by the Functor Category consisting of all functors from ''D'' to ''C'', with Natural Transformation s as morphisms.
- If ''C'' is a Small Category , then the Functor Category ''C'' consisting of all covariant functors from ''C'' into the category of sets, with Natural Transformation s as morphisms, is cartesian closed. If ''F'' and ''G'' are two functors from ''C'' to , then the exponential ''F''''G'' is the functor whose value on the object ''X'' of ''C'' is given by the set of all natural transformations from (''X'',−) × ''G'' to ''F''.
- --- The earlier example of ''G''-sets can be seen as a special case of functor categories: every group can be considered as a one-object category, and ''G''-sets are nothing but functors from this category to
- --- The category of all Directed Graphs is cartesian closed; this is a functor category as explained under Functor Category .
- In Hausdorff Space s is cartesian closed, as is the category of Frölicher Space s.
- If ''X'' is a Topological Space , then the Open Set s in ''X'' form the objects of a category O(''X'') for which there's a unique morphism from ''U'' to ''V'' if ''U'' is a subset of ''V'' and no morphism otherwise. This category is cartesian closed; the "product" of ''U'' and ''V'' is the intersection of ''U'' and ''V'' and the exponential ''U''''V'' is the Interior of ''U''∪(''X''\''V'').
The following categories are ''not'' cartesian closed:
- The category of all Vector Space s over some fixed Field is not cartesian closed, neither is the category of all Finite-dimensional vector spaces. While they have products (called direct sums), the product functors don't have right adjoints.
- The category of Abelian Group s is not cartesian closed, for the same reason.
In cartesian closed categories, a "function of two variables" (a morphism ''f'':''X''×''Y'' → ''Z'') can always be represented as a "function of one variable" (the morphism λ''f'':''X'' → ''Z''''Y''). In Computer Science applications, this is known as Currying ; it has led to the realization that simply-typed Lambda Calculus can be interpreted in any cartesian closed category.
Certain cartesian closed categories, the Topoi , have been proposed as a general setting for mathematics, instead of traditional Set Theory .
The renowned computer scientist John Backus has advocated a variable-free notation, or Function-level Programming , which in retrospect bears some similarity to the internal language of cartesian closed categories. CAML is more consciously modelled on cartesian closed categories.
In every cartesian closed category (using exponential notation), (''X''''Y'')''Z'' and (''X''''Z'')''Y'' are isomorphic for all objects ''X'', ''Y'' and ''Z''. We write this as the "equation"
:(''x''''y'')''z'' = (''x''''z'')''y''
What other such equations are valid in all cartesian closed categories? It turns out that all of them follow logically from the following axioms:
- ''x''×(''y''×''z'') = (''x''×''y'')×''z''
- ''x''×''y'' = ''y''×''x''
- ''x''×1 = ''x'' (here 1 denotes the terminal object of ''C'')
- 1''x'' = 1
- ''x''1 = ''x''
- (''x''×''y'')''z'' = ''x''''z''×''y''''z''
- (''x''''y'')''z'' = ''x''(''y''×''z'')
|
