more

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}