From 986b6bdb24347741547cac38288ddc65a1e0ed74 Mon Sep 17 00:00:00 2001 From: partowp Date: Mon, 27 Apr 2026 14:58:48 +0100 Subject: [PATCH] more --- draft/draft.tex | 28 +++++++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index bed6a91..70dad02 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1836,7 +1836,24 @@ We need the case that $R_1=R_2$, and we refer to it with $R$. So, we need to hav \begin{gather*} \appr;(FR)^\dagger;\appr\quad\cap\quad\appr^\op;(FR)^\dagger;\appr^\op\qquad\subseteq\qquad(FR)^\dagger. \end{gather*} -Assuming $(x_1,x_2)\quad\in\quad \appr;(FR)^\dagger;\appr\quad\cap\quad\appr^\op;(FR)^\dagger;\appr^\op$ means that there exist $(u,v),(u',v')\in (FR)^\dagger$, such that $x_1\appr u$, $u'\appr x_1$, $v\appr x_2$, and $x_2\appr v'$. We can also use the symmetry of $R$, and then from $(x_1,x_2)\in R$ derive that there exist $(w,z),(w',z')$ such that $x_1\appr z$, $z'\appr x_1$, $w\appr x_2$, and $x_2\appr w'$. But then how can we derive $(x_1,x_2)\in (FR)^\dagger$? +Assuming $(x_1,x_2)\quad\in\quad \appr;(FR)^\dagger;\appr\quad\cap\quad\appr^\op;(FR)^\dagger;\appr^\op$ means that there exist $(u,v),(u',v')\in (FR)^\dagger$, such that $x_1\appr u$, $u'\appr x_1$, $v\appr x_2$, and $x_2\appr v'$. We can also use the symmetry of $R$, and then from $(x_1,x_2)\in R$ derive that there exist $(w,z),(w',z')$ such that $x_1\appr z$, $z'\appr x_1$, $w\appr x_2$, and $x_2\appr w'$. The situation can be illustrated as the following: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + {u'} \&\& u \& v \&\& {v'} \\ + \& {x_1} \&\&\& {x_2} \\ + {z'} \&\& z \& w \&\& {w'} + \arrow["\appr"{marking, allow upside down}, draw=none, from=1-1, to=2-2] + \arrow["\appr"{marking, allow upside down}, draw=none, from=1-4, to=2-5] + \arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=1-3] + \arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=3-3] + \arrow["\appr"{marking, allow upside down}, draw=none, from=2-5, to=1-6] + \arrow["\appr"{marking, allow upside down}, draw=none, from=2-5, to=3-6] + \arrow["\appr"{marking, allow upside down}, draw=none, from=3-1, to=2-2] + \arrow["\appr"{marking, allow upside down}, draw=none, from=3-4, to=2-5] + \end{tikzcd} +\end{equation*} + +But then how can we derive $(x_1,x_2)\in (FR)^\dagger$? \todo{Investigate more! Can it be doable really?!} \subsection{Uniqueness of the witness in Hughes-Jacobs definition} @@ -1926,7 +1943,7 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge For a relator $\relar$ on a functor $F$, and a poset $\appr$ over $F$ a HJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition): \begin{equation*}\label{def:hej-sim} \begin{tikzcd}[ampersand replacement=\&] - X \& R \& Y \\ + X \& r \& Y \\ {FX} \& {\appr;\relar r;\appr} \& {FY} \arrow["\alpha"', from=1-1, to=2-1] \arrow["{p_1}"', from=1-2, to=1-1] @@ -1942,16 +1959,17 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge Hughes-Jacobs simulation is an instance of HJ-simulation, where $\relar r=(Fr)^\dagger$. \end{prop} \begin{proof} - We need to show that $(F-)^\dagger$ is a relator, we need to show that + We need to show that $(F-)^\dagger$ is a relator. We need to show that for a relations $r_1$ and $r_2$, where $r_1\appr r_2$ we have $\relar r_1\appr \relar r_2$. (What is $\appr$?!) - \todo{Finish.} + \todo{Sergey claims this. Ask him how can he?} \end{proof} \begin{prop} - For an arbitrary relator $\relar$ on a functor $F$, if a relation $r$ is a simulation, the witness is unique. + For an arbitrary relator $\relar$ on a functor $F$, if a relation $r$ is a HJ-simulation, the witness is unique. \end{prop} \begin{proof} It only relies on the fact that ${Fp_1}_\appr$ and ${Fp_2}_\appr$ in~\eqref{def:hej-sim} are jointly monic.\qed \end{proof} + \end{document}