diff --git a/draft/draft.tex b/draft/draft.tex index c35338e..82c605d 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1745,6 +1745,65 @@ We can also define $\join$ and $\meet$ on morphisms as follows: \end{gather*} By~\autoref{lem:alph-prod} there exists a simulation $\delta\in S$ for which we have $(\mathcal{P}p_1)^\dagger\comp\delta(x_1,x_2)=\alpha(x_1)$. So, $(\mathcal{P}p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2)=\alpha(x_1)$. Then by the equations in~\eqref{eq:diag-sym-rel} we also get $(\mathcal{P}p_2)^\dagger\comp((\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=\alpha(x_2)$.\qed \end{proof} +\section{Relators} +We start the discussion with answering the question that why there can be multiple simulation structures based on~\autoref{def:sim}. +At the moment we have limited the discussion to the category of sets and we are talking about the powerset functor. We know that $\sigma$ is unique in the following diagram: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \\ + {\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}X} + \arrow["\alpha"', from=1-1, to=2-1] + \arrow["{p_1}"', from=1-2, to=1-1] + \arrow["{p_2}", from=1-2, to=1-3] + \arrow["\sigma", dashed, from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["{{\mathcal{P}p_1^\dagger}_\subseteq}", from=2-2, to=2-1] + \arrow["{{\mathcal{P}p_2^\dagger}_\subseteq}"', from=2-2, to=2-3] + \end{tikzcd} +\end{equation*} +It is defined as $\sigma(x_1,x_2)=(\alpha(x_1),\alpha(x_2))$. +But $\sigma'$ in the following diagram is not unique: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \\ + {\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}X} + \arrow["\alpha"', from=1-1, to=2-1] + \arrow["\subseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2] + \arrow["{p_1}"', from=1-2, to=1-1] + \arrow["{p_2}", from=1-2, to=1-3] + \arrow["{\sigma'}", from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["\subseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3] + \arrow["{{\mathcal{P}p_1^\dagger}}", from=2-2, to=2-1] + \arrow["{{\mathcal{P}p_2^\dagger}}"', from=2-2, to=2-3] + \end{tikzcd} +\end{equation*} +Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\delta\c(\mathcal{P}R)^\dagger\to\subseteq;(\mathcal{P}R)^\dagger;\subseteq$ that $\sigma=\delta\comp\sigma'$, i.e., the following diagram commutes: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \\ + {\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}X} \\ + {\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}X} + \arrow["\alpha"', from=1-1, to=2-1] + \arrow["{p_1}"', from=1-2, to=1-1] + \arrow["{p_2}", from=1-2, to=1-3] + \arrow["{\sigma'}", from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["id"', from=2-1, to=3-1] + \arrow["\delta", from=2-2, to=3-2] + \arrow["id"', from=2-3, to=3-3] + \arrow["{{\mathcal{P}p_1^\dagger}_\subseteq}", from=3-2, to=3-1] + \arrow["{{\mathcal{P}p_2^\dagger}_\subseteq}"', from=3-2, to=3-3] + \end{tikzcd} +\end{equation*} +$\delta$ is defined as the following: +\begin{gather*} + \delta(w)= + \begin{cases} + (\alpha(x_1),\alpha(x_2)) & \exists x_1,x_2, \sigma'(x_1,x_2)=w \\ + w & \mathsf{o.w} + \end{cases} +\end{gather*} \end{document}