Re: Decidability of the theory of a monad

[Steve Lack <s.lack@uws.edu.au>]

Dear Andrej,

The free monad on a category has a well-known simple concrete description.
Let Ordf be the category of finite ordinals and order-preserving maps.
        -->
0 --> 1 <-- 2 ...
        -->
(This is sometimes called the algebraicist's simplicial category - it
contains the topologist's simplicial category as the full subcategory of
non-empty finite ordinals. Ordf is simply called Delta in Categories for the
Working Mathematician.) Ordinal sum makes Ordf into a strict monoidal
category. The object 1 is a monoid in this monoidal category, and in fact
is the "free monoid in a monoidal category", in the sense that for any
strict monoidal category C, there is a bijection between monoids in C and
strict monoidal functors from Ordf to C. (There is also a non-strict version
of this fact.)

The free "category with a monad" on a category A is the Ordf x A, with monad
having endofunctor part (n,a) |-> (n+1,a), with the obvious multiplication.

More generally, the monoidal category Ordf can be regarded as a one-object
2-category mnd, and 2-functors mnd-->K for a 2-category K, are in bijection
with monads in K. Freely adding a monad to an object of K can be seen as
left Kan extension along the unique 2-functor 1-->mnd.

Regards,

Steve Lack.


On 3/06/09 9:10 PM, "Andrej Bauer" <andrej.bauer@andrej.com> 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/ ]