ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 42
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. An Introduction to Category Theory
|
| 2.2. Isomorphism, Duality, and Zero Objects (cont.)
|
| Before introducing zero objects we consider the more general concept of
| zero morphisms which abstract from "totally undefined" morphisms in Pfn.
|
| 16. Definition. Let C be any category, and let 0_XY
| in C(X, Y) be given for each X and Y. Say that
| (0_XY) is a 'family of zero morphisms' if for
| every f : W -> X and g : Y -> Z we have:
|
| 0_WZ
| W o------------------->o Z
| | |
| | |
| | |
| f | | g
| | |
| | |
| v v
| X o------------------->o Y
| 0_XY
|
| On taking f or g equal to the identity, we see that this amounts to
| saying that "any composition which has a zero factor is itself zero".
| Set does not have a family of zero morphisms because Set(X, Ø) is empty
| whenever X =/= Ø. When a family of zero morphisms does exist, however,
| it is unique since if (0_XY), (Z_XY) are both families of zero morphisms:
|
| Z_XY = id_Y Z_XY (0_XX id_X) = (id_Y Z_XY) 0_XX id_X = 0_XY.
|
| We often write 0 : X -> Y for 0_XY : X -> Y if no confusion would arise.
|
| 17. Example. In Pfn, Mfn, and ANMfn,
| the totally undefined functions:
|
| ¡ !
| 0_XY = X ---> Ø ---> Y
|
| yield a family of zero morphisms.
|
| This example motivates the next definition and proposition.
|
| 18. Definition. A 'zero object' in a category C
| is an object that is both initial and terminal.
| We denote a zero object by 0, the same symbol
| as for an initial object. Though arbitrary,
| the convention is standard.
|
| 19. Proposition. A category with a zero object has zero morphisms.
| In a category with zero morphisms, each initial object is also
| a zero object and each terminal object is also a zero object.
|
| Proof. For the first statement,
| let 0 be a zero object and define:
|
| ¡ !
| 0_XY = X ---> 0 ---> Y.
|
| Then the following diagram commutes:
|
| ¡ 0 !
| W o----->o----->o Z
| | ^ \ |
| | / \ |
| f | / \ | g
| | / ¡ ! \ |
| | / \ |
| v/ vv
| X o o Y
|
| so (0_XY) is a family of zero morphisms.
|
| For the second statement, let zero morphisms exist
| and let 0 be an initial object. There exists at
| least one morphism X -> 0, namely, 0. As 0 is
| initial, 0 : 0 -> 0 is id_0 : 0 -> 0, so if
| f : X -> 0 is arbitrary, we have:
|
| f = id_0 f = 0f = 0.
|
| This shows that 0 is terminal.
| That a terminal object is initial
| is simply the dual statement. þ
|
| 20. Example. Pfn, Mfn, and ANMfn have Ø as zero object.
| The construction in Example 17 follows the proof of
| Theorem 19.
|
| In Pfn, we have said f : X -> Y is total iff DD(f) = X, that is,
| f(x) is defined for every x in X. In the same spirit, say that
| f : X -> Y in Mfn or ANMfn is total if f(x) =/= Ø for all x in X.
| It is easy to prove (work Exercise 7!) that these definitions are
| unified by the following abstract one.
|
| 21. Definition. Let C be a category with sero morphisms.
| Say that f : X -> Y is 'total' if, whenever t : T -> X,
| we have that t =/= 0 implies ft =/= 0.
|
| 22. Proposition. Let C be a category
| with zero morphisms and let
| f : X -> Y, g : Y -> Z.
| Then:
|
| 1. If f, g are total, so is gf : X -> Z.
|
| 2. If gf is total, so is f.
|
| Proof.
|
| 1. If t =/= 0 then ft =/= 0 so g(ft) = (gf)t =/= 0.
|
| 2. If t =/= 0 then (gf)t =/= 0 so g(ft) =/= 0.
| Since g0 = 0, ft =/= 0.
|
| þ
|
| Manes & Arbib, AAPS, pages 51-52.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤