ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 32
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. An Introduction to Category Theory
|
| 2.1. The Definition of a Category
|
| A "category" is an abstraction of "sets and functions between them". In a
| category sets become "objects", abstract things with no internal structure.
| There 'are' sets in the theory, however, namely, for each two objects X, Y
| there is a set of "morphisms" from X to Y. These morphisms compose in an
| associative way, and there are identity morphisms. The motivating examples
| for us are (2) and (3) below. Here, then, is the precise definition:
|
| 1. Definition. A 'category' C
| is given by data (1, 2, 3)
| subject to axioms (a, b, c)
| as follows:
|
| Datum 1. A collection ob(C) of C-'objects' X, Y, Z, ... .
|
| Datum 2. For each ordered pair of objects (X, Y) a set C(X, Y)
| of C-'morphisms' from X to Y. We use the term 'map'
| as a synonym for morphism.
|
| Axiom a. The sets C(X, Y) are disjoint:
|
| If C(X, Y) |^| C(X', Y') =/= 0,
|
| then X = X' and Y = Y'.
|
| We will rarely say f is in C(X, Y), introducing
| instead the following two synonymous notations:
|
| f : X -> Y
|
| f
| X -----> Y
|
| Here X is called the 'domain' of f
| and Y is called the 'codomain' of f.
| Axiom (a) guarantees that this definition
| makes sense, that is, there will never be
| any ambiguity concerning the domain or the
| codomain of a morphism.
|
| Datum 3. A composition operator 'o' assigning to each ordered pair
| of morphisms (f, g) of form f : X -> Y, g : Y -> Z (i.e.,
| the codomain of f coincides with the domain of g) a third
| morphism g o f : X -> Z whose domain is that of f and whose
| codomain is that of g.
|
| Axiom b. Composition is associative, that is, given
|
| f : X -> Y,
|
| g : Y -> Z,
|
| h : Z -> W,
|
| we have that
|
| (h o g) o f = h o (g o f) : X -> W.
|
| Axiom c. For each object X there exists an
| 'identity' morphism id_X : X -> X with
| domain and codomain X and with the property
|
| that for each morphism f : Y -> X,
|
| id_X o f = f,
|
| and for each morphism g : X -> Z,
|
| g o id_X = g.
|
| This completes the definition. We observe at once
| that the id_X of axiom (c) is unique. For suppose
| also that u : X -> X satisfies u o f = f for all
| f : Y -> X and g o u = g for all g : X -> Z.
| Regarding id_X as g for u, id_X o u = id_X.
| Regarding u as f for id_X, id_X o u = u.
| Thus u = id_X. Hence id_X is well named
| as 'the' identity morphism of X.
|
| As is usual for mathematical structures generally,
| a host of alternate notations may prove useful. Thus,
| composition might be denoted g * f instead of g o f for
| some categories. Since composition is the basic operation
| of category theory we shall most often write composition with
| no symbol at all, as gf. We shall almost always stick to id_X
| for the identity morphism of X. Even in our first examples,
| different categories may share the same objects and even
| the same morphisms. In such situations different arrows
| such as f : X -» Y may be used and alternate notation
| for composition may be essential.
|
| Manes & Arbib, AAPS, pages 39-40.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤