Compare commits

...

3 Commits

Author SHA1 Message Date
partowp 487e71294f minor 2026-08-04 17:08:21 +01:00
partowp 007a0999b9 Merge branch 'master' of git.wlog.site:pouya/coalgebraic-simulation 2026-08-04 17:02:59 +01:00
partowp 2888c0d3a5 minor 2026-08-04 17:02:54 +01:00
+2 -10
View File
@@ -527,15 +527,7 @@ The order structure that we can define for this functor is that for sets $X$ and
% \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}
<<<<<<< HEAD
$(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\sappr)}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:
>>>>>>> 8c1054256a4ef67f109cc6d30f3d3bd050e936cb
\begin{gather*}
k'(x)=
\begin{cases}
@@ -558,7 +550,7 @@ The order structure that we can define for this functor is that for sets $X$ and
\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
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)\leq 1\}$ 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*}
@@ -571,7 +563,7 @@ The definition derives the ordering on morphisms of each hom-set $\Hom(X,\sub Y)
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$.\\
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')=\nu$.\\
The assumption $\nu \appr Sg(\mu)$ means that for every $y \in Y$,
\begin{gather*}
\nu(y) \leq Sg(\mu)(y) = \sum_{x \in g^{\mone}(y)} \mu(x).