a prop

draft/draft.tex

@@ -389,7 +389,7 @@ Pouya Partow\inst{1}\orcidID{0009-0003-9652-9469}}
 \end{abstract}
 %
 %
-\section{Relation Lifting}
+\section{Liftable Orders}
 \begin{definition}[Natural Order Structure]\label{def:nat-ord}
 	A \emph{natural order structure} on a functor $F$ is a poset $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that if $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X'\to X$, $g\c Y\to Y'$, then:
 	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
@@ -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)$ 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$.}
+	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 epic, 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)$ 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 epic, 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}
@@ -468,6 +468,17 @@ We want to say that a natural order structure entails an order over a functor de
 	So it follows directly from applying $\op$ on both sides of $(I)$.\qed 
 \end{proof}
 
+\begin{prop}
+	Assuming that $F$ and $G$ are endofunctors on a category $\BC$, and $\appr$ is a liftable order structure on $F$, if $G$ preserves epics, then $\appr$ is a liftable order structure on $FG$ as well.
+\end{prop}
+\begin{proof}
+	$\appr$ being a liftable order structure on $F$ means that for morphisms $g\c Y\to Z$, $k\in\Hom(X,FY)$, and $h\in\Hom(X,FZ)$ that $g$ is epic, if $h\appr Fg\comp k$ then exists $k'\in\Hom(X,FY)$, such that $k\appr k'$ and $h=Fg\comp k'$. %Now, assuming $\alpha\c Y\to Z$, $\mu\in\Hom(X,FGY)$, and $\nu\in\Hom(X,FGZ)$ that $\alpha$ is epic, we need to prove that exists some $\mu'\in\Hom(X,FGY)$ such that $\mu'\appr\mu$ and $\nu=FG\alpha\comp\mu'$. Since $G$ preserves epimorphisms and $\alpha$ is epic, then $G\alpha$ is also epic. Furthermore, since $\appr$ is a liftable order structure on $F$, then the mentioned $\mu'$ exists.\qed  
+	Now, assuming $\alpha\c Y\to Z$, $\mu\in\Hom(X,FGY)$, and $\nu\in\Hom(X,FGZ)$ that $\alpha$ is epic. Since $G$ is assumed to preserve epimorphisms, $G\alpha$ is epic. Since $\appr$ is a liftable order structure on $F$, then there exists some $\mu'\in\Hom(X,FGY)$ such that $\mu'\appr\mu$ and $\nu=FG\alpha\comp\mu'$. So, $\appr$ is a liftable order structure for $FG$ as well.\qed
+\end{proof}
+\todo{It seems too much, but perhaps you can study if you can derive an order structure from $F$ to $G$ and consequently $GF$, by the following rule:
+\begin{gather*}
+	\infer{Gh\appr GFg\comp Gk}{h\appr Fg\comp k}
+	\end{gather*}}
 \subsection{Powerset Functor}
 In this section we discuss set inclusion as an ordering over the powerset functor.
 \begin{prop}\label{prop:lift-gen-func}