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

minor

Browse Source
This commit is contained in:
partowp
2026-06-11 17:01:07 +01:00
parent 8f306095ee
commit 08f1c1e782
1 changed files with 11 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+11 -11
View File
@@ -2497,9 +2497,9 @@ The following example justifies why the $g$ in~\autoref{def:coliftable-ord} shou
\begin{align*} \begin{align*}
\relar (g^\op\comp r\comp f)&\\ \relar (g^\op\comp r\comp f)&\\
=&\appr\comp F(g^\op\comp r\comp f)\\ =&\appr\comp F(g^\op\comp r\comp f)\\
=&\appr\comp(Fg^\op)\comp Fr\comp Ff\\ =&\appr\comp(Fg)^\op\comp Fr\comp Ff\\
=&(Fg^\op)\comp\appr\comp Fr\comp Ff&\by{\autoref{lem:liftable}}\\ =&(Fg)^\op\comp\appr\comp Fr\comp Ff&\by{\autoref{lem:liftable}}\\
=&(Fg^\op)\comp\relar r\comp Ff =&(Fg)^\op\comp\relar r\comp Ff
\end{align*}\qed \end{align*}\qed
\end{proof} \end{proof}
\begin{remark} \begin{remark}
@@ -2513,22 +2513,22 @@ The following example justifies why the $g$ in~\autoref{def:coliftable-ord} shou
\begin{align*} \begin{align*}
\hat{\relar}(g^\op\comp r\comp f)&\\ \hat{\relar}(g^\op\comp r\comp f)&\\
=&\relar(g^\op\comp r\comp f)\cap(\relar(f^\op\comp r^\op\comp g))^\op\\ =&\relar(g^\op\comp r\comp f)\cap(\relar(f^\op\comp r^\op\comp g))^\op\\
=&Fg^\op\comp\relar r\comp Ff\cap(Ff^\op\comp\relar r^\op\comp Fg)^\op\\ =&(Fg)^\op\comp\relar r\comp Ff\cap((Ff)^\op\comp\relar r^\op\comp Fg)^\op\\
=&Fg^\op\comp\relar r\comp Ff\cap Fg^\op\comp(\relar r^\op)^\op\comp Ff =&(Fg)^\op\comp\relar r\comp Ff\cap (Fg)^\op\comp(\relar r^\op)^\op\comp Ff
\end{align*} \end{align*}
So we are left to prove So we are left to prove
\begin{gather*} \begin{gather*}
Fg^\op\comp\relar r\comp Ff\cap Fg^\op\comp(\relar r^\op)^\op\comp Ff=Fg^\op\comp(\relar r\cap(\relar r^\op)^\op)\comp Ff (Fg)^\op\comp\relar r\comp Ff\cap (Fg)^\op\comp(\relar r^\op)^\op\comp Ff=(Fg)^\op\comp(\relar r\cap(\relar r^\op)^\op)\comp Ff
\end{gather*} \end{gather*}
because then we will have $\hat{\relar}(g^\op\comp r\comp f)=Fg^\op\comp\hat{\relar}\comp Ff$. We have because then we will have $\hat{\relar}(g^\op\comp r\comp f)=(Fg)^\op\comp\hat{\relar}\comp Ff$. We have
\begin{align*} \begin{align*}
(t,s)\in &Fg^\op\comp\relar r\comp Ff\cap Fg^\op\comp(\relar r^\op)^\op\comp Ff,\\ (t,s)\in &(Fg)^\op\comp\relar r\comp Ff\cap (Fg)^\op\comp(\relar r^\op)^\op\comp Ff,\\
&\iff(t,s)\in Fg^\op\comp\relar r\comp Ff\quad\&\quad (t,s)\in Fg^\op\comp(\relar r^\op)^\op\comp Ff,\\ &\iff(t,s)\in (Fg)^\op\comp\relar r\comp Ff\quad\&\quad (t,s)\in (Fg)^\op\comp(\relar r^\op)^\op\comp Ff,\\
&\iff Ff(t) \mathrel{(\relar r)} Fg(s) \quad\&\quad Ff(t) \mathrel{(\relar r^\op)^\op} Fg(s),\\ &\iff Ff(t) \mathrel{(\relar r)} Fg(s) \quad\&\quad Ff(t) \mathrel{(\relar r^\op)^\op} Fg(s),\\
&\iff Ff(t) \mathrel{(\relar\cap(\relar r^\op)^\op)} Fg(s),\\ &\iff Ff(t) \mathrel{(\relar\cap(\relar r^\op)^\op)} Fg(s),\\
&\iff t\mathrel{(Fg^\op\comp(\relar\cap(\relar r^\op)^\op)\comp Ff)} s. &\iff t\mathrel{((Fg)^\op\comp(\relar\cap(\relar r^\op)^\op)\comp Ff)} s.
\end{align*} \end{align*}
It worth noting that when we have $(t,s)\in Fg^\op\comp\relar r\comp Ff$, it mean that there exist $t'$ and $s'$ that $(t,t')\in Ff$, $(t',s')\in \relar r$, and $(s',s)\in Fg^\op$. Since $Ff$ and $Fg$ are functions, then $t'=Ff(t)$ and $s'=Fg(s)$, and these are unique elements. The uniqueness enables us in the above reasoning to go from the second line to the third line.\qed It worth noting that when we have $(t,s)\in (Fg)^\op\comp\relar r\comp Ff$, it mean that there exist $t'$ and $s'$ that $(t,t')\in Ff$, $(t',s')\in \relar r$, and $(s',s)\in Fg^\op$. Since $Ff$ and $Fg$ are functions, then $t'=Ff(t)$ and $s'=Fg(s)$, and these are unique elements. The uniqueness enables us in the above reasoning to go from the second line to the third line.\qed
\end{proof} \end{proof}
\begin{prop} \begin{prop}
If $\appr$ is an order structure on $F$ that for every sets $X$ and $Y$, $(\Hom(X,FY),\appr)$ is antisymmetric as well (making the posets), then the symmetrization of the left-lax Barr relator of $F$ and $\appr$ is normal. If $\appr$ is an order structure on $F$ that for every sets $X$ and $Y$, $(\Hom(X,FY),\appr)$ is antisymmetric as well (making the posets), then the symmetrization of the left-lax Barr relator of $F$ and $\appr$ is normal.