From 73dbac921fa647dfe47c6cd36ba8ebed78de7f75 Mon Sep 17 00:00:00 2001 From: partowp Date: Thu, 6 Aug 2026 17:10:49 +0100 Subject: [PATCH] homework in progress --- draft/draft.tex | 79 +++++++++++++++++++++++++++++++++---------------- 1 file changed, 54 insertions(+), 25 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index a9d7ffd..6b894f5 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -614,8 +614,7 @@ Now, we prove $Sg(\mu') = \nu$. \end{itemize}\qed \end{proof} - -\section{Coalgebraic Bisimulation}%\label{sec:} +\section{Spans and Relations} In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\ such spans $(X \stackrel{p_1}{\leftarrow} R @@ -624,19 +623,19 @@ We denote morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$. A morphism $R\rto S$ ($R\spto S$) in $\rel(\BC)$ ($\spa(\BC)$) is such a triple of morphisms $(f\c R\to S, g_1\c X_1\to Y_1, g_2\c X_2\to Y_2)$ in $\BC$ that the following diagram commutes: - \begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - {X_1} \& R \& {X_2} \\ - {Y_1} \& S \& {Y_2} - \arrow["{g_1}"', 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["f", from=1-2, to=2-2] - \arrow["{g_2}", from=1-3, to=2-3] - \arrow["{q_1}", from=2-2, to=2-1] - \arrow["{q_2}"', from=2-2, to=2-3] - \end{tikzcd} - \end{equation*} +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + {X_1} \& R \& {X_2} \\ + {Y_1} \& S \& {Y_2} + \arrow["{g_1}"', 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["f", from=1-2, to=2-2] + \arrow["{g_2}", from=1-3, to=2-3] + \arrow["{q_1}", from=2-2, to=2-1] + \arrow["{q_2}"', from=2-2, to=2-3] + \end{tikzcd} +\end{equation*} \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$, where the following diagram commutes: @@ -657,21 +656,21 @@ by the image factorization in regular categories. \ppnote{Initially, I wanted to % %\begin{equation*} % \begin{tikzcd}[ampersand replacement=\&] -% R \& {R^\dagger} \&\& {X\times X} -% \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^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4] -% \end{tikzcd} + % R \& {R^\dagger} \&\& {X\times X} + % \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^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4] + % \end{tikzcd} %\end{equation*} We define a functor of type $(-)^\dagger\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^\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^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4] - \end{tikzcd} + 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^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4] + \end{tikzcd} \end{equation*} So, for every functor $F\c\BC\to\BC$ we have $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ that takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation: @@ -692,7 +691,37 @@ For the time being, we limit the discussion to the case $\BC=\Set$. For simplici We can define morphisms in $\rel$ differently by only requesting such functions $g_1$ and $g_2$ that $x\mathrel{R}y$ entails $g_1(x)\mathrel{S}g_2(y)$. Let us call such morphisms \emph{anonymous} (because they omit the witnessing part $f$, which is unique for relations but not for general spans). This however yields an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.} +\begin{prop} + Assuming that $(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 $\spa$, there is an anonymous morphism $(g_1,g_2)\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$ iff there is an onymous $(g_1,g_2,w)$ of the same type, with the witness $w\c R\to S$ in $\spa$. +\end{prop} +\begin{proof} + $(\Rightarrow):$ We define $w$ as $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$. We have: + \begin{align*} + g_1\comp p_1(x_1,x_2)&\\ + =&g_1(x_1)\\ + =&q_1(g(x_1),g(x_2))\\ + =&q_1\comp w(x_1,x_2) + \end{align*} + Similarly, we have $g_2\comp p_2(x_1,x_2)=q_2\comp w(x_1,x_2)$. + + $(\Leftarrow):$ Assuming $x_1\mathrel{R}x_2$, then $w(x_1,x_2)\in S$ as well, and by the definition of onymous morphisms we have $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$, so we have $g_1(x_1)\mathrel{S}g_2(x_2)$. \qed +\end{proof} +\begin{prop} + Assuming that $(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$, there is an anonymous morphism $(g_1,g_2)\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 $\rel$ iff there is an onymous $(g_1,g_2,w)$ of the same type, with the witness $w\c R\to S$ in $\rel$. +\end{prop} +\begin{proof} + \todo{Finish} +\end{proof} + +\begin{prop} + Assuming that $(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$, there is an anonymous morphism $(g_1,g_2)\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)$ iff there is an onymous $(g_1,g_2,w)$ of the same type, with the witness $w\c R\to S$. +\end{prop} +\begin{proof} + \todo{Finish} +\end{proof} + +\section{Coalgebraic Bisimulation}%\label{sec:} By varying from anonymous to non-anonymous morphisms and from $\rel$ to $\spa$ we can obtain for flavors of bisimulation (\autoref{eq:acz-mend-diag}--\autoref{def:vanila}) -- \autoref{fig:anonymous_onymous} contains a comprehensible summary.