ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 40
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. An Introduction to Category Theory
|
| 2.2. Isomorphism, Duality, and Zero Objects (cont.)
|
| We are now going to place the concept of duality on a more formal footing,
| by regarding a diagram in this category C with all its arrows reversed as
| being identical to a diagram in the "opposite category" C^op. Here the
| abstraction of our general definition of a category begins to show its
| power. A function f : X -> Y from a set X to a set Y is certainly not
| to be considered as a function from Y to X, but there is nothing to
| prevent us from using the "arrow-reversed notation" f : Y -< X for
| f (using a distinctive new arrowhead) and calling this a morphism
| 'from' Y 'to' X in the new category Set^op. Here is the general
| definition.
|
| 12. Definition. Let C be a category.
| The 'dual' or 'opposite category'
| of C is the category C^op
| defined as follows:
|
| ob(C^op) = ob(C),
|
| C^op(X, Y) = C(Y, X).
|
| Taking C as the "primary" category whose arrows we write
| in the normal way f : X -> Y, we write the same morphism
| in C^op as f : Y -< X.
|
| If f in C^op(X, Y) and g in C^op(Y, Z) their composition g * f in C^op(X, Z)
| is obtained by taking the composition f o g of g in C(Z, Y) and f in C(Y, X)
| in C.
|
| f g g * f f o g
| X ---< Y ---< Z = X -------< Z = X -------< Z in C^op,
|
| where
|
| g f f o g
| Z ---> Y ---> X = Z -------> X in C.
|
| Axioms (a, b, c) for C^op follow easily from their correspondents in C.
| The identity morphisms of C^op coincide with those of C. Moreover,
| rephrasing our earlier observation that isomorphism is self-dual,
| f in C(X, Y) is an isomorphism in C if and only if the same g [f?]
| considered in C^op is an isomorphism in C^op.
|
| Proof. The following diagrams (in which equally labeled commutative diagrams)
| are equal statements in their respective categories) establish the assertion
| about isomorphisms:
|
| f f
| X o---------->o Y X o>----------o Y
| \ |\ v vv
| \ (A) | \ \ (B) | \
| \ | \ \ | \
| \ | \ \ | \
| \ g | \ \ g | \
| id_X \ | \ id_Y id_X \ | \ id_Y
| \ | \ \ | \
| \ | \ \ | \
| \ | \ \ | \
| \ | (B) \ \ | (A) \
| vv v \| \
| X o---------->o Y X o>----------o Y
| f f
|
| Clearly, C = (C^op)^op. There is nothing special about being of the form C^op.
| C^op ranges over all categories as C does. When C is a "concrete" category such
| as Set there is no guarantee that C^op will likewise have such a representation.
| Set^op is "more abstract" than Set.
|
| Manes & Arbib, AAPS, pages 49-50.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤