Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

ONT Re: Program Semantics




¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤

Note 37

¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤

| 2.  An Introduction to Category Theory
|
| 2.2.  Isomorphism, Duality, and Zero Objects
|
| This section introduces the fundamental equivalence relation of category theory,
| isomorphism.  Also discussed are duality, initial and terminal objects, as well
| as zero objects, which are simultaneously initial and terminal.  The Cartesian
| product of two sets, the set of words on a given alphabet, and the principle
| of simple recursion are all manifestations of initial or terminal objects.
|
| Isomorphisms
|
| All constructions in a category must ultimately be described entirely
| in the language of objects, morphisms, composition, and identities.
| Our first definition in this language is that of "isomorphism".
|
| 1.  Definition.  A morphism f : X -> Y in a category C
|     is an 'isomorphism' if there exists g : Y -> X
|     with gf = id_X and fg = id_Y, or, in terms of
|     a commutative diagram:
|
|             f 
|     X o---------->o Y
|        \          |\
|         \         | \
|          \        |  \
|           \       |   \
|            \    g |    \
|        id_X \     |     \ id_Y
|              \    |      \
|               \   |       \
|                \  |        \
|                 \ |         \
|                  vv          v
|                 X o---------->o Y
|                         f
|
| Such g, 'if it exists', is unique, since if also hf = id_X and fh = id_Y,
| then g = g id_Y = g(fh) = (gf)h = id_X h = h.  This proof uses the full
| force of axioms (b) and (c) in the definition of a category.  Such g,
| then, is called the 'inverse' of f and is written f^-1.
|
| 2.  Example.  In Set, f : X -> Y is an isomorphism if and only if
|     f is 'bijective', that is, f is one-one and onto.  To see this,
|     first suppose that f is an isomorphism.  If f(x) = f(x') then:
|
|     x  =  (f^-1)(f(x))  =  (f^-1)(f(x'))  =  x',
|
|     which proves that f is one-one (injective).
|
|     If y is any element of Y, then y = f((f^-1)(y)),
|     so f is onto (surjective).
|
|     Conversely, let f be injective and surjective.  If y is any element
|     of Y there exists a unique of X, call it g(y), which f maps to y.
|     Thus, f(g(y)) = y.  Since, in particular, f(g(f(x))) = f(x) and
|     f is injective, g(f(x)) = x.
|
| 3.  Example.  In Pfn, f : X -> Y is an isomorphism if and only if
|     f is a total function which is bijective.  By the first example
|     it is obvious that a bijective total function is an isomorphism.
|     Conversely, let f : X -> Y be an isomorphism.  Then (f^-1)f = id_X,
|     so that X = DD(id_X) = DD((f^-1)f) c DD(f), which implies that f is
|     a total function.  Similarly f(f^-1) = id_Y implies that f^-1 is total,
|     so f is an isomorphism in Set.
|
| 4.  Example.  In Mfn, f : X -> Y is an isomorphism if and only if f is a
|     total function which is bijective.  As in Example 3, one way is clear.
|     Conversely, let f : X -> Y be an isomorphism.
|
|     First observe that,
|
|     if y in f(x), then x in (f^-1)(y),
|
|     since f(f^-1)(y) = {y} implies that (f^-1)(y) =/= Ø,
|
|     and,
|
|     if x' in (f^-1)(y), then x' in (f^-1)f(x) = {x}, so that x' = x.
|
|     Then,
|
|     if y, y' in f(x), then x in (f^-1)(y) and y' in f(x),
|
|     so y' in f(f^-1)(y) = {y}, and so y = y'.
|
|     This proves that f is a partial function.
|     Symmetrically, f^-1 is a partial function.
|     Now use the preceding example.
|
| Manes & Arbib, AAPS, pages 46-47.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.

¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤