From d5a0824d1342bfeb005a37f59d0e4495186f2122 Mon Sep 17 00:00:00 2001 From: partowp Date: Mon, 14 Sep 2026 14:39:03 +0100 Subject: [PATCH] relation lifting and abstract relational bisimulation ommited --- draft/draft.tex | 126 ++++++++++++++++++++++++++++++++---------------- 1 file changed, 84 insertions(+), 42 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 4a726ba..2c3043f 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -687,9 +687,17 @@ Now, we prove $Sg(\mu') = \nu$. \end{tikzcd} \end{equation*} \end{definition} - +% +\begin{definition}[Jointly Monic] + A pair of morphisms $p_1\c R\to X$ and $p_2\c R\to Y$ is jointly monic iff for every pair of morphisms $f,g\c A \to R$ assuming that $p_1\comp f=p_1\comp g$ and $p_2\comp f=p_2\comp g$ then $f=g$. +\end{definition} +% +\begin{prop} + In a category $\BC$ with products, two morphisms $p_1\c R\to X$ and $p_2\c R \to Y$ are jointly monic iff $\brks{p_1,p_2}\c R\to X\times Y$ is monic.\qed +\end{prop} +% \begin{definition}[Category of Relations] -For an arbitrary category $\BC$\sgnote{In this definition $\BC$ is not arbitrary -- it must have products. But this can be fixed by reformulating in terms of joint monics.}, the category of relations, denoted by $\rel(\BC)$ has as objects such spans $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ that $\brks{p_1,p_2}$ is a monomorphism. A morphism $(g_1,g_2,w)\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(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(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(\BC)$ as well, and $(g_1,g_2,w)$ is a morphism in $\spa(\BC)$. +For an arbitrary category $\BC$\sgnote{In this definition $\BC$ is not arbitrary -- it must have products. But this can be fixed by reformulating in terms of joint monics.}, the category of relations, denoted by $\rel(\BC)$ has as objects such spans $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ that $\brks{p_1,p_2}$ is a monomorphism. A morphism $(g_1,g_2,w)\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(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(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(\BC)$ as well, and $g_1$ and $g_2$ are jointly monic. \end{definition} % %\begin{prop} @@ -1194,25 +1202,25 @@ So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \sta In an arbitrary category $\BC$, a span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{Aczel-Mendler bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\spa(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$. \end{definition} % -\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$, whenever the following diagram commutes: - \begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - \rel(\BC) \&\& \rel(\BC) \\ - {\BC\times\BC} \&\& {\BC\times\BC} - \arrow["{\rel(F)}", from=1-1, to=1-3] - \arrow["{U}"',from=1-1, to=2-1] - \arrow["{U}",from=1-3, to=2-3] - \arrow["{F\times F}"', from=2-1, to=2-3] - \end{tikzcd} - \end{equation*} -\end{definition} -\begin{definition}[Abstract Relational Bisimulation]\label{def:abs-rel-bis} - In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{abstract relational bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{\rel(F)p_1}{\leftarrow} \rel(F)R \stackrel{\rel(F)p_2}{\to}FY)$. -\end{definition} -The given definition is highly abstract. There is a relation lifting that abstracts Barr-relators that are known to be well-behaved relators, and it also gives an interesting notion of bisimulation, called \emph{Hermida-Jacobs bisimulation}. +%\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$, whenever the following diagram commutes: +% \begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% \rel(\BC) \&\& \rel(\BC) \\ +% {\BC\times\BC} \&\& {\BC\times\BC} +% \arrow["{\rel(F)}", from=1-1, to=1-3] +% \arrow["{U}"',from=1-1, to=2-1] +% \arrow["{U}",from=1-3, to=2-3] +% \arrow["{F\times F}"', from=2-1, to=2-3] +% \end{tikzcd} +% \end{equation*} +%\end{definition} +%\begin{definition}[Abstract Relational Bisimulation]\label{def:abs-rel-bis} +% In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{abstract relational bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{\rel(F)p_1}{\leftarrow} \rel(F)R \stackrel{\rel(F)p_2}{\to}FY)$. +%\end{definition} +%The given definition is highly abstract. There is a relation lifting that abstracts Barr-relators that are known to be well-behaved relators, and it also gives an interesting notion of bisimulation, called \emph{Hermida-Jacobs bisimulation}. % - The lifting is using the image factorization in regular categories. %\ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.} +% The lifting is using the image factorization in regular categories. %\ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.} % %\begin{equation*} % \begin{tikzcd}[ampersand replacement=\&] @@ -1222,28 +1230,62 @@ The given definition is highly abstract. There is a relation lifting that abstra % \arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4] % \end{tikzcd} %\end{equation*} - For a regular category $\BC$, we define a functor of type $(-)^\clubsuit\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^\clubsuit} \&\& {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^\clubsuit_1,p^\clubsuit_2}}"', tail, from=1-2, to=1-4] - \end{tikzcd} - \end{equation*} - Also, for every functor $F\c\BC\to\BC$ we have a trivial lifting to $\spa(\BC)$ that takes every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$, and every morphism $(f,g,w)$ to $(Ff,Fg,Fw)$, and we denote it with $\spa(F)$. Since $\rel(\BC)$ is a subcategory of $\spa(\BC)$, we have an inclusion functor $I\c\rel(\BC)\to\spa(\BC)$ as well. - So, given a functor $F\c\BC\to\BC$ we define its lifting $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ as $(F-)^\dagger=(\spa(F)I-)^\clubsuit$. The functor $(F-)^\dagger$ takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation: - \begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - \& {(FR)^\dagger} \& \\ - FX \&\& FY \\ - \& {FX\times FY} - \arrow["{{{(Fp_1)^\dagger}}}"', from=1-2, to=2-1] - \arrow["{{{(Fp_2)^\dagger}}}", from=1-2, to=2-3] - \arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2] - \end{tikzcd} - \end{equation*} + By applying the functor $F$ on all of the components of $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ that is an object of $\spa(\BC)$ we get another object of $\spa(\BC)$, but it is not the case for $\rel(\BC)$. As an example, if we set $F$ to be the powerset functor $\powf$, then $(\powf X \stackrel{\powf p_1}{\leftarrow} \powf R \stackrel{\powf p_2}{\to}\powf Y)$ is not necessarily a relation anymore because if we take $R=\{(1,0),(0,1),(0,0),(1,1)\}$, and define functions $f\c R\to \powf R$ and $g\c R\to \powf R$ as + \begin{gather*} + f(w)= + \begin{cases} + \{(1,0),(0,1),(0,0),(1,1)\} & w=(0,0) \\ + R & otherwise + \end{cases}\\ + g(w)= + \begin{cases} + \{(1,0),(0,1),(0,0)\} & w=(0,0) \\ + R & otherwise + \end{cases} + \end{gather*} + then $\powf p_1\comp f=\powf p_1\comp g$ and $\powf p_2\comp f=\powf p_2\comp g$ hold, but $f\neq g$. So, $\powf p_1$ and $\powf p_2$ are not jointly monic. +% For a regular category $\BC$, we define a functor of type $(-)^\clubsuit\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^\clubsuit} \&\& {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^\clubsuit_1,p^\clubsuit_2}}"', tail, from=1-2, to=1-4] +% \end{tikzcd} +% \end{equation*} +% Also, for every functor $F\c\BC\to\BC$ we have a trivial lifting to $\spa(\BC)$ that takes every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$, and every morphism $(f,g,w)$ to $(Ff,Fg,Fw)$, and we denote it with $\spa(F)$. Since $\rel(\BC)$ is a subcategory of $\spa(\BC)$, we have an inclusion functor $I\c\rel(\BC)\to\spa(\BC)$ as well. +% So, given a functor $F\c\BC\to\BC$ we define its lifting $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ as $(F-)^\dagger=(\spa(F)I-)^\clubsuit$. The functor $(F-)^\dagger$ takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation: +% \begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% \& {(FR)^\dagger} \& \\ +% FX \&\& FY \\ +% \& {FX\times FY} +% \arrow["{{{(Fp_1)^\dagger}}}"', from=1-2, to=2-1] +% \arrow["{{{(Fp_2)^\dagger}}}", from=1-2, to=2-3] +% \arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2] +% \end{tikzcd} +% \end{equation*} +To cope with this, we assume $\BC$ to be a regular category, so we have the following epi-mono decomposition for every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\spa(\BC)$: +\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} +\end{equation*} +We can define $(-)^\dagger$ as a functor from $\spa(\BC)\to\rel(\BC)$ that takes $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(X \stackrel{p^\dagger_1}{\leftarrow} R^\dagger \stackrel{p^\dagger_2}{\to}Y)$, then we define $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ to take $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ to the following relation: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + \& {(FR)^\dagger} \& \\ + FX \&\& FY \\ + \& {FX\times FY} + \arrow["{{{(Fp_1)^\dagger}}}"', from=1-2, to=2-1] + \arrow["{{{(Fp_2)^\dagger}}}", from=1-2, to=2-3] + \arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2] + \end{tikzcd} +\end{equation*} % \begin{definition}[Hermida-Jacobs Bisimulation] In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a \emph{Hermida-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$.