ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 38
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. An Introduction to Category Theory
|
| 2.2. Isomorphism, Duality, and Zero Objects (cont.)
|
| 5. Definition. Two objects X, Y in a category C are 'isomorphic' if
| there exists an isomorphism f : X -> Y. This is written X ~=~ Y.
|
| 6. Observation. Isomorphism is an equivalence relation on ob(C).
|
| Proof. id_X : X -> X is an isomorphism with (id_X)^-1 = id_X,
| so that X ~=~ X and isomorphism is 'reflexive'. If f : X -> Y
| is an isomorphism, so is f^-1 : Y -> X, so that isomorphism is
| 'symmetric'. To see that 'transitivity' holds, if f : X -> Y
| and g : Y -> Z are isomorphisms, then:
|
| (g f)(f^-1 g^-1) = g (f f^-1) g^-1 = g g^-1 = id_Z
|
| and (f^-1 g^-1)(g f) = id_X similarly
|
| so that gf is an isomorphism (and (gf)^-1 = f^-1 g^-1). þ
|
| As a rule, definitions and constructions in category theory
| (beginning with (7) below; see Theorem 8) are not unique
| but are "unique up to isomorphism". Thus, a major aspect
| of the philosophy of category is that "isomorphism"
| formalizes "abstractly the same".
|
| Each theorem of category theory has a "dual theorem" whose
| proof is an automatic consequence of the original, obtained
| by "reversing the arrows". Before giving the general notion
| of duality, we explore the motivating duality of initial and
| terminal objects.
|
| 7. Definition. An object A in a category C is 'initial' if
| for every object X there exists exactly one morphism from
| A to X. We denote this unique morphism by ! : A -> X.
|
| The next result, simple as its proof may be, is one of the most
| fundamental in category theory, because it turns out that many
| important constructs can be shown to be equivalent to initial
| objects in suitable categories.
|
| 8. Theorem. If A and B are both initial objects in a category C
| then ! : A -> B is an isomorphism. Thus, if C has an initial
| object it is unique up to a unique isomorphism.
|
| Proof. As any two morphisms from A to A are equal,
| similarly B to B, the following diagram commutes:
|
| !
| A o---------->o B
| \ |\
| \ | \
| \ | \
| \ | \
| \ ! | \
| id_A \ | \ id_B
| \ | \
| \ | \
| \ | \
| \ | \
| vv v
| A o---------->o B
| !
|
| 9. Example. The empty set Ø is initial in Pfn with ! : Ø -> X
| being the totally undefined function. Since this function is
| total (else it would be undefined on some element of Ø) we have
| that Ø is also initial in Set. Thus, ! : Ø -> X is not only the
| unique partial function but also the unique multifunction (by 1.4.3)
| so Ø is again the initial object of Mfn and ANMfn.
|
| Manes & Arbib, AAPS, page 48.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤