Categories

Download

categories-list@categories.org.au

November 1990

2 participants
1 discussions

Homotopy = homobject
by Vaughan Pratt 14 Nov '90

14 Nov '90

Cellular geometry arises both with categories, starting with Ehresmann's 1965 notion of an n-category, and with concurrency as per my POPL-91 paper and also as per a paper that David Murphy just brought to my attention, ``Deterministic Asynchronous Automata,'' Mike Shields, Proc. Formal Models in Programming (Ed. E.Neuhold, G.Choust), Elsevier 1985. I'm not sure who in category-land cares about homotopy in n-categories, but it is the basis for distinguishing true from false nondeterminism in my POPL paper. As David points out to me, a special case of homotopy can be found in Mazurkiewicz's independence relation: the independence of a and b should be identified with the paths ab and ba being homotopic, as in a|b. In ab+ba however these two paths are not homotopic: one has to decide which of the ab or ba paths one is going to follow. While the following is obviously too cryptic for general consumption, I am mentioning the idea here for two reasons: to mumble my obscure thought processes concerning true nondeterminism out loud on the concurrency and category lists, and to find out if this definition of homotopy as homobject rings a bell with anyone. It seems so obvious that I am fully expecting it to have been around for decades, at least somewhere. It just isn't in the places I've looked so far. If it is spelled out somewhere, any attempt on my part to expand on the mumbling below may not be necessary. Here's the idea. It seems to me that a very natural definition of homotopy is arrived at by identifying homotopy with homobject, in the enriched category sense. That is, the homotopy of the paths from x to y is the homobject ?x,y?, or d(x,y) in the notation of Casley et al, CTCS-89, Manchester, LNCS 389, the "distance" from point x to point y. (The basic law governing homobjects is the abstract triangle inequality, which is why it is appropriate to think of the homobject ?x,y? as an abstract distance d(x,y). This view is due to Lawvere 1974.) Hence homotopy is governed principally by the triangle inequality, the basic law of enriched category theory. In this sense the homotopy from x to y and the distance from x to y become the same thing. The homotopy of an ordinary category is discrete because its homobjects are sets. The homotopy of a set is nonexistent because sets don't have homobjects worth mentioning (all points are equidistant). The homotopy of a poset is trivial because its homobjects contain either no elements (i.e. paths) or one. The intuitive notion of homotopy as an equivalence relation on paths arises for categories whose homobjects are equivalence relations; then ?x,y? is a set (X,^) of paths and an equivalence ^ on paths whose blocks are the homotopy classes. However it would seem nicer to take arbitrary categories for homobjects, the homotopy of a 2-category. The homotopy of an order-enriched category lies between that of categories and 2-categories. The simplest case of this arises for a monoid (1-object category), the basis for my recently developed "action logic" ACT (pub/jelia.{tex,dvi} via ftp from boole.stanford.edu) Action logic is accessible to anyone who understands lattice theory, and employs no categorical language or explicit categorical concepts, yet it contains interesting homotopy in the above sense, in a way that Boolean logic and intuitionistic logic as cartesian closed posets do not. In a closed category homotopy is internalized just like a homobject, via exponentiation/implication. That is, the entire homotopy ?x,y? can be compressed into the single point b?a or a=>b as its internal representation. The homotopy so coded can then be recovered as the homotopy from I (the unit of the closed category) to that point, via the isomorphism between ?I,a=>b? and ?a,b?. Thus isomorphic copies of all homotopy present in a closed category can be found radiating out from its unit. In the case of action logic the homotopies so radiating out from I (called 1 there) are exactly the theorems of action logic. I know the above must look to many of you rather unrelated to the traditional geometry of triangles, circles, and squares. Hopefully someone will someday volunteer to draw enough pretty pictures of this really very simple notion of homotopy to dispel any remaining mystery about it. You will find a few such pictures at the end of the action logic paper, of paths with fixed endpoints sweeping across surfaces, which should fit right in with any prior intuition you had about homotopy. Vaughan Pratt

2 1