ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 39
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. An Introduction to Category Theory
|
| 2.2. Isomorphism, Duality, and Zero Objects (cont.)
|
| For each construction defined in a general category C,
| the 'dual construction' is the construction obtained
| by "reversing all arrows". An intitial object is
| one admitting unique morphisms from itself, so
| the dual concept should be an object admitting
| unique morphisms to itself, and such is aptly
| called a 'terminal object'.
|
| 10. Definition. An object A in a category C is 'terminal'
| if for each object X of C there exists exactly one
| C-morphism from X to A. The unique C-morphism
| from X to A will be denoted ¡ : X -> A.
|
| As another exercise in the language of duality, consider the notion of
| an isomorphism. We saw that f : X -> Y is an isomorphism just in case
| there is a map g : Y -> X such that the following diagram commutes:
|
| g
| Y o---------->o X
| \ |\
| \ | \
| \ | \
| \ | \
| \ f | \
| id_Y \ | \ id_X
| \ | \
| \ | \
| \ | \
| \ | \
| vv v
| Y o---------->o X
| g
|
| If we reverse all of the arrows, we say that f : Y -> X
| is "the dual of an isomorphism" just in case there is a
| map g : X -> Y such that the following diagram commutes:
|
| g
| Y o<----------o X
| ^ ^^
| \ | \
| \ | \
| \ | \
| \ f | \
| id_Y \ | \ id_X
| \ | \
| \ | \
| \ | \
| \ | \
| \| \
| Y o<----------o X
| g
|
| But this just says that f is an isomorphism,
| so the concept of isomorphism is self-dual.
| With this observation, the dual of Theorem 8
| is the following:
|
| 11. Theorem. If A and B are both terminal objects in
| a category C, then ¡ : A -> B is an isomorphism.
|
| Proof. Once the concept of duality is understood,
| no proof is needed -- just reverse all arrows in
| the proof of Theorem 8. þ
|
| Manes & Arbib, AAPS, page 49.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤