liftable
This commit is contained in:
partowp
+134
-82
@@ -406,12 +406,12 @@ We want to say that a natural order structure entails an order over a functor de
|
||||
\end{proof}
|
||||
|
||||
\begin{definition}[Liftable Order Structure]\label{def:liftable-ord}
|
||||
A \emph{liftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $h\appr Fg\comp k$ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k'\appr k$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
|
||||
A \emph{liftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $h\appr Fg\comp k$ in $\Hom(X,FZ)$, and $g$ is surjective, then there is $k'\c X\to FY$ such that $k'\appr k$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.\ppnote{I added the surjection condition on $g$.}
|
||||
\end{definition}
|
||||
|
||||
|
||||
\begin{definition}[Coliftable Order Structure]\label{def:coliftable-ord}
|
||||
A \emph{coliftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, and $g$ is surjective, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
|
||||
A \emph{coliftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, and $g$ is surjective, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
|
||||
\end{definition}
|
||||
|
||||
\begin{lemma}\label{lem:set-ord-str}
|
||||
@@ -429,6 +429,47 @@ We want to say that a natural order structure entails an order over a functor de
|
||||
The exact same argument in~\autoref{lem:set-ord-str} is true for coliftable order structures.
|
||||
\end{remark}
|
||||
|
||||
\begin{lemma}\label{lem:liftable}
|
||||
Assuming that a a functor $F$ has an order structure $\appr$ that is liftable, then for every surjective $f\in\Hom(X,FY)$ we have:
|
||||
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
||||
\item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$
|
||||
\item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$
|
||||
\end{enumerate}
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
$(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$.
|
||||
|
||||
Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
|
||||
|
||||
$(II)$ Basically, by definition of $\op$ and relation composition we have
|
||||
\begin{gather*}
|
||||
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
|
||||
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
|
||||
\end{gather*}
|
||||
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
|
||||
\end{proof}
|
||||
\begin{lemma}\label{lem:coliftable}
|
||||
Assuming that a a functor $F$ has an order structure $\appr$ that is coliftable, then for every surjective $f\in\Hom(X,FY)$ we have:
|
||||
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
||||
\item $Ff\comp\appr\quad=\quad\appr\comp Ff$
|
||||
\item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$
|
||||
\end{enumerate}
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
$(I)$ Assuming $t\mathrel{(Ff\comp\appr)} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is coliftable, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{(\appr\comp Ff)} x$.
|
||||
|
||||
Assuming $t\mathrel{(\appr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:coliftable-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
|
||||
|
||||
$(II)$ Basically, by definition of $\op$ and relation composition we have
|
||||
\begin{gather*}
|
||||
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
|
||||
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
|
||||
\end{gather*}
|
||||
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
|
||||
\end{proof}
|
||||
|
||||
\subsection{Powerset Functor}
|
||||
In this section we discuss set inclusion as an ordering over the powerset functor.
|
||||
\begin{prop}\label{prop:lift-gen-func}
|
||||
For a functor $F\c\Set\to\Set$, a functor of the form $\powf F$, where $\powf$ is the powerset functor, the set inclusion is a liftable order structure.
|
||||
\end{prop}
|
||||
@@ -475,56 +516,98 @@ 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*)]
|
||||
\item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$
|
||||
\item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$
|
||||
\end{enumerate}
|
||||
\end{lemma}
|
||||
\subsection{Maybe Functor}
|
||||
The order structure that we can define for this functor is that for sets $X$ and $Y$, and functions $f,g\c X\to Y+1$ we have $f\appr g$ whenever $\Dom(f)\subseteq\Dom(g)$, and for every $x\in\Dom(f)$ we have $f(x)=g(x)$ ($\Dom(f)$ is the domain of a function $f$).
|
||||
\begin{prop}\label{prop:maybe-lif}
|
||||
The order structure on the set-functor $FX=X+1$ is a liftable order.
|
||||
\end{prop}
|
||||
% By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr Fg(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
|
||||
% \begin{itemize}
|
||||
% \item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$.
|
||||
% \item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed
|
||||
% \end{itemize}
|
||||
\begin{proof}
|
||||
$(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$.
|
||||
|
||||
Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
|
||||
|
||||
$(II)$ Basically, by definition of $\op$ and relation composition we have
|
||||
Assuming that $h\in\Hom(X,Z+1)$, $g\c Y\to Z$, $k\in\Hom(X,Y+1)$, such that $h\appr (g+1)\comp k$. We define $k'\in\Hom(X,Y+1)$ as follows:
|
||||
\begin{gather*}
|
||||
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
|
||||
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
|
||||
k'(x)=
|
||||
\begin{cases}
|
||||
\bot&x\notin\Dom(h)\\
|
||||
k(x)&x\in\Dom(h)
|
||||
\end{cases}
|
||||
\end{gather*}
|
||||
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
|
||||
We have $\Dom((g+1)\comp k')=\Dom(k')$ and $\Dom(k')=\Dom(h)$, so we have $\Dom((g+1)\comp k')=\Dom(h)$. If $x\in\Dom(h)$, then $h(x)=(g+1)\comp k(x)$ and $(g+1)\comp k(x)=(g+1)\comp k'(x)$, so we have $h(x)=(g+1)\comp k'(x)$. So, we have $h=(g+1)\comp k'$. Additionally, $\Dom(k')\subseteq\Dom(k)$, and for every $x\in \Dom(k')$, we have $k'(x)=k(x)$, so we have $k'\appr k$. \qed
|
||||
\end{proof}
|
||||
\begin{lemma}\label{lem:coliftable}
|
||||
Assuming that a a functor $F$ has an order structure $\appr$ that is coliftable, then for every surjective $f\in\Hom(X,FY)$ we have:
|
||||
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
|
||||
\item $Ff\comp\appr\quad=\quad\appr\comp Ff$
|
||||
\item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$
|
||||
\end{enumerate}
|
||||
\end{lemma}
|
||||
\begin{prop}\label{prop:maybe-colif}
|
||||
The order structure on the set-functor $FX=X+1$ is a coliftable order.
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
$(I)$ Assuming $t\mathrel{(Ff\comp\appr)} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is coliftable, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{(\appr\comp Ff)} x$.
|
||||
|
||||
Assuming $t\mathrel{(\appr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:coliftable-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
|
||||
|
||||
$(II)$ Basically, by definition of $\op$ and relation composition we have
|
||||
By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $Fg(k)\appr h$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k\appr k'$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
|
||||
\begin{itemize}
|
||||
\item $Fg(k)=h$: In this case we take $k'=k$, and then we have $Fg(k')=h$.
|
||||
|
||||
\item $Fg(k)=\bot$: It entails that $k=\bot$. We either have $h=\bot$ or $h\in Y$. If $h=\bot$ then we take $k'=k$, and we are done. If $h\in Y$, then by the surjectivity of $g$, there exists $k'$ such that $g(k')=h$ that entails $Fg(k')=h$ as well.\qed
|
||||
\end{itemize}
|
||||
\end{proof}
|
||||
|
||||
\subsection{Subdistribution Functor}
|
||||
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$.
|
||||
\begin{prop}
|
||||
The pointwise ordering on $\sub$ is a liftable ordering.
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
Assuming that $\mu\in SX$, $g\c X\to Y$ is surjective, $\nu\in SY$, and $\nu\appr \sub g(\mu)$, then there exists $\mu'\in \sub X$ such that $\mu'\appr \mu$ and $\sub g(\mu')=h$.\\
|
||||
The assumption $\nu \appr Sg(\mu)$ means that for every $y \in Y$,
|
||||
\begin{gather*}
|
||||
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
|
||||
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
|
||||
\nu(y) \leq Sg(\mu)(y) = \sum_{x \in g^{\mone}(y)} \mu(x).
|
||||
\end{gather*}
|
||||
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
|
||||
We construct $\mu'$ as follows:
|
||||
\begin{gather*}
|
||||
\mu'(x)=
|
||||
\begin{cases}
|
||||
\frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)&Sg(\mu)(g(x))\neq 0\\
|
||||
0&Sg(k)(g(x))= 0
|
||||
\end{cases}
|
||||
\end{gather*}
|
||||
First, we need to prove that $\mu'$ is a subdistribution.
|
||||
For every $x \in X$, $\mu'(x) \ge 0$. The total mass of $\mu'$ is
|
||||
\begin{align*}
|
||||
\sum_{x \in X} \mu'(x)&\\
|
||||
=& \sum_{x \in X} \frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)\\
|
||||
=& \sum_{y \in Y} \sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)\\
|
||||
=& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)\\
|
||||
=& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)\\
|
||||
=& \sum_{y \in Y} \nu(y)\\
|
||||
\leq& 1
|
||||
\end{align*}
|
||||
Thus $\mu'$ is a subdistribution. Now, we prove $Sg(\mu') = \nu$.
|
||||
For any $y \in Y$, we have:
|
||||
\begin{align*}
|
||||
Sg(\mu')(y)&\\
|
||||
= &\sum_{x \in g^{\mone}(y)} \mu'(x)\\
|
||||
= &\sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)\;\;(Sg(\mu)(y)\neq 0)\\
|
||||
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)\;\;(Sg(\mu)(y)\neq 0)\\
|
||||
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)\;\;(Sg(\mu)(y)\neq 0)\\
|
||||
= &\mu(y)
|
||||
\end{align*}
|
||||
(If $Sg(\mu)(y) = 0$, then $\nu(y) = 0$, and the sum is $0$ as well, so the equality still holds.) \\
|
||||
Now, we are left to prove that $\mu'\appr\mu$.
|
||||
For every $x\in X$, have the following cases:
|
||||
\begin{itemize}
|
||||
\item $Sg(\mu)(g(x))= 0$: We have $\mu'(x)=0$, and obviously $\mu'\appr\mu$.
|
||||
\item $Sg(\mu)(g(x))\neq 0$: We have $\frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)$, and since $\nu\appr Sg(\mu)$ then we have:
|
||||
\begin{align*}
|
||||
&\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\leq 1\\
|
||||
\Rightarrow&\quad\frac{\nu(g(x))}{Sg(\mu)(g(x))}\comp \mu(x)\leq \mu(x)
|
||||
\end{align*}\qed
|
||||
\end{itemize}
|
||||
\end{proof}
|
||||
|
||||
|
||||
@@ -2400,39 +2483,8 @@ Now, we prove our main statement.
|
||||
\end{cor}
|
||||
Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor.
|
||||
\subsection{Maybe Functor}
|
||||
We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for sets $X$ and $Y$, and functions $f,g\c X\to Y+1$ we have $f\appr g$ whenever $\Dom(f)\subseteq\Dom(g)$, and for every $x\in\Dom(f)$ we have $f(x)=g(x)$ ($\Dom(f)$ is the domain of a function $f$).
|
||||
Now, we prove that the given order on the maybe functor is liftable and coliftable.
|
||||
\begin{lemma}\label{lem:maybe-lif}
|
||||
The order structure on the set-functor $FX=X+1$ is a liftable order.
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
% By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr Fg(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
|
||||
% \begin{itemize}
|
||||
% \item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$.
|
||||
% \item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed
|
||||
% \end{itemize}
|
||||
Assuming that $h\in\Hom(X,Z+1)$, $g\c Y\to Z$, $k\in\Hom(X,Y+1)$, such that $h\appr (g+1)\comp k$. We define $k'\in\Hom(X,Y+1)$ as follows:
|
||||
\begin{gather*}
|
||||
k'(x)=
|
||||
\begin{cases}
|
||||
\bot&x\notin\Dom(h)\\
|
||||
k(x)&x\in\Dom(h)
|
||||
\end{cases}
|
||||
\end{gather*}
|
||||
We have $\Dom((g+1)\comp k')=\Dom(k')$ and $\Dom(k')=\Dom(h)$, so we have $\Dom((g+1)\comp k')=\Dom(h)$. If $x\in\Dom(h)$, then $h(x)=(g+1)\comp k(x)$ and $(g+1)\comp k(x)=(g+1)\comp k'(x)$, so we have $h(x)=(g+1)\comp k'(x)$. So, we have $h=(g+1)\comp k'$. Additionally, $\Dom(k')\subseteq\Dom(k)$, and for every $x\in \Dom(k')$, we have $k'(x)=k(x)$, so we have $k'\appr k$. \qed
|
||||
\end{proof}
|
||||
\begin{lemma}\label{lem:maybe-colif}
|
||||
The order structure on the set-functor $FX=X+1$ is a coliftable order.
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $Fg(k)\appr h$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k\appr k'$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
|
||||
\begin{itemize}
|
||||
\item $Fg(k)=h$: In this case we take $k'=k$, and then we have $Fg(k')=h$.
|
||||
|
||||
\item $Fg(k)=\bot$: It entails that $k=\bot$. We either have $h=\bot$ or $h\in Y$. If $h=\bot$ then we take $k'=k$, and we are done. If $h\in Y$, then by the surjectivity of $g$, there exists $k'$ such that $g(k')=h$ that entails $Fg(k')=h$ as well.\qed
|
||||
\end{itemize}
|
||||
\end{proof}
|
||||
So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alpha)$ of a functor with a liftable order, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=Fp_1\comp\sigma$.
|
||||
We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$.\\
|
||||
Proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alpha)$ of a functor with a liftable order, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=Fp_1\comp\sigma$. We have shown that the ordering on the maybe functor is liftable and coliftalbe in~\autoref{prop:maybe-lif} and~\autoref{prop:maybe-colif}
|
||||
%\begin{lemma}\label{lem:maybe-func-set}
|
||||
% Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$
|
||||
% \begin{gather*}
|
||||
@@ -2441,7 +2493,7 @@ So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alph
|
||||
% \end{gather*}
|
||||
%\end{lemma}
|
||||
%\begin{proof}
|
||||
% By~\autoref{prop:alph-prod-dubut} and~\autoref{lem:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $Fp_1\comp\sigma=\alpha\comp p_1$. %Since $R$ is symmetric, for every $(x_1,x_2)\in R$ we have the following\sgnote{Consider noting which facts come from the pair $(x_1,x_2)$ (namely \eqref{eq:maybe-func-set-1} and \eqref{eq:maybe-func-set-4}) and which from $(x_2,x_1)$ (namely \eqref{eq:maybe-func-set-2} and \eqref{eq:maybe-func-set-3}); it saves the reader from reconstructing it.}:
|
||||
% By~\autoref{prop:alph-prod-dubut} and~\autoref{prop:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $Fp_1\comp\sigma=\alpha\comp p_1$. %Since $R$ is symmetric, for every $(x_1,x_2)\in R$ we have the following\sgnote{Consider noting which facts come from the pair $(x_1,x_2)$ (namely \eqref{eq:maybe-func-set-1} and \eqref{eq:maybe-func-set-4}) and which from $(x_2,x_1)$ (namely \eqref{eq:maybe-func-set-2} and \eqref{eq:maybe-func-set-3}); it saves the reader from reconstructing it.}:
|
||||
%% \begin{enumerate}
|
||||
%% \item $\alpha(x_1)=Fp_1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}
|
||||
%% \item $\alpha(x_2)=Fp_1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}
|
||||
@@ -2585,7 +2637,7 @@ Assuming $f,g\in\Hom(X,Y+1)$, and that $f'\c X_f\rightarrowtail X$ and $g'\c X_g
|
||||
\arrow["{f'}"', tail, from=2-1, to=1-2]
|
||||
\end{tikzcd}
|
||||
\end{equation*}
|
||||
\begin{lemma}\label{lem:maybe-lif-abs}
|
||||
\begin{lemma}\label{prop:maybe-lif-abs}
|
||||
The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order.
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
@@ -3061,7 +3113,7 @@ 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$. 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 $\overrightarrow{F}$ 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
|
||||
@@ -3194,7 +3246,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
|
||||
% Since $\appr$ is a coliftable order structure by~\autoref{def:coliftable-ord} there exists a $w$ such that $z\appr w$ and $F\pi_j(w)=y$. So, we have $w \mathrel{(F\pi_j)} y$, $z\mathrel{\appr} w$, and $z\mathrel{(F\pi_i)} x$ that gives $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$.\qed
|
||||
%\end{proof}
|
||||
\begin{prop}\label{prop:all-rel-compa}
|
||||
For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that a set-functor $F$ has an order structure $\appr$, the following propositions hold:
|
||||
For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $\pi_1$ and $\pi_2$ are surjective, assuming that a set-functor $F$ has an order structure $\appr$, the following propositions hold:
|
||||
\begin{enumerate}
|
||||
\item If $\appr$ is liftable, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad F\pi_2\comp(F\pi_1)^\op\comp\appr$
|
||||
\item If $\appr$ is coliftable, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad \appr\comp F\pi_2\comp(F\pi_1)^\op$
|
||||
|
||||
Reference in New Issue
Block a user