From 4dedba1ee580c1f94583bbcc8655b3c2c61721bb Mon Sep 17 00:00:00 2001 From: partowp Date: Wed, 2 Sep 2026 21:24:30 +0100 Subject: [PATCH] rel --- draft/draft.tex | 283 ++++++++++++++++++++++++------------------------ 1 file changed, 143 insertions(+), 140 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 3d96d96..1635e48 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -815,149 +815,152 @@ As mentioned in the previous section, there is a way to define morphisms in $\sp \arrow["{p_2}"', from=2-1, to=2-2] \end{tikzcd} \end{gather*} -\end{example} - For morphisms - \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) - \end{gather*} - and - \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) - \end{gather*} - we have the following commutative diagram: - \begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - \&\& {R\odot W} \&\& \\ - X \& R \& Y \& W \& P \\ - Y \& S \& Z \& V \& Q \\ - \&\& {S\odot V} - \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["{c_W}", from=1-3, to=2-4] - \arrow["f"', from=2-1, to=3-1] - \arrow["{p_1}"', from=2-2, to=2-1] - \arrow["{p_2}", from=2-2, to=2-3] - \arrow["w", from=2-2, to=3-2] - \arrow["g", from=2-3, to=3-3] - \arrow["{t_1}"', from=2-4, to=2-3] - \arrow["{t_2}", from=2-4, to=2-5] - \arrow["v", from=2-4, to=3-4] - \arrow["h", from=2-5, to=3-5] - \arrow["{q_1}", from=3-2, to=3-1] - \arrow["{q_2}"', from=3-2, to=3-3] - \arrow["{r_1}", from=3-4, to=3-3] - \arrow["{r_2}"', from=3-4, to=3-5] - \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["{c_V}"', from=4-3, to=3-4] - \end{tikzcd} - \end{equation*} - Since we have - \begin{align*} - r_1\comp v\comp c_W&\\ - &=g\comp t_1\comp c_w\\ - &=g\comp p_2\comp c_R\\ - &=q_2\comp w\comp c_R - \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: - \begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - R \& {R\odot W} \& W \\ - S \& {S\odot V} \& V - \arrow["w", from=1-1, to=2-1] - \arrow["{c_R}"', from=1-2, to=1-1] - \arrow["{c_W}", from=1-2, to=1-3] - \arrow["u"', dashed, from=1-2, to=2-2] - \arrow["v", from=1-3, to=2-3] - \arrow["{c_S}", from=2-2, to=2-1] - \arrow["{c_V}"', from=2-2, to=2-3] - \end{tikzcd} - \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. +For morphisms +\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) +\end{gather*} +and +\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) +\end{gather*} +we have the following commutative diagram: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + \&\& {R\odot W} \&\& \\ + X \& R \& Y \& W \& P \\ + Y \& S \& Z \& V \& Q \\ + \&\& {S\odot V} + \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["{c_W}", from=1-3, to=2-4] + \arrow["f"', from=2-1, to=3-1] + \arrow["{p_1}"', from=2-2, to=2-1] + \arrow["{p_2}", from=2-2, to=2-3] + \arrow["w", from=2-2, to=3-2] + \arrow["g", from=2-3, to=3-3] + \arrow["{t_1}"', from=2-4, to=2-3] + \arrow["{t_2}", from=2-4, to=2-5] + \arrow["v", from=2-4, to=3-4] + \arrow["h", from=2-5, to=3-5] + \arrow["{q_1}", from=3-2, to=3-1] + \arrow["{q_2}"', from=3-2, to=3-3] + \arrow["{r_1}", from=3-4, to=3-3] + \arrow["{r_2}"', from=3-4, to=3-5] + \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["{c_V}"', from=4-3, to=3-4] + \end{tikzcd} +\end{equation*} +Since we have +\begin{align*} + r_1\comp v\comp c_W&\\ + &=g\comp t_1\comp c_w\\ + &=g\comp p_2\comp c_R\\ + &=q_2\comp w\comp c_R +\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: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + R \& {R\odot W} \& W \\ + S \& {S\odot V} \& V + \arrow["w", from=1-1, to=2-1] + \arrow["{c_R}"', from=1-2, to=1-1] + \arrow["{c_W}", from=1-2, to=1-3] + \arrow["u"', dashed, from=1-2, to=2-2] + \arrow["v", from=1-3, to=2-3] + \arrow["{c_S}", from=2-2, to=2-1] + \arrow["{c_V}"', from=2-2, to=2-3] + \end{tikzcd} +\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. 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. % \begin{equation*} -% \begin{tikzcd}[ampersand replacement=\&] -% \&\& {R\odot W} \&\& \\ -% X \& R \& Y \& W \& P \\ -% Y \& S \& Z \& V \& Q \\ -% {Y'} \& {S'} \& {Z'} \& {V'} \& {Q'} \\ -% \&\& {S'\odot V'} -% \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[from=1-3, to=2-4] -% \arrow["f"', from=2-1, to=3-1] -% \arrow["{p_1}"', from=2-2, to=2-1] -% \arrow["{p_2}", from=2-2, to=2-3] -% \arrow["w", from=2-2, to=3-2] -% \arrow["g", from=2-3, to=3-3] -% \arrow["{t_1}"', from=2-4, to=2-3] -% \arrow["{t_2}", from=2-4, to=2-5] -% \arrow["v", from=2-4, to=3-4] -% \arrow["h", from=2-5, to=3-5] -% \arrow["{f'}"', from=3-1, to=4-1] -% \arrow["{q_1}", from=3-2, to=3-1] -% \arrow["{q_2}"', from=3-2, to=3-3] -% \arrow["{w'}", from=3-2, to=4-2] -% \arrow["{g'}", from=3-3, to=4-3] -% \arrow["{r_1}", from=3-4, to=3-3] -% \arrow["{r_2}"', from=3-4, to=3-5] -% \arrow["{v'}", from=3-4, to=4-4] -% \arrow["{h'}", from=3-5, to=4-5] -% \arrow["{q_1'}", from=4-2, to=4-1] -% \arrow["{q_2'}"', from=4-2, to=4-3] -% \arrow["{r_1'}", from=4-4, to=4-3] -% \arrow["{r_2'}"', from=4-4, to=4-5] -% \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[from=5-3, to=4-4] -% \end{tikzcd} -% \end{equation*} + % \begin{tikzcd}[ampersand replacement=\&] + % \&\& {R\odot W} \&\& \\ + % X \& R \& Y \& W \& P \\ + % Y \& S \& Z \& V \& Q \\ + % {Y'} \& {S'} \& {Z'} \& {V'} \& {Q'} \\ + % \&\& {S'\odot V'} + % \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[from=1-3, to=2-4] + % \arrow["f"', from=2-1, to=3-1] + % \arrow["{p_1}"', from=2-2, to=2-1] + % \arrow["{p_2}", from=2-2, to=2-3] + % \arrow["w", from=2-2, to=3-2] + % \arrow["g", from=2-3, to=3-3] + % \arrow["{t_1}"', from=2-4, to=2-3] + % \arrow["{t_2}", from=2-4, to=2-5] + % \arrow["v", from=2-4, to=3-4] + % \arrow["h", from=2-5, to=3-5] + % \arrow["{f'}"', from=3-1, to=4-1] + % \arrow["{q_1}", from=3-2, to=3-1] + % \arrow["{q_2}"', from=3-2, to=3-3] + % \arrow["{w'}", from=3-2, to=4-2] + % \arrow["{g'}", from=3-3, to=4-3] + % \arrow["{r_1}", from=3-4, to=3-3] + % \arrow["{r_2}"', from=3-4, to=3-5] + % \arrow["{v'}", from=3-4, to=4-4] + % \arrow["{h'}", from=3-5, to=4-5] + % \arrow["{q_1'}", from=4-2, to=4-1] + % \arrow["{q_2'}"', from=4-2, to=4-3] + % \arrow["{r_1'}", from=4-4, to=4-3] + % \arrow["{r_2'}"', from=4-4, to=4-5] + % \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[from=5-3, to=4-4] + % \end{tikzcd} + % \end{equation*} % \begin{equation*} -% \begin{tikzcd}[ampersand replacement=\&] -% \&\& {R\odot W} \&\&\&\&\& {S\odot V} \&\& \\ -% X \& R \& Y \& W \& P \& Y \& S \& Z \& V \& Q \\ -% Y \& S \& Z \& V \& Q \& {Y'} \& {S'} \& {Z'} \& {V'} \& {Q'} \\ -% \&\& {S\odot V} \&\&\&\&\& {S'\odot V'} -% \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["{c_W}", from=1-3, to=2-4] -% \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["{c_V}", from=1-8, to=2-9] -% \arrow["f"', from=2-1, to=3-1] -% \arrow["{p_1}"', from=2-2, to=2-1] -% \arrow["{p_2}", from=2-2, to=2-3] -% \arrow["w", from=2-2, to=3-2] -% \arrow["g", from=2-3, to=3-3] -% \arrow["{t_1}"', from=2-4, to=2-3] -% \arrow["{t_2}", from=2-4, to=2-5] -% \arrow["v", from=2-4, to=3-4] -% \arrow["h", from=2-5, to=3-5] -% \arrow["{f'}"', from=2-6, to=3-6] -% \arrow["{q_1}"', from=2-7, to=2-6] -% \arrow["{q_2}", from=2-7, to=2-8] -% \arrow["{w'}", from=2-7, to=3-7] -% \arrow["{g'}", from=2-8, to=3-8] -% \arrow["{r_1}"', from=2-9, to=2-8] -% \arrow["{r_2}", from=2-9, to=2-10] -% \arrow["{v'}", from=2-9, to=3-9] -% \arrow["{h'}", from=2-10, to=3-10] -% \arrow["{q_1}", from=3-2, to=3-1] -% \arrow["{q_2}"', from=3-2, to=3-3] -% \arrow["{r_1}", from=3-4, to=3-3] -% \arrow["{r_2}"', from=3-4, to=3-5] -% \arrow["{q'_1}", from=3-7, to=3-6] -% \arrow["{q_2'}"', from=3-7, to=3-8] -% \arrow["{r'_1}", from=3-9, to=3-8] -% \arrow["{r'_2}"', from=3-9, to=3-10] -% \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["{c_V}"', from=4-3, to=3-4] -% \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["{c_{V'}}"', from=4-8, to=3-9] -% \end{tikzcd} -% \end{equation*} + % \begin{tikzcd}[ampersand replacement=\&] + % \&\& {R\odot W} \&\&\&\&\& {S\odot V} \&\& \\ + % X \& R \& Y \& W \& P \& Y \& S \& Z \& V \& Q \\ + % Y \& S \& Z \& V \& Q \& {Y'} \& {S'} \& {Z'} \& {V'} \& {Q'} \\ + % \&\& {S\odot V} \&\&\&\&\& {S'\odot V'} + % \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["{c_W}", from=1-3, to=2-4] + % \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["{c_V}", from=1-8, to=2-9] + % \arrow["f"', from=2-1, to=3-1] + % \arrow["{p_1}"', from=2-2, to=2-1] + % \arrow["{p_2}", from=2-2, to=2-3] + % \arrow["w", from=2-2, to=3-2] + % \arrow["g", from=2-3, to=3-3] + % \arrow["{t_1}"', from=2-4, to=2-3] + % \arrow["{t_2}", from=2-4, to=2-5] + % \arrow["v", from=2-4, to=3-4] + % \arrow["h", from=2-5, to=3-5] + % \arrow["{f'}"', from=2-6, to=3-6] + % \arrow["{q_1}"', from=2-7, to=2-6] + % \arrow["{q_2}", from=2-7, to=2-8] + % \arrow["{w'}", from=2-7, to=3-7] + % \arrow["{g'}", from=2-8, to=3-8] + % \arrow["{r_1}"', from=2-9, to=2-8] + % \arrow["{r_2}", from=2-9, to=2-10] + % \arrow["{v'}", from=2-9, to=3-9] + % \arrow["{h'}", from=2-10, to=3-10] + % \arrow["{q_1}", from=3-2, to=3-1] + % \arrow["{q_2}"', from=3-2, to=3-3] + % \arrow["{r_1}", from=3-4, to=3-3] + % \arrow["{r_2}"', from=3-4, to=3-5] + % \arrow["{q'_1}", from=3-7, to=3-6] + % \arrow["{q_2'}"', from=3-7, to=3-8] + % \arrow["{r'_1}", from=3-9, to=3-8] + % \arrow["{r'_2}"', from=3-9, to=3-10] + % \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["{c_V}"', from=4-3, to=3-4] + % \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["{c_{V'}}"', from=4-8, to=3-9] + % \end{tikzcd} + % \end{equation*} +\end{example} +\begin{example} + \todo{Talk about $\spa_a$ and $\rel_a$.} +\end{example} \section{Coalgebraic Bisimulation}%\label{sec:} % %\begin{definition}[Relation Lifting]