relation lifting and abstract relational bisimulation ommited
This commit is contained in:
partowp
+68
-26
@@ -687,9 +687,17 @@ Now, we prove $Sg(\mu') = \nu$.
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
\end{definition}
|
||||
|
||||
%
|
||||
\begin{definition}[Jointly Monic]
|
||||
A pair of morphisms $p_1\c R\to X$ and $p_2\c R\to Y$ is jointly monic iff for every pair of morphisms $f,g\c A \to R$ assuming that $p_1\comp f=p_1\comp g$ and $p_2\comp f=p_2\comp g$ then $f=g$.
|
||||
\end{definition}
|
||||
%
|
||||
\begin{prop}
|
||||
In a category $\BC$ with products, two morphisms $p_1\c R\to X$ and $p_2\c R \to Y$ are jointly monic iff $\brks{p_1,p_2}\c R\to X\times Y$ is monic.\qed
|
||||
\end{prop}
|
||||
%
|
||||
\begin{definition}[Category of Relations]
|
||||
For an arbitrary category $\BC$\sgnote{In this definition $\BC$ is not arbitrary -- it must have products. But this can be fixed by reformulating in terms of joint monics.}, the category of relations, denoted by $\rel(\BC)$ has as objects such spans $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ that $\brks{p_1,p_2}$ is a monomorphism. A morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ are objects in $\rel(\BC)$ as well, and $(g_1,g_2,w)$ is a morphism in $\spa(\BC)$.
|
||||
For an arbitrary category $\BC$\sgnote{In this definition $\BC$ is not arbitrary -- it must have products. But this can be fixed by reformulating in terms of joint monics.}, the category of relations, denoted by $\rel(\BC)$ has as objects such spans $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ that $\brks{p_1,p_2}$ is a monomorphism. A morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ are objects in $\rel(\BC)$ as well, and $g_1$ and $g_2$ are jointly monic.
|
||||
\end{definition}
|
||||
%
|
||||
%\begin{prop}
|
||||
@@ -1194,25 +1202,25 @@ So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \sta
|
||||
In an arbitrary category $\BC$, a span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{Aczel-Mendler bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\spa(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$.
|
||||
\end{definition}
|
||||
%
|
||||
\begin{definition}[Relation Lifting]
|
||||
Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, whenever the following diagram commutes:
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
\rel(\BC) \&\& \rel(\BC) \\
|
||||
{\BC\times\BC} \&\& {\BC\times\BC}
|
||||
\arrow["{\rel(F)}", from=1-1, to=1-3]
|
||||
\arrow["{U}"',from=1-1, to=2-1]
|
||||
\arrow["{U}",from=1-3, to=2-3]
|
||||
\arrow["{F\times F}"', from=2-1, to=2-3]
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
\end{definition}
|
||||
\begin{definition}[Abstract Relational Bisimulation]\label{def:abs-rel-bis}
|
||||
In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{abstract relational bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{\rel(F)p_1}{\leftarrow} \rel(F)R \stackrel{\rel(F)p_2}{\to}FY)$.
|
||||
\end{definition}
|
||||
The given definition is highly abstract. There is a relation lifting that abstracts Barr-relators that are known to be well-behaved relators, and it also gives an interesting notion of bisimulation, called \emph{Hermida-Jacobs bisimulation}.
|
||||
%\begin{definition}[Relation Lifting]
|
||||
% Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, whenever the following diagram commutes:
|
||||
% \begin{equation*}
|
||||
% \begin{tikzcd}[ampersand replacement=\&]
|
||||
% \rel(\BC) \&\& \rel(\BC) \\
|
||||
% {\BC\times\BC} \&\& {\BC\times\BC}
|
||||
% \arrow["{\rel(F)}", from=1-1, to=1-3]
|
||||
% \arrow["{U}"',from=1-1, to=2-1]
|
||||
% \arrow["{U}",from=1-3, to=2-3]
|
||||
% \arrow["{F\times F}"', from=2-1, to=2-3]
|
||||
% \end{tikzcd}
|
||||
% \end{equation*}
|
||||
%\end{definition}
|
||||
%\begin{definition}[Abstract Relational Bisimulation]\label{def:abs-rel-bis}
|
||||
% In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{abstract relational bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{\rel(F)p_1}{\leftarrow} \rel(F)R \stackrel{\rel(F)p_2}{\to}FY)$.
|
||||
%\end{definition}
|
||||
%The given definition is highly abstract. There is a relation lifting that abstracts Barr-relators that are known to be well-behaved relators, and it also gives an interesting notion of bisimulation, called \emph{Hermida-Jacobs bisimulation}.
|
||||
%
|
||||
The lifting is using the image factorization in regular categories. %\ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.}
|
||||
% The lifting is using the image factorization in regular categories. %\ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.}
|
||||
%
|
||||
%\begin{equation*}
|
||||
% \begin{tikzcd}[ampersand replacement=\&]
|
||||
@@ -1222,18 +1230,52 @@ The given definition is highly abstract. There is a relation lifting that abstra
|
||||
% \arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
|
||||
% \end{tikzcd}
|
||||
%\end{equation*}
|
||||
For a regular category $\BC$, we define a functor of type $(-)^\clubsuit\c\spa(\BC)\to\rel(\BC)$. It takes every span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the image of its legs:
|
||||
|
||||
By applying the functor $F$ on all of the components of $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ that is an object of $\spa(\BC)$ we get another object of $\spa(\BC)$, but it is not the case for $\rel(\BC)$. As an example, if we set $F$ to be the powerset functor $\powf$, then $(\powf X \stackrel{\powf p_1}{\leftarrow} \powf R \stackrel{\powf p_2}{\to}\powf Y)$ is not necessarily a relation anymore because if we take $R=\{(1,0),(0,1),(0,0),(1,1)\}$, and define functions $f\c R\to \powf R$ and $g\c R\to \powf R$ as
|
||||
\begin{gather*}
|
||||
f(w)=
|
||||
\begin{cases}
|
||||
\{(1,0),(0,1),(0,0),(1,1)\} & w=(0,0) \\
|
||||
R & otherwise
|
||||
\end{cases}\\
|
||||
g(w)=
|
||||
\begin{cases}
|
||||
\{(1,0),(0,1),(0,0)\} & w=(0,0) \\
|
||||
R & otherwise
|
||||
\end{cases}
|
||||
\end{gather*}
|
||||
then $\powf p_1\comp f=\powf p_1\comp g$ and $\powf p_2\comp f=\powf p_2\comp g$ hold, but $f\neq g$. So, $\powf p_1$ and $\powf p_2$ are not jointly monic.
|
||||
% For a regular category $\BC$, we define a functor of type $(-)^\clubsuit\c\spa(\BC)\to\rel(\BC)$. It takes every span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the image of its legs:
|
||||
%
|
||||
% \begin{equation*}
|
||||
% \begin{tikzcd}[ampersand replacement=\&]
|
||||
% R \& {R^\clubsuit} \&\& {X\times Y}
|
||||
% \arrow["{e_R}"', two heads, from=1-1, to=1-2]
|
||||
% \arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
|
||||
% \arrow["{\brks{p^\clubsuit_1,p^\clubsuit_2}}"', tail, from=1-2, to=1-4]
|
||||
% \end{tikzcd}
|
||||
% \end{equation*}
|
||||
% Also, for every functor $F\c\BC\to\BC$ we have a trivial lifting to $\spa(\BC)$ that takes every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$, and every morphism $(f,g,w)$ to $(Ff,Fg,Fw)$, and we denote it with $\spa(F)$. Since $\rel(\BC)$ is a subcategory of $\spa(\BC)$, we have an inclusion functor $I\c\rel(\BC)\to\spa(\BC)$ as well.
|
||||
% So, given a functor $F\c\BC\to\BC$ we define its lifting $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ as $(F-)^\dagger=(\spa(F)I-)^\clubsuit$. The functor $(F-)^\dagger$ takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation:
|
||||
% \begin{equation*}
|
||||
% \begin{tikzcd}[ampersand replacement=\&]
|
||||
% \& {(FR)^\dagger} \& \\
|
||||
% FX \&\& FY \\
|
||||
% \& {FX\times FY}
|
||||
% \arrow["{{{(Fp_1)^\dagger}}}"', from=1-2, to=2-1]
|
||||
% \arrow["{{{(Fp_2)^\dagger}}}", from=1-2, to=2-3]
|
||||
% \arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2]
|
||||
% \end{tikzcd}
|
||||
% \end{equation*}
|
||||
To cope with this, we assume $\BC$ to be a regular category, so we have the following epi-mono decomposition for every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\spa(\BC)$:
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
R \& {R^\clubsuit} \&\& {X\times Y}
|
||||
R \& {R^\dagger} \&\& {X\times Y}
|
||||
\arrow["{e_R}"', two heads, from=1-1, to=1-2]
|
||||
\arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
|
||||
\arrow["{\brks{p^\clubsuit_1,p^\clubsuit_2}}"', tail, from=1-2, to=1-4]
|
||||
\arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
Also, for every functor $F\c\BC\to\BC$ we have a trivial lifting to $\spa(\BC)$ that takes every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$, and every morphism $(f,g,w)$ to $(Ff,Fg,Fw)$, and we denote it with $\spa(F)$. Since $\rel(\BC)$ is a subcategory of $\spa(\BC)$, we have an inclusion functor $I\c\rel(\BC)\to\spa(\BC)$ as well.
|
||||
So, given a functor $F\c\BC\to\BC$ we define its lifting $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ as $(F-)^\dagger=(\spa(F)I-)^\clubsuit$. The functor $(F-)^\dagger$ takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation:
|
||||
We can define $(-)^\dagger$ as a functor from $\spa(\BC)\to\rel(\BC)$ that takes $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(X \stackrel{p^\dagger_1}{\leftarrow} R^\dagger \stackrel{p^\dagger_2}{\to}Y)$, then we define $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ to take $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ to the following relation:
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
\& {(FR)^\dagger} \& \\
|
||||
|
||||
Reference in New Issue
Block a user