delta

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}