From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4925 Path: news.gmane.org!not-for-mail From: Steve Vickers Newsgroups: gmane.science.mathematics.categories Subject: Re: Decidability of the theory of a monad Date: Thu, 04 Jun 2009 11:59:12 +0100 Message-ID: Reply-To: Steve Vickers NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1244163037 7275 80.91.229.12 (5 Jun 2009 00:50:37 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 5 Jun 2009 00:50:37 +0000 (UTC) To: Andrej Bauer , Original-X-From: categories@mta.ca Fri Jun 05 02:50:35 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1MCNdj-0007tO-Fu for gsmc-categories@m.gmane.org; Fri, 05 Jun 2009 02:50:35 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1MCN2W-0006hQ-88 for categories-list@mta.ca; Thu, 04 Jun 2009 21:12:08 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:4925 Archived-At: Dear Andrej, It seems to me that the monad-on-a-category freely generated by one object should be the simplicial category Delta, following from the facts that Delta contains the universal monoid and a monad on C is a monoid in C^C - see Mac Lane Cats for Working Mathematician Section VII.5, VII.6. The object n of Delta will correspond to T^n(X) where T is the (functor for the) monad and X the generating object. If I've got that right then I would presume it's already known and proved carefully somewhere. After that, the monad-on-a-category freely generated by a category C would seem to be CxDelta. (Object (X,n) represents T^n(X), morphism (f,s): (X,m) -> (Y,n) corresponds to T^m(f);s(Y): T^m(X) -> T^m(Y) -> T^n(Y) and using naturality of T to deduce that s(Y);T^n(g) = T^m(g);s(Z) so the f's can always be shunted to the left.) Again, if I've got that right then it wouldn't surprise me to find it's already known. This would suggest that C |-> CxDelta is a monad on Cat. Then a monad on C is a structure morphism CxDelta -> C, i.e. Delta -> C^C with appropriate properties, which looks like a monoid in C^C, which we knew already. I don't know Knuth-Bendix well enough to understand the issues there. But since you mention various orderings, that reminds me of Freyd's trick in "essentially algebraic" presentations of these cartesian theories. (Amongst theories of partial operators, it is the cartesian theories that have good universal algebraic properties.) That involves ordering the operators so that, for each one, its domain of definition is defined by equations involving "earlier" operators. (Ultimately that comes down to total operators, for which no equations are needed.) Then the equations s = t are understood in the sense "if s and t are both defined, then they are equal". I don't know if that can be accommodated in Knuth-Bendix as it stands. In particular, I don't know how amenable K-B is to incorporating conditional rewrites. Conditional equations seem inevitable in cartesian theories; the essentially algebraic formulation reduces them to definedness explicitly conditional on equations, and equations implicitly conditional on definedness. You might want to look at my paper with Palmgren, which unifies them by identifying definedness with self-equality. You ask whether a free "monad on a category" is the same as a "free monad" on "free category". Of course, in using the word "free" one ought to be careful what kind of structure these are free over, but generally speaking if the forgetful functors compose then so will their left adjoints, the free functors. Best wishes, Steve. Andrej Bauer wrote: > Consider the theory of a monad, i.e., the axioms are those of a > category and a monad given as a triple: an operation T on objects, for > each object A a morphism eta_A : A -> T A, and an operation lift_{A,B} > which maps morphisms f : A -> T B to lift f : T A -> T B. Concretely, > the axioms are (where lift f is written f* and composition is > juxtaposition): > > id f = f > f id = f > (f g) h = f (g h) > eta* = id > f* eta = f > (f* g)* = f* g* > > Presumably, the equational theory (with partial operations) of such a > triple is decidable. Is this known? If we ignore the types and > partiality, we can attempt to turn the above equations into a > confluent terminating rewrite system using the Knuth-Bendix algorithm, > but it gets stuck (on various orderings I tried). > > A more categorical way of asking the same question is: what is a > concrete description of the free "monad on a category" (is this the > same as "free monad" on "free category"?). > > With kind regards, > > Andrej > > > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] [For admin and other information see: http://www.mta.ca/~cat-dist/ ]