liftablity

draft/draft.tex

@@ -304,6 +304,7 @@
 		}%
 	}%
 }
+\newcommand{\sub}{\mathcal{S}}
 
 
 \newcommand{\bba}{
@@ -474,6 +475,19 @@ We want to say that a natural order structure entails an order over a functor de
 	We could not prove a general statement like~\autoref{prop:lift-gen-func} for coliftability even if the surgectivity of $g$ remains in the definition. Perhaps more conditions on $F$ in~\autoref{prop:lift-gen-func} are needed. Conditions like preserving surjections and unions that make the statement extremely limited, and meaningless.
 \end{remark}
 
+\begin{example}
+	The subdistribution functor $\sub\c\Set\to\Set$ is defined as $\sub X=\{\mu\c X\to[0,1]\mid \sum_{x\in X}\mu(x)\}$ on objects, and for $\sub f\c \sub X\to\sub Y$, we have 
+	\begin{gather*}
+	\sub f(\mu)=y\mapsto\sum_{x\in f^{\mone}(y)}\mu(x),
+	\end{gather*}
+	on morphisms. We define the ordering on $\sub X$ for $\mu_1,\mu_2\in \sub X$ as
+	\begin{gather*}
+		\mu_1\appr \mu_2\iff \forall x\in X, \mu_1(x)\leq\mu_2(x).
+	\end{gather*} 
+	The definition derives the ordering on morphisms of each hom-set $\hom(X,\sub Y)$ as usual in $\Set$.\\
+	Assuming $\mu\in\sub X$, $g\c X\to Y$, $\nu\in\sub Y$, and $\nu\appr \sub g(\mu)$, we need to prove that there exists $\mu'\in \sub X$, that $\mu'\appr\mu$ and $\nu=\sub g(\mu')$.
+\end{example}
+
 \begin{lemma}\label{lem:liftable}
 	Assuming that a a functor $F$ has an order structure $\appr$ that is liftable, then for every $f\in\Hom(X,FY)$ we have:
 	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
@@ -3037,6 +3051,12 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	$\hat{L}$ is a Barr relator.
 \end{prop}
 \begin{proof}
+	We have
+	\begin{gather*}
+		\hat{\emre}r=\emre r\cap (\emre r^\op)^\op,\\
+		\hat{\emre}r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}\cap\{(T,S)\mid x\in S\Rightarrow \exists y\in T, y\;r\;x\}.
+	\end{gather*}
+	Assuming that $r=\pi_2\comp(\pi_1)^\op$ we have to prove that $\hat{L}r=\powf\pi_2\comp(\powf\pi_1)^\op$.
 	\todo{Finish.}
 \end{proof}
 
@@ -3199,6 +3219,9 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \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
 \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.
+\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$.
 %	
@@ -3336,6 +3359,7 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
 	\todo{Write it down. You have it in your notes.}
 \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!}
+\subsection{Symmetric relation}
 \begin{prop}
 Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a coalgebra $(X,\alpha)$, then $r$ is an $\hat{\relar}$-bisimulation.
 \end{prop}