From 0a0e89518995ce1850aed758cafa95263cfd2e72 Mon Sep 17 00:00:00 2001 From: partowp Date: Sun, 19 Jul 2026 18:29:26 +0100 Subject: [PATCH] liftable arvitrary F --- draft/draft.tex | 211 +++++++++++++++++++++++++++--------------------- 1 file changed, 119 insertions(+), 92 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 6eaec3a..82f3eb1 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -402,6 +402,117 @@ We want to say that a natural order structure entails an order over a functor de \begin{proof} We take $\tilde{F}X=\Hom(1,FX)$. Assuming that $U$ takes every poset to its carrier set, then we have $U\comp\tilde{F}X=FX$ for every object $X$.\qed \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'$. +\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'$. +\end{definition} + +\begin{lemma}\label{lem:set-ord-str} + In $\Set$, assuming that for every set $Y$ we have an order $\leq$ on $\Hom(1,FY)$ that satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, and if for $A\in\Hom(1,FZ)$, $B\in\Hom(1,FY)$, and $g\c Y\to Z$, $h\leq Fg(B)$ in $\Hom(1,FZ)$ there exists $B'\in\Hom(1,FY)$ such that $B'\leq B$ and $B\in\Hom(1,FY)$ and $A=Fg(B')$, then there exists an order structure $\appr$ on $F$ that is a liftable order structure. +\end{lemma} +\begin{proof} + For every $f,g\in\Hom(X,FY)$, we define $f\appr g$ whenever for all $x\in X$, $f(x)\leq g(x)$. + + Now, assuming $f\c X'\to X$, $\alpha,\beta\c X\to FY$, and $\alpha\appr\beta$, then for every $x'\in X'$, we have $\alpha(f(x'))\leq\beta(f(x'))$, so we have $\alpha\comp f\appr \beta\comp f$. Additionally, if we assume $g\c Y\to Y'$, then since $\leq$ satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, for every $x\in X$ we have $Fg\comp\alpha(x)\leq Fg\comp\beta(x)$. + + Furthermore, if we have $g\c Y\to Z$, $k\c X\to FY$, $h\c X\to FZ$, and $Fg\comp k\appr h$, then for every $x\in X$ we have $Fg\comp k(x)\leq h(x)$, thus by the assumption of the lemma, for every $x$, there exists a set that we call $k'(x)$, for which we have $Fg(k'(x))\leq h(x)$. So, we have a function $k'\c X\to FY$, such that for every $x$ we have $Fg\comp k'(x)\leq h(x)$ that means $Fg\comp k'\appr h$. + \qed +\end{proof} +\begin{remark}\label{rem:set-ord-str-co} + The exact same argument in~\autoref{lem:set-ord-str} is true for coliftable order structures. +\end{remark} + +\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} +\begin{proof} + Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf FZ)$, $k\in\Hom(1,\powf FY)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf Fg(k)$, we define $k'\in\powf FY$ that that $k'=\{y\mid Fg(y)\in h\}$. We show that $k'\subseteq k$ and $\powf Fg(k')=h$. + + Assuming $y\in k'$ we have $Fg(y)\in h$. Since $h\subseteq \powf Fg(k)$ we have $Fg(y)\in\powf Fh(h)$, so we have $y\in k$ that means $k'\subseteq k$. + + Assuming $z\in\powf Fg(k')$, then there exists $y'\in k'$ that $z=Fg(y')$, so $z\in h$ and $\powf Fg(k')\subseteq h$. + + Assuming $z\in h$, since $h\subseteq \powf Fg(k)$, then $z\in\powf Fg(k)$. So, there exists $y'\in k$ such that $Fg(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means $z\in\powf Fg(k')$.\qed +\end{proof} + +\begin{example} + In the category of sets, subset over the powerset functor is an example of a coliftable order structure if the $g$ in~\autoref{def:coliftable-ord} is a surjective. Using~\autoref{rem:set-ord-str-co} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, $g\c Y\to Z$, such that $\powf g(k)\subseteq h$. We define $k'=k\cup\{y\mid g(y)\in h\}$, and we show that $\powf g(k')=h$. + + Obviously, $\powf g(k')\subseteq h$. Now, assuming $z\in h$ we prove that $z\in \powf g(k')$. Since $g$ is surjective, then exists $A\subseteq Y$ such that $\powf g(A)=h$. By the definition of $k'$, $A\subseteq k'$. So from $z\in h$ we have $z\in \powf g(A)$ that means that exists $a\in A$, such that $g(a)=z$. Now, since $A\subseteq k'$, then $a\in k'$. So, we have $z\in \powf g(k')$.\qed +\end{example} + +\begin{remark} + We give an example that justifies why the $g$ in~\autoref{def:coliftable-ord} should be surjective. + If we take the surjectivity of $g$ out of~\autoref{def:coliftable-ord}, subset relation over the powerset functor is not an example of a coliftable order! For some set $X$ we take $h\c X\to\powf\mathbb{Z}$, for every $x\in X$, $h(x)=\mathbb{Z}$, $g\c\mathbb{Z}\to\mathbb{Z}$, and for every $z\in\mathbb{Z}$, + \begin{gather*} + g(z)= + \begin{cases} + 0 & z\in\mathbb{Z}^+ \\ + 1 & \mathsf{otherwise} + \end{cases} + \end{gather*} + then + \begin{gather*} + \powf g(A)= + \begin{cases} + \emptyset & A=\emptyset \\ + \{0\} & A\subseteq \mathbb{Z}^+,A\neq\emptyset\\ + \{1\} & A\subseteq \mathbb{Z}^-\cup\{0\},A\neq\emptyset\\ + \{0,1\} & \mathsf{otherwise} + \end{cases} + \end{gather*} + then no matter what $k\c X\to\powf\mathbb{Z}$ is there will be no $k'\c X\to\powf\mathbb{Z}$, for every $x\in X$, $\powf g(k'(x))=h(x)$, as $\powf g(k'(x))\subseteq\{0,1\}$, while $h(x)=\mathbb{Z}$, so $\powf g(k'(x))\subset h(x)$. +\end{remark} + +\begin{remark} + 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{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} +\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} + + \section{Coalgebraic Bisimulation}%\label{sec:} In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\ @@ -2953,65 +3064,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i % \end{enumerate} %\end{definition} -\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'$. -\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'$. -\end{definition} -\begin{lemma}\label{lem:set-ord-str} - In $\Set$, assuming that for every set $Y$ we have an order $\leq$ on $\Hom(1,FY)$ that satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, and if for $A\in\Hom(1,FZ)$, $B\in\Hom(1,FY)$, and $g\c Y\to Z$, $h\leq Fg(B)$ in $\Hom(1,FZ)$ there exists $B'\in\Hom(1,FY)$ such that $B'\leq B$ and $B\in\Hom(1,FY)$ and $A=Fg(B')$, then there exists an order structure $\appr$ on $F$ that is a liftable order structure. -\end{lemma} -\begin{proof} - For every $f,g\in\Hom(X,FY)$, we define $f\appr g$ whenever for all $x\in X$, $f(x)\leq g(x)$. - - Now, assuming $f\c X'\to X$, $\alpha,\beta\c X\to FY$, and $\alpha\appr\beta$, then for every $x'\in X'$, we have $\alpha(f(x'))\leq\beta(f(x'))$, so we have $\alpha\comp f\appr \beta\comp f$. Additionally, if we assume $g\c Y\to Y'$, then since $\leq$ satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, for every $x\in X$ we have $Fg\comp\alpha(x)\leq Fg\comp\beta(x)$. - - Furthermore, if we have $g\c Y\to Z$, $k\c X\to FY$, $h\c X\to FZ$, and $Fg\comp k\appr h$, then for every $x\in X$ we have $Fg\comp k(x)\leq h(x)$, thus by the assumption of the lemma, for every $x$, there exists a set that we call $k'(x)$, for which we have $Fg(k'(x))\leq h(x)$. So, we have a function $k'\c X\to FY$, such that for every $x$ we have $Fg\comp k'(x)\leq h(x)$ that means $Fg\comp k'\appr h$. - \qed -\end{proof} -\begin{remark}\label{rem:set-ord-str-co} - 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 $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} %\begin{prop} % For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a coliftable order structure $\appr$, the following propositions hold: % \begin{enumerate} @@ -3055,40 +3108,14 @@ 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{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$. - - Assuming $z\in\powf g(k')$, then there exists $y'\in \{y\mid g(y)\in h\}$ that $z=g(y')$, so $z\in h$ and $\powf g(k')\subseteq h$. - - Assuming $z\in h$, since $h\subseteq \powf g(k)$, then $z\in\powf g(k)$. So, there exists $y'\in k$ such that $g(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means $z\in\powf g(k')$.\qed -\end{example} -The following example justifies why the $g$ in~\autoref{def:coliftable-ord} should be surjective: -\begin{example} - If we take the surjectivity of $g$ out of~\autoref{def:coliftable-ord}, subset relation over the powerset functor is NOT an example of a coliftable order! For some set $X$ we take $h\c X\to\powf\mathbb{Z}$, for every $x\in X$, $h(x)=\mathbb{Z}$, $g\c\mathbb{Z}\to\mathbb{Z}$, and for every $z\in\mathbb{Z}$, - \begin{gather*} - g(z)= - \begin{cases} - 0 & z\in\mathbb{Z}^+ \\ - 1 & \mathsf{otherwise} - \end{cases} - \end{gather*} - then - \begin{gather*} - \powf g(A)= - \begin{cases} - \emptyset & A=\emptyset \\ - \{0\} & A\subseteq \mathbb{Z}^+,A\neq\emptyset\\ - \{1\} & A\subseteq \mathbb{Z}^-\cup\{0\},A\neq\emptyset\\ - \{0,1\} & \mathsf{otherwise} - \end{cases} - \end{gather*} - then no matter what $k\c X\to\powf\mathbb{Z}$ is there will be no $k'\c X\to\powf\mathbb{Z}$, for every $x\in X$, $\powf g(k'(x))=h(x)$, as $\powf g(k'(x))\subseteq\{0,1\}$, while $h(x)=\mathbb{Z}$, so $\powf g(k'(x))\subset h(x)$. -\end{example} -\begin{example} - In the category of sets, subset over the powerset functor is an example of a coliftable order structure if the $g$ in~\autoref{def:coliftable-ord} is a surjective. Using~\autoref{rem:set-ord-str-co} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, $g\c Y\to Z$, such that $\powf g(k)\subseteq h$. We define $k'=k\cup\{y\mid g(y)\in h\}$, and we show that $\powf g(k')=h$. - - Obviously, $\powf g(k')\subseteq h$. Now, assuming $z\in h$ we prove that $z\in \powf g(k')$. Since $g$ is surjective, then exists $A\subseteq Y$ such that $\powf g(A)=h$. By the definition of $k'$, $A\subseteq k'$. So from $z\in h$ we have $z\in \powf g(A)$ that means that exists $a\in A$, such that $g(a)=z$. Now, since $A\subseteq k'$, then $a\in k'$. So, we have $z\in \powf g(k')$.\qed -\end{example} +%\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$. +% +% Assuming $z\in\powf g(k')$, then there exists $y'\in \{y\mid g(y)\in h\}$ that $z=g(y')$, so $z\in h$ and $\powf g(k')\subseteq h$. +% +% Assuming $z\in h$, since $h\subseteq \powf g(k)$, then $z\in\powf g(k)$. So, there exists $y'\in k$ such that $g(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means $z\in\powf g(k')$.\qed +%\end{example} + \begin{definition}[Natural Relator] An $F$-relator $\relar$ is called \emph{natural}, whenever for every relation $r\c X\rto Y$, and all functions $f\c A\to X$, and $g\c B\to Y$, we have $\relar (g^\op\comp r\comp f)=(Fg)^\op\comp\relar r\comp Ff$. \end{definition}