pouya/coalgebraic-simulation
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

more

Browse Source
This commit is contained in:
partowp
2026-09-08 20:47:35 +01:00
parent 01cd129e96
commit 7d013ddf97
1 changed files with 78 additions and 21 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+78 -21
View File
@@ -789,13 +789,18 @@ As mentioned in the previous section, there is a way to define morphisms in $\sp
T(\mathcal{R}\odot \mathcal{S})=T\mathcal{S}
\end{gather*}
\end{definition}
%
\begin{definition}
In a double category $\BC_1\rightrightarrows\BC_0$ for promorphisms $\mathcal{R}$ and $\mathcal{S}$ that $S\mathcal{R}=S\mathcal{S}$ and $T\mathcal{R}=T\mathcal{S}$, an \emph{inclusion cell} is a cell $\alpha\c\mathcal{R}\Rightarrow\mathcal{S}$ such that $S\alpha=\id_{S\mathcal{R}}$ and $T\alpha=\id_{T\mathcal{R}}$.
\end{definition}
%
\begin{example}\label{ex:spa-double-cat}
We show that assuming the category $\BC$ has pullbacks, $\spa(\BC)\rightrightarrows\BC$ is a double category. We define $S$ and $T$ as follows:
\begin{gather*}
S(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)=X_1\\
S(g_1,g_2,w)=g_1\\\\
S(g_1,g_2,w)=g_1\\
T(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)=X_2\\
T(g_1,g_2,w)=g_2\\
T(g_1,g_2,w)=g_2
\end{gather*}
Furthermore, for every object $X$ in $\BC$ we show the kernel pair of $\id_X$ with $\Delta_X$, and we define $UX=\Delta_X$ and for a morphism $f\c X\to Y$ in $\BC$, $Uf$ is the unique morphism $\Delta_f$ in the diagram below that is obtained by the universal property of pullbacks:
\begin{equation*}
@@ -989,7 +994,8 @@ So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \sta
\begin{gather*}
(g,h)\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*}
by the axiom of choice and~\autoref{prop:spa-spaa} there exist $c_1\c R\to S$ and $c_2\c W\to V$ such that $(f,g,c_1)$ and $(g,h,c_2)$ are morphisms of the same type in $\spa$. So, as we did show in~\autoref{ex:spa-double-cat} there exists $u\c R\odot W\to S\odot V$ such that $(c_1,c_2,u)\c (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)$ is a morphism in $\spa$ and it is equal with $(f,g,c_1)\odot(g,h,c_2)$, so here we define $(f,g)\odot(g,h)=(c_1,c_2)$. Using $u$ it is obvious that $(c_1,c_2)$ is a morphism in $\spa_a$. Defining the natural isomorphisms are the same for~\autoref{ex:spa-double-cat}. Again, for $\rel_a$ the definitions are similar, except that to define $\odot$ we need to take the image of the pullback over its legs, similar to the case for $\rel(\BC)$.\todo{It is better to double check your last claims.}
by the axiom of choice and~\autoref{prop:spa-spaa} there exist $c_1\c R\to S$ and $c_2\c W\to V$ such that $(f,g,c_1)$ and $(g,h,c_2)$ are morphisms of the same type in $\spa$. So, as we did show in~\autoref{ex:spa-double-cat} there exists $u\c R\odot W\to S\odot V$ such that $(c_1,c_2,u)\c (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)$ is a morphism in $\spa$ and it is equal with $(f,g,c_1)\odot(g,h,c_2)$, so here we define $(f,g)\odot(g,h)=(c_1,c_2)$. Using $u$ it is obvious that $(c_1,c_2)$ is a morphism in $\spa_a$. Defining the natural isomorphisms are the same for~\autoref{ex:spa-double-cat}. Again, for $\rel_a$ the definitions are similar, except that to define $\odot$ we need to take the image of the pullback over its legs, similar to the case for $\rel(\BC)$.\todo{It is better to double check your last claims.}\\
Inclusion cells in these categories imply set inclusion.
\end{example}
%
\section{Coalgebraic Bisimulation}%\label{sec:}
@@ -1439,10 +1445,6 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
A relator $\relar$ is symmetric if and only if for every relation $R$ we have $\relar(R^\op)=(\relar R)^\op$.
\end{definition}
%
\begin{definition}[Natural Relator]
An $F$-relator $\relar$ is called \emph{natural}, whenever for every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$, and arbitrary functions $f\c A\to X$, and $g\c B\to Y$, we have $\relar (g^\op\comp R\comp f)=(Fg)^\op\comp\relar R\comp Ff$.
\end{definition}
%
\begin{definition}[Relator-based Bisimulation]
Given a relator $\relar$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an $\relar$-bisimulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ whenever $R$ is an $\relar$-simulation, and $\relar$ is a symmetric relator.
\end{definition}
@@ -1965,28 +1967,46 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
%
%
\begin{definition}[Double Relator]\label{def:doub-rela}
Given a double category $\BC_1\rightrightarrows\BC_0$, for an endofunctor $F$, an $F$-double relator $\relar$ is an endomap on objects and morphisms of category $\BC_1$, for which the following equations hold:
Given a double category $\BC_1\rightrightarrows\BC_0$, for an endofunctor $F$, an $F$-double relator $\relar$ is an endomap on objects of category $\BC_1$, for which the following equations hold:
\begin{enumerate}
\item $S\comp\relar=F\comp S$
\item $T\comp\relar=F\comp T$
\end{enumerate}
Additionally, it takes every cell of type $\mathcal{R}\Rightarrow\mathcal{S}$ to a cell of type $\relar\mathcal{R}\Rightarrow\relar\mathcal{S}$.
Additionally, it has the following condition called monotonicity: If there is an inclusion cell from a promorphisms $\mathcal{R}$ to $\mathcal{S}$ then there must be an inclusion promorphism from $\relar\mathcal{R}$ to $\relar\mathcal{S}$ as well.
\end{definition}
\begin{remark}
In the above definition we are describing an endomap on objects and morphisms of a category, and we form equations with compositions of this map. The composition that we mean, is the one over functions and not the functors. Indeed, it does not make a functor, but it makes another function. Additionally, the endomap that we define is actually two endomaps on objects and morphisms, respectively, but we use the tradition in denoting functors for it that is to use one letter to refer to both maps. Basically, one can think of a relator $\relar$ as a functor that does not necessarily preserve identities and compositions.
In the above definition we are describing an endomap on objects of a category, and we form equations with compositions of this map. The composition that we mean, is the one over functions and not the functors. Indeed, it does not make a functor, but it makes another function. Additionally, we will the endomap in the future with another endomap on morphisms as well, but we use the tradition in denoting functors for it that is to use one letter to refer to both maps. %Basically, one can think of a relator $\relar$ as a functor that does not necessarily preserve identities and compositions.
\end{remark}
%
\begin{definition}[Normal Double Relator]
A $F$-double relator $\relar$ is normal, whenever the following equation holds:
\begin{gather*}
\relar\comp U=U\comp F
\end{gather*}
\end{definition}
\begin{definition}[Double Coalgebra]
Given a double category $\BC_1\rightrightarrows\BC_0$, and a $F$-double relator $\relar$, a pair $(\mathcal{R},\delta)$ that $\delta\c\mathcal{R}\Rightarrow\relar\mathcal{R}$ is an $\relar$-double coalgebra on $\BC_1\rightrightarrows\BC_0$.
\end{definition}
%
Given an $F$-relator $\relar$ defined in~\autoref{def:relator} we have a canonical way to extend its definition over morphisms of $\rel_a$ as well:
\begin{example}
For every relator $\relar$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an $\relar$-simulation from a coalgebra $(X,f)$ to $(Y,g)$ if and only if $((X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y),(f,g))$ is an $\relar$-double coalgebra in $\rel_a\rightrightarrows\Set$.
\end{example}
%
%\subsection{Properties of Double Relators}
\begin{definition}[Normal Double Relator]
An $F$-double relator $\relar$ is normal, whenever the following equation holds:
\begin{gather*}
\relar\comp U=U\comp F
\end{gather*}
\end{definition}
\begin{definition}
An $F$-relator $\relar$ is normal, whenever for every set $X$, we have $\relar\id_X=\id_{FX}$.
\end{definition}
%
It is obvious to see that normal relators and double relators in $\rel_a\rightrightarrows\Set$ coincide.\\
%
\begin{definition}[Natural Double Relator]
An $F$-double relator $\relar$ is natural, whenever it takes every cell of type $\mathcal{R}\Rightarrow\mathcal{S}$ to a cell of type $\relar\mathcal{R}\Rightarrow\relar\mathcal{S}$.
\end{definition}
Given an $F$-relator $\relar$ defined in~\autoref{def:relator} we have a canonical way to extend its definition over morphisms of $\rel_a$ as well:
\begin{definition}[Natural Relator]
An $F$-relator $\relar$ is called \emph{natural}, whenever for every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$, and arbitrary functions $f\c A\to X$, and $g\c B\to Y$, we have $\relar (g^\op\comp R\comp f)=(Fg)^\op\comp\relar R\comp Ff$.
\end{definition}
%
\begin{definition}[Extendable Relator]
Assuming $\relar$ is an $F$-relator, it is an \emph{extendable} relator whenever for every morphims $(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_a$ there exists the morphism $(Fg_1,Fg_2)\c(FX_1 \stackrel{Fp_1}{\leftarrow} \relar R \stackrel{Fp_2}{\to}FX_2)\to(FY_1 \stackrel{Fq_1}{\leftarrow} \relar S \stackrel{Fq_2}{\to}FY_2)$ in $\rel_a$.
\end{definition}
@@ -2000,11 +2020,48 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
Assuming that there exists $(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_a$ we need to show that exists the morphism $(Fg_1,Fg_2)\c(FX_1 \stackrel{Fp_1}{\leftarrow} \relar R \stackrel{Fp_2}{\to}FX_2)\to(FY_1 \stackrel{Fq_1}{\leftarrow} \relar S \stackrel{Fq_2}{\to}FY_2)$ in $\rel_a$. It is equivalent with showing that $\relar R\subseteq (Fg_2)^\op\comp\relar S\comp Fg_1$. Since $\relar$ is natural we have $(Fg_2)^\op\comp\relar S\comp Fg_1=\relar(g_2^\op\comp S\comp g_1)$. Existence of $(g_1,g_2)$ is equivalent with $R\subseteq g_2^\op\comp S\comp g_1$, so by the monotonicity of $\relar$ as a relator we have $\relar R\subseteq \relar(g_2^\op\comp S\comp g_1)$. So, we have $\relar R\subseteq Fg_2^\op\comp \relar S\comp Fg_1$.\qed
\end{proof}
\begin{cor}
Every natural relator is a double relator in $\rel_a\rightrightarrows\Set$.
Every natural relator is a natural double relator in $\rel_a\rightrightarrows\Set$.
\end{cor}
So, now we see that for every natural relator $\relar$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an $\relar$-simulation from a coalgebra $(X,f)$ to $(Y,g)$ if and only if $((X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y),(f,g))$ is an $\relar$-double coalgebra in $\rel_a\rightrightarrows\Set$.
\todo{First, finish the subsection in section 2, then come back here and continue this by saying that every relator is a double relator in $\Set$, and then define symmetric double relators, and then instantiate every notion that you have introduced in previous sections.}
\todo{Perhaps in the future you can also introduce properties of relators for double relatros.}
%
\begin{definition}[Two-sided Double Category]
Assuming that in the double category $\BC_1\rightrightarrows\BC_0$ for every promorphism $\mathcal{R}$ there exists an up to isomorphism unique promorphism $\mathcal{R}^\op$ such that $S\mathcal{R}=T\mathcal{R}^\op$, $T\mathcal{R}=S\mathcal{R}^\op$, and there is an inclusion cell between the two promorphisms that is an isomorphism in $\BC_1$, then $\BC_1\rightrightarrows\BC_0$ is a \emph{two-sided} double category.
\end{definition}
\begin{example}
For an arbitrary category $\BC$ all the categories $\spa(\BC)$, $\rel(\BC)$, $\spa_a$, and $\rel_a$, are two-sided double categories.
\end{example}
%
\begin{definition}[Symmetric Double Relator]
An $F$-double relator $\relar$ over a two-sided double category $\BC_1\rightrightarrows\BC_0$ is a \emph{symmetric} double relator, whenever for every promorphism $\mathcal{R}$, the promorphism $\relar(\mathcal{R}^\op)$ is isomorphic to $(\relar\mathcal{R})^\op$.
\end{definition}
%
\begin{example}
Every relator $\relar$ is symmetric if and only if it is a symmetric double relator on $\rel_a\rightrightarrows\Set$.
Additionally, for every symmetric relator $\relar$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an $\relar$-bisimulation in coalgebras $(X,f)$ and $(Y,g)$ if and only if $((X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y),(f,g))$ is an $\relar$-double coalgebra on $\rel_a\rightrightarrows\Set$.
\end{example}
%
\begin{example}
For a category $\BC_0$ with pullbacks, every Aczel-Mendler bisimulation is an $\relar$-double coalgebra that $\relar$ is the map that takes every span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to a span $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$.
\end{example}
%
\begin{definition}[Barr Double Relator]
\todo{Finish}
\end{definition}
\begin{example}
For a category $\BC_0$ with pullbacks, every Hermida-Jacobs bisimulation is an $\relar$-double coalgebra that $\relar$ is the map that takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to a relation $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$.
\end{example}
%
\todo{Talk more about the poset enrichment here. You can say that in $\rel(\BC)\rightrightarrows\BC$ and $\spa(\BC)\rightrightarrows\BC$ an order enrichment on $F$ can be represented as a functor of type $\BC\to\spa(\BC)$ or $\BC\to\rel(\BC)$!}
\begin{definition}[Bi-laxed Barr Double Relator]
\todo{Finish}
\end{definition}
\begin{prop}
A span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an Aczel-Mendler simulation from a coalgebra $(X,g)$ to $(Y,h)$ with the morhpism $(g,h,w)$ if and only if it is a $((X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y),(g,h,w))$ is an $F^\leftrightarrow$-double coalgebra, and $F^\leftrightarrow$ is a bi-laxed Barr double relator.
\end{prop}
\begin{proof}
\todo{Finish}
\end{proof}
\todo{Investigate if double coalgebras form a (possibly double) category. If it is true find out what is the final object their!}
\subsection{Bisimulation in Double Categories}
\todo{Start writing this after the section for double categories in the previous section. You should first introduce your definition, and then give all the definitions as examples of your "double coalgebra".}
\subsection{Simulations in Double Categories}