From 406fe32e54e26303620261f1122c989b30c478a3 Mon Sep 17 00:00:00 2001 From: partowp Date: Thu, 13 Aug 2026 17:50:01 +0100 Subject: [PATCH] bluh bluh --- draft/draft.tex | 37 ++++++++++++++++++++----------------- 1 file changed, 20 insertions(+), 17 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 373e08b..43fc677 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -3384,10 +3384,10 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \end{proof} \begin{definition}[Mid-lax Barr relator] - Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$, and $\pi_1$ and $\pi_2$ are surjective, assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{mid-lax Barr relator} if we have: + Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$, and $\pi_1$ and $\pi_2$ are surjective, assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\relar$ is a \emph{mid-lax Barr relator} if we have: % A relator over a functor $F$ is a one-sided Barr relator, shown by $\overrightarrow{F}$, iff for a partial order $\appr$ over $F$, a relation $r\c X\rto Y$, and a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$ we have: \begin{gather*} - \overrightarrow{F}r=F\pi_2\comp\appr\comp(F\pi_1)^\op + \relar=F\pi_2\comp\appr\comp(F\pi_1)^\op \end{gather*} \end{definition} @@ -3533,17 +3533,20 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \begin{proof} They all follow in an obvious way from~\autoref{lem:liftable} and~\autoref{lem:coliftable}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed \end{proof} +\begin{notation} + From now on we show relators $\bar{F}-\comp\appr$ with $F^\rightarrow$, $\appr\comp\bar{F}-$ with $F^\leftarrow$, and $\appr\comp\bar{F}-\comp\appr$ with $F^\leftrightarrow$. +\end{notation} \begin{prop}\label{prop:lax-relator-full-comm} For a functor $F$ with a liftable order we have: \begin{gather*} - (\bar{F}r\comp\appr)\subseteq(\appr\comp\bar{F}r) + F^\rightarrow r\leq F^\leftarrow r \end{gather*} \end{prop} \begin{proof} - Assuming $x \mathrel{(\bar{F}r\comp\appr)} y$ and $\bar{F}r=F\pi_2\comp(F\pi_1)^\op$, then there exist $x'$ and $p$ such that $x\appr x'$, $p\mathrel{F\pi_1}x'$, and $p\mathrel{F\pi_2}y$. So, we have $x\appr F\pi_1(p)$ then by liftability there exists $p'$ such that $p'\appr p$, and $F\pi_1(p')=x$. Then from $p'\appr p$ we get $F\pi_2(p')\appr y$ that is equivalent with $p' \mathrel{(\appr\comp F\pi_2)} y$, and then we have $x \mathrel{(\appr\comp F\pi_2\comp(F\pi_1)^\op)} y$.\qed + Assuming $x \mathrel{(F^\rightarrow r)} y$ and $\bar{F}r=F\pi_2\comp(F\pi_1)^\op$, then there exist $x'$ and $p$ such that $x\appr x'$, $p\mathrel{F\pi_1}x'$, and $p\mathrel{F\pi_2}y$. So, we have $x\appr F\pi_1(p)$ then by liftability there exists $p'$ such that $p'\appr p$, and $F\pi_1(p')=x$. Then from $p'\appr p$ we get $F\pi_2(p')\appr y$ that is equivalent with $p' \mathrel{(\appr\comp F\pi_2)} y$, and then we have $x \mathrel{(\appr\comp F\pi_2\comp(F\pi_1)^\op)} y$ that is $x\mathrel{(F^\leftarrow r)}y$.\qed \end{proof} \begin{cor} - Assuming that $r$ is an $(\bar{F}r\comp\appr)$-simulation, then it is an $(\appr\comp\bar{F}r)$-simulation as well. + Assuming that $r$ is an $F^\rightarrow$-simulation, if $\appr$ is liftable, then it is an $F^\leftarrow$-simulation as well. \end{cor} %\begin{example} % In the category of sets, subset over the powerset functor is an example of a liftable order. Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf g(k)$, we define $k'\in\powf Y$ that that $k'=\{y\mid g(y)\in h\}$. We show that $\powf g(k')=h$. @@ -3563,23 +3566,23 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i An $F$-relator $\relar$ is \emph{normal}, whenever for every set $X$, $\id_{FX}=\relar\id_X$. \end{definition} \begin{prop} - Every normal relational connect is difunctionally functorial.\qed + Every normal relational connector is difunctionally functorial.\qed \end{prop} \begin{prop} - Assuming that a set-functor $F$ has a liftable order structure $\appr$, then the $F$-relator $\relar r=\appr\comp Fr$ is natural. + Assuming that a set-functor $F$ has a liftable order structure $\appr$, then the relator $F^\leftarrow$ is natural. \end{prop} \begin{proof} \begin{align*} - \relar (g^\op\comp r\comp f)&\\ + F^\leftarrow (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 + =&(Fg)^\op\comp F^\leftarrow r\comp Ff \end{align*}\qed \end{proof} \begin{remark} - One may wonder if the above proposition is true for $F$-relators $r\mapsto Fr\comp\appr$ or $r\mapsto \appr\comp Fr\comp\appr$, where the order structure $\appr$ over $F$ is coliftable. But it may not be the case because the surjectivity condition on the $g$ in~\autoref{def:coliftable-ord} prevents the same reasoning. + One may wonder if the above proposition is true for relators $F^\rightarrow$ or $F^\leftrightarrow$, where the order structure $\appr$ over $F$ is coliftable. But it may not be the case because the surjectivity condition on the $g$ in~\autoref{def:coliftable-ord} prevents the same reasoning. \end{remark} \begin{prop} Symmetrization of a natural relator, is natural. @@ -3683,12 +3686,12 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat \end{proof} \todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion. See if~\autoref{prop:lax-relator-full-comm} or~\autoref{lem:lax-relator-str} can help!} % -%\begin{prop} -% For every functor $F\c\Set\to\Set$, assuming $\relar$ is the left-lax Barr relator for $F$, then for every relation $r\subseteq X\times Y$, we have $\hat{\relar}r\subseteq \bar{F}r$. -%\end{prop} -%\begin{proof} -% -%\end{proof} +\begin{prop}\label{prop:left-lax-inc-triv} + For every functor $F\c\Set\to\Set$, we have $\bar{F}\leq F^\leftarrow$. +\end{prop} +\begin{proof} + For a relation $r$, assuming $(x,y)\in \bar{F}r$, since $\appr$ is reflexive we have $y\mathrel{\appr}y$, so we have $x\mathrel{(\bar{F}\comp\appr)} y$ that is $(x,y)\in F^\leftarrow r$.\qed +\end{proof} % \subsection{Symmetric relation} \begin{prop} @@ -3706,7 +3709,7 @@ Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a Now, assuming $x\mathrel{r}y$ gives us $x\mathrel{(\alpha^\op\comp\relar r\comp \alpha)} y$ that is equivalent with saying that exist $x'$ and $y'$ such that $x\mathrel{\alpha}x'$, $y\mathrel{\alpha}y'$, and $x'\mathrel{\relar r}y'$. Since $r$ is symmetric, we have $y\mathrel{r} x$ that means that exist $x''$ and $y''$ such that $x\mathrel{\alpha}x''$, $y\mathrel{\alpha}y''$, and $y''\mathrel{\relar r}x''$. On the other hand since $\alpha$ is a function, we have $x''=x'$ and $y''=y'$, so we have $y'\mathrel{\relar r}x'$ that ultimately gives $x\mathrel{(\alpha^\op\comp\hat{\relar}r\comp\alpha)}y$. So, $r$ is an $\hat{\relar}$-bisimulation as well.\qed \end{proof} \begin{cor} - For a functor $F\c\Set\to\Set$, assuming that for a relation $r$ we have $\appr\comp\bar{F}r\leq\bar{F}r$, if $r$ is symmetric, and it is a $\appr\comp\bar{F}$-simulation, then it is a $\hat{\appr\comp\bar{F}}$-bisimulation.\ppnote{This is a bad notation for lax Barr-relators. Switch them with $F^\rightarrow$, $F^\leftarrow$, and $F^\leftrightarrow$.} + Recalling~\autoref{prop:left-lax-inc-triv}, for a functor $F\c\Set\to\Set$, assuming that $F^\leftarrow\leq\bar{F}$, we get $F^\leftarrow=\bar{F}$. So, if $r$ is symmetric, and it is a $F^\leftarrow$-simulation, then it is a $\bar{F}$-bisimulation. \end{cor} \end{document}