diff --git a/draft/draft.tex b/draft/draft.tex index 73ed9b4..3ea97a5 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2497,9 +2497,9 @@ The following example justifies why the $g$ in~\autoref{def:coliftable-ord} shou \begin{align*} \relar (g^\op\comp r\comp f)&\\ =&\appr\comp F(g^\op\comp r\comp f)\\ - =&\appr\comp(Fg^\op)\comp Fr\comp Ff\\ - =&(Fg^\op)\comp\appr\comp Fr\comp Ff&\by{\autoref{lem:liftable}}\\ - =&(Fg^\op)\comp\relar r\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\relar r\comp Ff \end{align*}\qed \end{proof} \begin{remark} @@ -2513,22 +2513,22 @@ The following example justifies why the $g$ in~\autoref{def:coliftable-ord} shou \begin{align*} \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\\ - =&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((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 \end{align*} So we are left to prove \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*} - 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*} - (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,\\ + (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 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 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*} - 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} \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.