(unknown)

[nobody@nowhere.invalid (Unknown)]

<cat-dist@mta.ca> Envelope-to: categories-list@mta.ca
Delivery-date: Tue, 01 Jun 2004 08:40:09 -0300 Received: from
Majordom by mailserv.mta.ca with local (Exim 4.10)
    id 1BV7aG-0000eY-00
    for categories-list@mta.ca; Tue, 01 Jun 2004 08:37:32 -0300
Mime-Version: 1.0 (Apple Message framework v613)
To: categories@mta.ca
Message-Id: <CBA97319-B35F-11D8-A257-000D9367EB64@vuw.ac.nz>
Content-Type: multipart/alternative; boundary=Apple-Mail-6-367120408
From: Rob Goldblatt <Rob.Goldblatt@vuw.ac.nz>
Subject: categories: preprint on behavioural covarieties
Date: Tue, 1 Jun 2004 12:08:22 +1200
Content-Transfer-Encoding: quoted-printable
Content-Type: text/plain;charset=ISO-8859-1;format=flowed
Sender: cat-dist@mta.ca
Precedence: bulk
Status: RO
X-Status:
X-Keywords:
X-UID: 1

A preprint of a paper entitled

"A comonadic account of behavioural covarieties of coalgebras"

is available for downloading as a pdf file from

www.mcs.vuw.ac.nz/~rob

Rob Goldblatt


ABSTRACT:
A class K of coalgebras for an endofunctor T on the category of sets is=20=

a behavioural covariety if it is closed under disjoint unions and=20
images of bisimulation relations (hence closed under images and domains=20=

of coalgebraic morphisms, including subcoalgebras). K may be thought of=20=

as the class of all coalgebras that satisfy some computationally=20
significant property. In any logical system suitable for specifying=20
properties of state-transition systems in the Hennessy-Milner style,=20
each formula will define a class of models that is a behavioural=20
variety.

  Assume that the forgetful functor on T-coalgebras has a right adjoint,=20=

providing for the construction of cofree coalgebras, and let G^T be the=20=

comonad arising from this adjunction. Then we show that behavioural=20
covarieties K are (isomorphic to) the Eilenberg-Moore categories of=20
coalgebras for certain comonads G^K naturally associated with G^T.=20
These are called pure subcomonads of G^T, and a categorical=20
characterization of them is given, involving a pullback condition on=20
the naturality squares of a transformation from G^K to G^T.

  We show that=A0 there is a bijective correspondence between =
behavioural=20
covarieties of T-coalgebras and isomorphism classes of pure subcomonads=20=

of G^T.


 =20=