Cartesian closed category

Cartesian closed category

In category theory, a category is cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in that they provide a natural setting for lambda calculus. For generalizations of this notion to monoidal categories, see closed monoidal category.

Definition

The category "C" is called cartesian closed 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-sets:mathrm{Hom}(X imes Y,Z) cong mathrm{Hom}(X,Z^Y)which is natural in both "X" and "Z".

If a category is such that all its slice categories are cartesian closed, then it is called locally cartesian closed.

Examples

Examples of cartesian closed categories include:
* The category Set of all sets, with functions 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 curried 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 set of all functions from "Y" to "Z" with "G" action defined by ("g"."F")("y") = "g".(F("g""-1".y)) for all "g" in "G", "F":"Y" → "Z" and "y" in "Y".
* The category of finite "G"-sets is also cartesian closed.
* The category Cat 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 transformations as morphisms.
* If "C" is a small category, then the functor category Set"C" consisting of all covariant functors from "C" into the category of sets, with natural transformations as morphisms, is cartesian closed. If "F" and "G" are two functors from "C" to Set, 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 Set
** The category of all directed graphs is cartesian closed; this is a functor category as explained under functor category.
* In algebraic topology, cartesian closed categories are particularly easy to work with. Neither the category of topological spaces with continuous maps nor the category of smooth manifolds with smooth maps is cartesian closed. Substitute categories have therefore been considered: the category of compactly generated Hausdorff spaces is cartesian closed, as is the category of Frölicher spaces.
* In order theory, complete partial orders ("cpo"s) have a natural topology, the Scott topology, whose continuous maps do form a cartesian closed category (that is, the objects are the cpos, and the functors are the Scott continuous maps). Both currying and "apply" are continuous functions in the Scott topology, and currying, together with apply, provide the adjoint. [H.P. Barendregt, "The Lambda Calculus", (1984) North-Holland ISBN 0-444-87508-5 "(See theorem 1.2.16)"]
* A Heyting algebra is a Cartesian closed poset. An important example arises from topological spaces. If "X" is a topological space, then the open sets 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 poset is a cartesian closed category: 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 spaces 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. (They are, however, symmetric monoidal closed categories: the set of linear transformations between two vector spaces forms another vector space, so they're closed, and if one replaces the product by the tensor product, a similar isomorphism exists between the Hom spaces.)
* The category of abelian groups is not cartesian closed, for the same reason.

Applications

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.

The Curry-Howard-Lambek correspondence provides a deep isomorphism between intuitionistic logic, simply-typed lambda calculus and cartesian closed categories.

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.

Equational theory

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"

One may ask what other such equations are valid in all cartesian closed categories. It turns out that all of them follow logically from the following axioms [S. Soloviev. "Category of Finite Sets and Cartesian Closed Categories", Journal of Soviet Mathematics, 22, 3 (1983)] :
*"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")

References


Wikimedia Foundation. 2010.

Игры ⚽ Нужно сделать НИР?

Look at other dictionaries:

  • Closed category — In category theory, a branch of mathematics, a closed category is a special kind of category. In any category (more precisely, in any locally small category), the morphisms between any two given objects x and y comprise a set, the external hom (x …   Wikipedia

  • Closed monoidal category — In mathematics, especially in category theory, a closed monoidal category is a context where we can take tensor products of objects and also form mapping objects . A classic example is the category of sets, Set, where the tensor product of sets A …   Wikipedia

  • Category (mathematics) — In mathematics, a category is an algebraic structure that comprises objects that are linked by arrows . A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object. A …   Wikipedia

  • Category theory — In mathematics, category theory deals in an abstract way with mathematical structures and relationships between them: it abstracts from sets and functions to objects and morphisms . Categories now appear in most branches of mathematics and in… …   Wikipedia

  • Category of sets — In mathematics, the category of sets, denoted as Set, is the category whose objects are all sets and whose morphisms are all functions. It is the most basic and the most commonly used category in mathematics.Properties of the category of setsThe… …   Wikipedia

  • Category of topological spaces — In mathematics, the category of topological spaces, often denoted Top, is the category whose objects are topological spaces and whose morphisms are continuous maps. This is a category because the composition of two continuous maps is again… …   Wikipedia

  • Category of abelian groups — In mathematics, the category Ab has the abelian groups as objects and group homomorphisms as morphisms. This is the prototype of an abelian category.The monomorphisms in Ab are the injective group homomorphisms, the epimorphisms are the… …   Wikipedia

  • Outline of category theory — The following outline is provided as an overview of and guide to category theory: Category theory – area of study in mathematics that examines in an abstract way the properties of particular mathematical concepts, by formalising them as… …   Wikipedia

  • Product (category theory) — In category theory, the product of two (or more) objects in a category is a notion designed to capture the essence behind constructions in other areas of mathematics such as the cartesian product of sets, the direct product of groups, the direct… …   Wikipedia

  • List of category theory topics — This is a list of category theory topics, by Wikipedia page. Specific categories *Category of sets **Concrete category *Category of vector spaces **Category of graded vector spaces *Category of finite dimensional Hilbert spaces *Category of sets… …   Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”