From efb6fd8e6ab7701936069f6a16d43f35a1e6569a Mon Sep 17 00:00:00 2001 From: partowp Date: Thu, 9 Jul 2026 19:36:52 +0100 Subject: [PATCH] doesn't seem to work! --- draft/draft.tex | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index cac318c..8d19dcb 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2269,10 +2269,10 @@ So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra \qed \end{proof} -Now, we want to abstract the given proof for an arbitrary category that has coproducts and terminal objects (so that we have the maybe functor). We assume a natural order structure $\appr$ for the maybe functor. For every objects $X$ and $Y$, we define $\appr$ on each $\Hom(X,Y+1)$ by saying that for $f,g\in\Hom(X,Y+1)$ we have $f\appr g$ whenever either $f=g$ or $f=\bot$. +Now, we want to abstract the given proof for an extensive category that has terminal objects (so that we have the maybe functor). We assume a natural order structure $\appr$ for the maybe functor. For every objects $X$ and $Y$, we define $\appr$ on each $\Hom(X,Y+1)$ by saying that for $f,g\in\Hom(X,Y+1)$ we have $f\appr g$ whenever either $f=g$ or $f=\bot$. %Although even in the context that we are at the moment, it does not seem plausible to prove that a symmetric simulation is a bisimulation without having an operator like $\join$ in~\autoref{prop:sym-sim-bis-maybe} that takes two morphisms of the same type and gives one. \begin{lemma}\label{lem:maybe-lif-abs} - The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order.\ppnote{incomplete! Say why $(\alpha(x_1),\alpha(x_2))\in R+1$.} + The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order. \end{lemma} \begin{proof} For morphisms $h\c X\to Z+1$, $g\c Y\to Z$, and $k\c X\to Y+1$, we assume $h\appr g+1\comp k$ that means we have two cases: @@ -2281,11 +2281,12 @@ Now, we want to abstract the given proof for an arbitrary category that has copr \item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $g+1\comp k'=h$.\qed \end{itemize} \end{proof} +To have an abstraction of~\autoref{lem:maybe-func-set} recalling that our category extensive, we use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$. In our case, we take $\brks{\alpha\comp p_1,\alpha\comp p_2}\c R\to (X+1)\times(X+1)$, where $(X+1)\times (X+1)\iso X^2+(2\times X)+1$, and we assume the following pullbacks exist: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] - {I_{X^2}} \& R \& {I_{(2\times X)}} \& R \\ + {R_{X^2}} \& R \& {R_{2\times X}} \& R \\ {X^2} \& {X^2+(2\times X)+1} \& {(2\times X)} \& {X^2+(2\times X)+1} \\ - \& {I_1} \& R \\ + \& {R_1} \& R \\ \& 1 \& {X^2+(2\times X)+1} \arrow["{q_1}", from=1-1, to=1-2] \arrow["{q_2}"', from=1-1, to=2-1] @@ -2304,17 +2305,19 @@ Now, we want to abstract the given proof for an arbitrary category that has copr \arrow["{\mathsf{in}_3}"', from=4-2, to=4-3] \end{tikzcd} \end{equation*} -\begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - R \& I \& {X^2+(2\times X)+1} - \arrow["e", two heads, from=1-1, to=1-2] - \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}"', bend right=20, from=1-1, to=1-3] - \arrow["m", tail, from=1-2, to=1-3] - \end{tikzcd} -\end{equation*} +%\begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% R \& I \& {X^2+(2\times X)+1} +% \arrow["e", two heads, from=1-1, to=1-2] +% \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}"', bend right=20, from=1-1, to=1-3] +% \arrow["m", tail, from=1-2, to=1-3] +% \end{tikzcd} +%\end{equation*} +So, we have the following: \begin{gather*} - I\iso I_{X^2}+I_{2\times X}+I_{1} + R\iso R_{X^2}+R_{2\times X}+R_{1} \end{gather*} +And now we can use $q_2+r_2+s_2\c R_{X^2}+R_{2\times X}+R_{1}\to X^2+(2\times X)+1$ instead of $\brks{\alpha\comp p_1,\alpha\comp p_2}$. To prove~\autoref{lem:maybe-func-set} abstractly is to prove that $q_2+r_2+s_2$ factors through $X^2+1$. To achieve this, we need to show that $R_{2\times X}\iso 0$. \section{Relators} \subsection{Two-way similarity in Hughes-Jacobs} Hughes and Jacobs define two-way similarity as $\leq\cap\leq^\op$. They give a sufficient condition for the two-way similarity to be the bisimilarity. We discuss that this condition does not allow us to say that a symmetric simularity is a bisimilarity. The condition is: