pouya/coalgebraic-simulation
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

rel

Browse Source
This commit is contained in:
partowp
2026-09-02 21:24:30 +01:00
parent eee6bfc547
commit 4dedba1ee5
1 changed files with 143 additions and 140 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+101 -98
View File
@@ -815,17 +815,16 @@ As mentioned in the previous section, there is a way to define morphisms in $\sp
\arrow["{p_2}"', from=2-1, to=2-2] \arrow["{p_2}"', from=2-1, to=2-2]
\end{tikzcd} \end{tikzcd}
\end{gather*} \end{gather*}
\end{example} For morphisms
For morphisms \begin{gather*}
\begin{gather*}
(f,g,w)\c(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(Y \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Z) (f,g,w)\c(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(Y \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Z)
\end{gather*} \end{gather*}
and and
\begin{gather*} \begin{gather*}
(g,h,v)\c(Y \stackrel{t_1}{\leftarrow} W \stackrel{t_2}{\to}Z)\to(Z \stackrel{r_1}{\leftarrow} V \stackrel{r_2}{\to}Q) (g,h,v)\c(Y \stackrel{t_1}{\leftarrow} W \stackrel{t_2}{\to}Z)\to(Z \stackrel{r_1}{\leftarrow} V \stackrel{r_2}{\to}Q)
\end{gather*} \end{gather*}
we have the following commutative diagram: we have the following commutative diagram:
\begin{equation*} \begin{equation*}
\begin{tikzcd}[ampersand replacement=\&] \begin{tikzcd}[ampersand replacement=\&]
\&\& {R\odot W} \&\& \\ \&\& {R\odot W} \&\& \\
X \& R \& Y \& W \& P \\ X \& R \& Y \& W \& P \\
@@ -851,16 +850,16 @@ As mentioned in the previous section, there is a way to define morphisms in $\sp
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=4-3, to=3-3] \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=4-3, to=3-3]
\arrow["{c_V}"', from=4-3, to=3-4] \arrow["{c_V}"', from=4-3, to=3-4]
\end{tikzcd} \end{tikzcd}
\end{equation*} \end{equation*}
Since we have Since we have
\begin{align*} \begin{align*}
r_1\comp v\comp c_W&\\ r_1\comp v\comp c_W&\\
&=g\comp t_1\comp c_w\\ &=g\comp t_1\comp c_w\\
&=g\comp p_2\comp c_R\\ &=g\comp p_2\comp c_R\\
&=q_2\comp w\comp c_R &=q_2\comp w\comp c_R
\end{align*} \end{align*}
by the universal property of pullbacks, there exists a morphism $u\c R\odot W\to S\odot V$, such that the following diagram commutes: by the universal property of pullbacks, there exists a morphism $u\c R\odot W\to S\odot V$, such that the following diagram commutes:
\begin{equation*} \begin{equation*}
\begin{tikzcd}[ampersand replacement=\&] \begin{tikzcd}[ampersand replacement=\&]
R \& {R\odot W} \& W \\ R \& {R\odot W} \& W \\
S \& {S\odot V} \& V S \& {S\odot V} \& V
@@ -872,92 +871,96 @@ As mentioned in the previous section, there is a way to define morphisms in $\sp
\arrow["{c_S}", from=2-2, to=2-1] \arrow["{c_S}", from=2-2, to=2-1]
\arrow["{c_V}"', from=2-2, to=2-3] \arrow["{c_V}"', from=2-2, to=2-3]
\end{tikzcd} \end{tikzcd}
\end{equation*} \end{equation*}
So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \stackrel{c_W}{\to}W)\to(S \stackrel{c_S}{\leftarrow} S\odot V \stackrel{c_V}{\to}V)$. So, we define $(f,g,w)\odot(g,h,v)=(w,v,u)$. To define the natural isomorphisms is a cumbersome task, but it is known in the literature. So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \stackrel{c_W}{\to}W)\to(S \stackrel{c_S}{\leftarrow} S\odot V \stackrel{c_V}{\to}V)$. So, we define $(f,g,w)\odot(g,h,v)=(w,v,u)$. To define the natural isomorphisms is a cumbersome task, but it is known in the literature. Additionally, showing that $\rel(\BC)\rightrightarrows\BC$ is also a double category is almost the same. The functors are defined the same, except that the functor $\odot$ takes the image of the pullback over its legs, instead of the pullback itself.
% The following diagrams help to see why the defined $\odot$ is a functor. % The following diagrams help to see why the defined $\odot$ is a functor.
% \begin{equation*} % \begin{equation*}
% \begin{tikzcd}[ampersand replacement=\&] % \begin{tikzcd}[ampersand replacement=\&]
% \&\& {R\odot W} \&\& \\ % \&\& {R\odot W} \&\& \\
% X \& R \& Y \& W \& P \\ % X \& R \& Y \& W \& P \\
% Y \& S \& Z \& V \& Q \\ % Y \& S \& Z \& V \& Q \\
% {Y'} \& {S'} \& {Z'} \& {V'} \& {Q'} \\ % {Y'} \& {S'} \& {Z'} \& {V'} \& {Q'} \\
% \&\& {S'\odot V'} % \&\& {S'\odot V'}
% \arrow[from=1-3, to=2-2] % \arrow[from=1-3, to=2-2]
% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-3, to=2-3] % \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-3, to=2-3]
% \arrow[from=1-3, to=2-4] % \arrow[from=1-3, to=2-4]
% \arrow["f"', from=2-1, to=3-1] % \arrow["f"', from=2-1, to=3-1]
% \arrow["{p_1}"', from=2-2, to=2-1] % \arrow["{p_1}"', from=2-2, to=2-1]
% \arrow["{p_2}", from=2-2, to=2-3] % \arrow["{p_2}", from=2-2, to=2-3]
% \arrow["w", from=2-2, to=3-2] % \arrow["w", from=2-2, to=3-2]
% \arrow["g", from=2-3, to=3-3] % \arrow["g", from=2-3, to=3-3]
% \arrow["{t_1}"', from=2-4, to=2-3] % \arrow["{t_1}"', from=2-4, to=2-3]
% \arrow["{t_2}", from=2-4, to=2-5] % \arrow["{t_2}", from=2-4, to=2-5]
% \arrow["v", from=2-4, to=3-4] % \arrow["v", from=2-4, to=3-4]
% \arrow["h", from=2-5, to=3-5] % \arrow["h", from=2-5, to=3-5]
% \arrow["{f'}"', from=3-1, to=4-1] % \arrow["{f'}"', from=3-1, to=4-1]
% \arrow["{q_1}", from=3-2, to=3-1] % \arrow["{q_1}", from=3-2, to=3-1]
% \arrow["{q_2}"', from=3-2, to=3-3] % \arrow["{q_2}"', from=3-2, to=3-3]
% \arrow["{w'}", from=3-2, to=4-2] % \arrow["{w'}", from=3-2, to=4-2]
% \arrow["{g'}", from=3-3, to=4-3] % \arrow["{g'}", from=3-3, to=4-3]
% \arrow["{r_1}", from=3-4, to=3-3] % \arrow["{r_1}", from=3-4, to=3-3]
% \arrow["{r_2}"', from=3-4, to=3-5] % \arrow["{r_2}"', from=3-4, to=3-5]
% \arrow["{v'}", from=3-4, to=4-4] % \arrow["{v'}", from=3-4, to=4-4]
% \arrow["{h'}", from=3-5, to=4-5] % \arrow["{h'}", from=3-5, to=4-5]
% \arrow["{q_1'}", from=4-2, to=4-1] % \arrow["{q_1'}", from=4-2, to=4-1]
% \arrow["{q_2'}"', from=4-2, to=4-3] % \arrow["{q_2'}"', from=4-2, to=4-3]
% \arrow["{r_1'}", from=4-4, to=4-3] % \arrow["{r_1'}", from=4-4, to=4-3]
% \arrow["{r_2'}"', from=4-4, to=4-5] % \arrow["{r_2'}"', from=4-4, to=4-5]
% \arrow[from=5-3, to=4-2] % \arrow[from=5-3, to=4-2]
% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=5-3, to=4-3] % \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=5-3, to=4-3]
% \arrow[from=5-3, to=4-4] % \arrow[from=5-3, to=4-4]
% \end{tikzcd} % \end{tikzcd}
% \end{equation*} % \end{equation*}
% \begin{equation*} % \begin{equation*}
% \begin{tikzcd}[ampersand replacement=\&] % \begin{tikzcd}[ampersand replacement=\&]
% \&\& {R\odot W} \&\&\&\&\& {S\odot V} \&\& \\ % \&\& {R\odot W} \&\&\&\&\& {S\odot V} \&\& \\
% X \& R \& Y \& W \& P \& Y \& S \& Z \& V \& Q \\ % X \& R \& Y \& W \& P \& Y \& S \& Z \& V \& Q \\
% Y \& S \& Z \& V \& Q \& {Y'} \& {S'} \& {Z'} \& {V'} \& {Q'} \\ % Y \& S \& Z \& V \& Q \& {Y'} \& {S'} \& {Z'} \& {V'} \& {Q'} \\
% \&\& {S\odot V} \&\&\&\&\& {S'\odot V'} % \&\& {S\odot V} \&\&\&\&\& {S'\odot V'}
% \arrow["{c_R}"', from=1-3, to=2-2] % \arrow["{c_R}"', from=1-3, to=2-2]
% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-3, to=2-3] % \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-3, to=2-3]
% \arrow["{c_W}", from=1-3, to=2-4] % \arrow["{c_W}", from=1-3, to=2-4]
% \arrow["{c_S}"', from=1-8, to=2-7] % \arrow["{c_S}"', from=1-8, to=2-7]
% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-8, to=2-8] % \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-8, to=2-8]
% \arrow["{c_V}", from=1-8, to=2-9] % \arrow["{c_V}", from=1-8, to=2-9]
% \arrow["f"', from=2-1, to=3-1] % \arrow["f"', from=2-1, to=3-1]
% \arrow["{p_1}"', from=2-2, to=2-1] % \arrow["{p_1}"', from=2-2, to=2-1]
% \arrow["{p_2}", from=2-2, to=2-3] % \arrow["{p_2}", from=2-2, to=2-3]
% \arrow["w", from=2-2, to=3-2] % \arrow["w", from=2-2, to=3-2]
% \arrow["g", from=2-3, to=3-3] % \arrow["g", from=2-3, to=3-3]
% \arrow["{t_1}"', from=2-4, to=2-3] % \arrow["{t_1}"', from=2-4, to=2-3]
% \arrow["{t_2}", from=2-4, to=2-5] % \arrow["{t_2}", from=2-4, to=2-5]
% \arrow["v", from=2-4, to=3-4] % \arrow["v", from=2-4, to=3-4]
% \arrow["h", from=2-5, to=3-5] % \arrow["h", from=2-5, to=3-5]
% \arrow["{f'}"', from=2-6, to=3-6] % \arrow["{f'}"', from=2-6, to=3-6]
% \arrow["{q_1}"', from=2-7, to=2-6] % \arrow["{q_1}"', from=2-7, to=2-6]
% \arrow["{q_2}", from=2-7, to=2-8] % \arrow["{q_2}", from=2-7, to=2-8]
% \arrow["{w'}", from=2-7, to=3-7] % \arrow["{w'}", from=2-7, to=3-7]
% \arrow["{g'}", from=2-8, to=3-8] % \arrow["{g'}", from=2-8, to=3-8]
% \arrow["{r_1}"', from=2-9, to=2-8] % \arrow["{r_1}"', from=2-9, to=2-8]
% \arrow["{r_2}", from=2-9, to=2-10] % \arrow["{r_2}", from=2-9, to=2-10]
% \arrow["{v'}", from=2-9, to=3-9] % \arrow["{v'}", from=2-9, to=3-9]
% \arrow["{h'}", from=2-10, to=3-10] % \arrow["{h'}", from=2-10, to=3-10]
% \arrow["{q_1}", from=3-2, to=3-1] % \arrow["{q_1}", from=3-2, to=3-1]
% \arrow["{q_2}"', from=3-2, to=3-3] % \arrow["{q_2}"', from=3-2, to=3-3]
% \arrow["{r_1}", from=3-4, to=3-3] % \arrow["{r_1}", from=3-4, to=3-3]
% \arrow["{r_2}"', from=3-4, to=3-5] % \arrow["{r_2}"', from=3-4, to=3-5]
% \arrow["{q'_1}", from=3-7, to=3-6] % \arrow["{q'_1}", from=3-7, to=3-6]
% \arrow["{q_2'}"', from=3-7, to=3-8] % \arrow["{q_2'}"', from=3-7, to=3-8]
% \arrow["{r'_1}", from=3-9, to=3-8] % \arrow["{r'_1}", from=3-9, to=3-8]
% \arrow["{r'_2}"', from=3-9, to=3-10] % \arrow["{r'_2}"', from=3-9, to=3-10]
% \arrow["{c_S}", from=4-3, to=3-2] % \arrow["{c_S}", from=4-3, to=3-2]
% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=4-3, to=3-3] % \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=4-3, to=3-3]
% \arrow["{c_V}"', from=4-3, to=3-4] % \arrow["{c_V}"', from=4-3, to=3-4]
% \arrow["{c_{S'}}", from=4-8, to=3-7] % \arrow["{c_{S'}}", from=4-8, to=3-7]
% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=4-8, to=3-8] % \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=4-8, to=3-8]
% \arrow["{c_{V'}}"', from=4-8, to=3-9] % \arrow["{c_{V'}}"', from=4-8, to=3-9]
% \end{tikzcd} % \end{tikzcd}
% \end{equation*} % \end{equation*}
\end{example}
\begin{example}
\todo{Talk about $\spa_a$ and $\rel_a$.}
\end{example}
\section{Coalgebraic Bisimulation}%\label{sec:} \section{Coalgebraic Bisimulation}%\label{sec:}
% %
%\begin{definition}[Relation Lifting] %\begin{definition}[Relation Lifting]