naturally investigated

draft/draft.tex

@@ -2333,7 +2333,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	A \emph{good 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}[Cogood Order Structure]\label{def:cogood-ord}
-	A \emph{cogood 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)$, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
+	A \emph{cogood 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}
@@ -2370,16 +2370,16 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	So it follows directly from applying $\op$ on both sides of $(I)$.\qed 
 \end{proof}
 \begin{lemma}\label{lem:cogood}
-	Assuming that a a functor $F$ has an order structure $\appr$ that is cogood, then for every $f\in\Hom(X,FY)$ we have:
+	Assuming that a a functor $F$ has an order structure $\appr$ that is cogood, 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 cogood, 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$.
+	$(I)$ Assuming $t\mathrel{(Ff\comp\appr)} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is cogood, 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:cogood-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$.
+	Assuming $t\mathrel{(\appr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:cogood-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*}
@@ -2414,8 +2414,8 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 %	\end{gather*}
 %	Since $\appr$ is a cogood order structure by~\autoref{def:cogood-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}
+\begin{prop}\label{prop:all-rel-compa}
-	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $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)$, assuming that a set-functor $F$ has an order structure $\appr$, the following propositions hold:
 	\begin{enumerate}
 		\item If $\appr$ is good, 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 cogood, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad \appr\comp F\pi_2\comp(F\pi_1)^\op$
@@ -2438,8 +2438,9 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	
 	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:cogood-ord} should be surjective:
 \begin{example}
-	In the category of sets, subset over the powerset functor is NOT an example of a cogood 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}$, 
+	If we take the surjectivity of $g$ out of~\autoref{def:cogood-ord}, subset relation over the powerset functor is NOT an example of a cogood 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} 
@@ -2459,13 +2460,32 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	\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}
-The previous example suggests that cogoodness is a strong condition. It can be limited to be meaningful. If we limit it to the case where the $g$ in~\autoref{def:cogood-ord} is a surjection, we can use if for the scenario, where we have a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, where for a relation $r$, $r=\pi_2\comp\pi_1^\op$. Then we have the following:
 \begin{example}
 	In the category of sets, subset over the powerset functor is an example of a cogood order structure if the $g$ in~\autoref{def:cogood-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}
-\todo{Pedro!}
+\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}
+\begin{prop}
+	Assuming that a set-functor $F$ has a good order structure $\appr$, then the $F$-relator $\relar r=\appr\comp Fr$ is natural. 
+\end{prop}
+\begin{proof}
+	\begin{align*}
+		\relar (g^\op\comp r\comp f)&\\
+		=&\appr\comp F(g^\op\comp r\comp f)\\
+		=&\appr\comp(Fg^\op)\comp F(r)\comp F(f)\\
+		=&(Fg^\op)\comp\appr\comp F(r)\comp F(f)\\
+		=&(Fg^\op)\comp\relar r\comp F(f)
+	\end{align*}\qed
+\end{proof}
+\begin{cor}
+	By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is good, then the mid-lax relator is natural as well.
+\end{cor}
+\begin{remark}
+	One may wonder if the above proposition is true for $F$-relators $r\mapsto Fr\comp\appr$ or $r\mapsto \appr\comp Fr\comp\appr$, where the order structure $\appr$ over $F$ is cogood. But it is not the case because of the surjectivity condition on the $g$ in~\autoref{def:cogood-ord}.
+\end{remark}
 \begin{prop}
 	For a natural order structure $\appr$ on a set-functor $F$, if for every $f\in\Hom(X,FY)$ we have $Ff\comp\appr=\appr\comp Ff$, then $\appr$ is cogood.
 \end{prop}