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

ONT Re: Higher Order Categorical Logic -- Discussion


o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

HOC.  Discussion Note 8

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

MW = Matthew West

MW: First, thank you for this excellent tutorial.
    Even I can more or less follow you.

Matthew,

Thanks, and I will share the thanks all round,
as this form of semi-auto-tutorial is largely
dependent on penetrating questions from the
participants to see through the f o g.

MW: Can I chip in a question here.  You talk about
    structure-preserving functions below.  Is that
    the same as an isomorphism?  If not what is
    the difference?

The full official name of a morphism is a "homomorphism",
which was chosen to suggest "same form, more or less",
whereas "isomorphism" means "same form, exactly".

An "isomorphism" f : X -> Y is a special case of
a homomorphism from X to Y where f is "bijective",
that is, in some of the other language that gets
used here, f is both "injective" ("one-to-one")
and "surjective" ("onto").  (That's the English
"onto", not the Greek "onto-", by the way.)

That's how one thinks of it in concrete categories,
anyway, where the objects are just garden variety
sets and all the arrows are ordinary functions.
In categories more abstractly viewed, that is,
purely in terms of the axiomatic properties
that they exemplify, it is usual to give
more elegant definitions of isomorphism.

Lambek & Scott give an abstract definition of isomorphism on page 7.

HOC.    http://suo.ieee.org/ontology/thrd36.html#03373
HOC 6.  http://suo.ieee.org/ontology/msg03381.html

L&S: | Definition 1.5.  An arrow f : A -> B in a category
     | is called an 'isomorphism' if there is an arrow
     | g : B -> A such that gf = 1_A and fg = 1_B.
     | One writes A ~=~ B to mean that such an
     | isomorphism exists and says that
     | A is 'isomorphic' with B.

For instance, look at the example of a concrete morphism that I gave next:

HOC Discussion.    http://suo.ieee.org/ontology/thrd37.html#05262
HOC Discussion 7.  http://suo.ieee.org/ontology/msg05268.html

Here we have a morphism f : X -> Y, where X is an infinite set
and Y is a finite set, so f can't possibly be an isomorphism.

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
http://www.cs.bsu.edu/homepages/mighty/history.html
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o