diff --git a/draft/draft.tex b/draft/draft.tex index f1de9e7..3093ada 100644 --- a/draft/draft.tex +++ b/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} - 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: +\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: \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}