ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 47
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. An Introduction to Category Theory
|
| 2.3. Products and Coproducts (cont.)
|
| We turn now to a description of Cartesian products that uses
| only category-theoretic language in Set. Our starting point
| is a given family (X_i : i in I) of sets. Our Definition 1
| is in terms of elements; we must think more in terms of how
| to use morphisms in Set to characterize when a set X is to be
| isomorphic to ]¯[_(i in I) X_i. To this end consider a family
| of morphisms of the form (f_i : Y -> X_i : i in I). For each
| y in Y, (f_i (y) : i in I) is an element of ]¯[_(i in I) X_i
| and so should correspond to a definite element of X, call it
| f(x). In this way there is a bijective correspondence between
| morphisms Y -> X and families of morphisms Y -> X_i. Moreover,
| when X = ]¯[_(i in I) X_i this correspondence is easily described
| in terms of commutative diagrams. To begin, we need the following
| definition:
|
| 5. Definition. For (X_i : i in I) a family of sets and j in I,
| the 'j^th projection function' is:
|
| pr_j
| ]¯[_(i in I) X_i -------> X_j, (x_i) ~> x_j.
|
| We then observe that the relationship between f and the f_i is precisely:
|
| 6.
| pr_j
| ]¯[_(i in I) X_i o------------------>o X_j
| ^ ^
| \ /
| \ /
| \ /
| f \ / f_j (for all j in I)
| \ /
| \ /
| \ /
| \ /
| o
| Y
|
| In terms of elements, (6) asserts that:
|
| f(y) = (f_i (y) : i in I)
|
| which is what we expected. We have motivated the following definition.
|
| 7. Definition. Let C be any category and let (X_i : i in I) be a family of
| objects of C. A 'product' of (X_i : i in I) is (P, (pr_i : i in I)),
| where P is an object of C and for each i in I, pr_i : P -> X_i is
| a C-morphism, all subject to the following property:
|
| Given (Y, (f_i : i in I)) with C-object Y and C-morphisms f_i : Y -> X_i,
| there exists a unique f : Y -> P such that pr_i f = f_i for all i in I,
| as shown here:
|
| pr_i
| P o------------------>o X_i
| ^ ^
| \ /
| \ /
| \ /
| f \ / f_i
| \ /
| \ /
| \ /
| \ /
| o
| Y
|
| The pr_i are called 'projection morphisms'.
|
| 8. Example. In Set, P = ]¯[_(i in I) X_i,
| with pr_i as in (5), is a product of
| (X_i : i in I). This was established
| in the discussion motivating (7).
|
| Manes & Arbib, AAPS, pages 59-60.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤