2.3.2 Système de transition comme
coalgèbre d'un foncteur.
Sur le point de vue ensembliste les systèmes de
transition sont les coalgèbres du foncteur puissance
covariant.
En effet, pour tout système ensembliste (S,
S > ), l'application : aS : S -? P (S)
qui à
tout s E S associe aS (s) = {s'
tel que s S > s'} est une co-structure du foncteur puissance
covariant P. Donc (S, aS) est une
P-coalgèbre.
Réciproquement, à toute
P-coalgèbre (S, aS) correspond un
système de transition (S, S >)
avec S> = {(s, s')
E S x S, s' E aS (s)} .
Bien évidemment, tout P-morphisme f
: S -? U est un morphisme de systèmes de transition
et réciproquement.
En effet, si f est un morphisme de
système de transition, pour tout s E S, on a :
aU o f (s) = aU (f
(s))
= {u E U, f (s) > u}
{=f (s'), s' E
S; f (s)
> f (s')} car f
réfléchit les transitions
S
= {f (s'), s' E aS
(s)} =P (f) o a, (s)
Donc aU o f = P (f) o aS.
Ce qui montre bien que f est un
P-morphisme. D'où le résultat suivant :
v
Sur la catégorie CPO, considérons la
correspondance F : CPO -? CPO définie : * Sur
les objets par F (A) = (P (A), ?)
pour tout opc A.
Résultat 2.1. Les systèmes de transition
supportés par un ensemble sont les coalgèbres du
foncteur puissance covariant
** sur les morphismes par
F (f) : (P (A),
ç) -? (P (B),ç)
X 7-? f (X) pour toute application continue
f : A -? B.
Cette correspondance définie un foncteur de CPO dans CPO.
áS n'est pas continue car pour le système de
transition ci-dessous représenté, s(a) =
{a, b} {b} = s(b); pourtant, a =
b.
T
S :: b OO T
%%
a
BB
Remarquons que le foncteur F a
été construit par analogie au foncteur puissance
covariant P qui se défini sur les objets par
P(A) = 2 pour tout ensemble A; ceci
suppose donc l'existence d'un classifiant de sous objets (c'est le cas dans ENS
où 2 = {0, 1} est un classifiant de sous
objets). Or nous n'avons pas pu construire dans la catégorie
CPO un classifiant de sous objets. nous y reviendrons dans nos
prochains travaux.
| 
