proof and counter-example

draft/draft.tex

@@ -2334,6 +2334,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \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'$.
 \end{definition}
+
 \begin{lemma}\label{lem:good}
 	Assuming that a a functor $F$ has an order structure $\appr$ that is good, then for every $f\in\Hom(X,FY)$ we have:
 	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
@@ -2372,32 +2373,32 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	\end{gather*}
 	So it follows directly from applying $\op$ on both sides of $(I)$.\qed 
 \end{proof}
-\begin{prop}
+%\begin{prop}
-	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold:
+%	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold:
-	\begin{enumerate}
+%	\begin{enumerate}
-		\item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$
+%		\item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$
-		\item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$
+%		\item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$
-	\end{enumerate}
+%	\end{enumerate}
-\end{prop}
+%\end{prop}
-\begin{proof}
+%\begin{proof}
-	Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $F\pi_j\comp\appr\comp(F\pi_i)^\op\quad=\quad\appr\comp F\pi_j\comp(F\pi_i)^\op$.
+%	Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $F\pi_j\comp\appr\comp(F\pi_i)^\op\quad=\quad\appr\comp F\pi_j\comp(F\pi_i)^\op$.
-	
+%	
-	Assuming $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that
+%	Assuming $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that
-	\begin{gather*}
+%	\begin{gather*}
-		z \mathrel{(F\pi_i)} x,\\
+%		z \mathrel{(F\pi_i)} x,\\
-		z \mathrel{\appr} z',\\
+%		z \mathrel{\appr} z',\\
-		z'\mathrel{(F\pi_j)} y.
+%		z'\mathrel{(F\pi_j)} y.
-	\end{gather*}
+%	\end{gather*}
-	Then from $z \mathrel{\appr} z'$ since $\appr$ is a cogood order structure by~\ref{item:nat-ord:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$.
+%	Then from $z \mathrel{\appr} z'$ since $\appr$ is a cogood order structure by~\ref{item:nat-ord:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$.
-	
+%	
-	Now, assuming $x \mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
+%	Now, assuming $x \mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
-	\begin{gather*}
+%	\begin{gather*}
-		z\mathrel{(F\pi_i)} x,\\
+%		z\mathrel{(F\pi_i)} x,\\
-		z \mathrel{(F\pi_j)} y',\\
+%		z \mathrel{(F\pi_j)} y',\\
-		y' \mathrel{\appr} y.
+%		y' \mathrel{\appr} y.
-	\end{gather*}
+%	\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
+%	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}
+%\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{enumerate}
@@ -2415,6 +2416,41 @@ 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:good} and~\autoref{lem:cogood}. 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 good order. For every $h\c X\to\powf Z$, $k\c X\to \powf Y$, and $g\c Y\to Z$, such that $h\subseteq\powf g\comp k$, there exists $k'\c X\to\powf Y$ that for every $x\in X$, $k'(x)=k(x)\setminus\{y\mid g(y)\notin h(x)\}$. We show that for every $x\in X$, we have $\powf g\comp k'(x)=h(x)$.
+	
+	Assuming $z\in\powf g(k'(x))$, then there exist $y'\in k(x)\setminus \{y\mid g(y)\notin h(x)\}$ that $g(y')=z$, so $y'\in k(x)$, $y'\notin\{y\mid g(y)\notin h(x)\}$. $y'\notin\{y\mid g(y)\notin h(x)\}$ means that $g(y')\in h(x)$, thus $\powf g\comp k'\subseteq h$.
+	
+	Assuming $z\in h(x)$, since $h\subseteq \powf g\comp k$, then $z\in\powf g\comp k(x)$. So, there exists $y'$ such that $y'\in k(x)$ and $g(y')=z$. Since $g(y')\in h(x)$ then $y'\notin\{y\mid g(y)\notin h(x)\}$ meaning that $y'\in k'(x)$ that means $z\in \powf g(k'(x))$, thus $h\subseteq \powf g\comp k'$.\qed
+\end{example}
+\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}$, 
+	\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}
+The previous example suggests that cogoodness is a strong condition. Perhaps it can be limited to be meaningful. Maybe the morphism $g$ can be limited to legs of 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$.
+\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}
+\begin{proof}
+	\todo{Investigate if it's true! If it is, is naturality necessary? It is really weird! If having a good order structure forces every witness for AM-simulation to have the left cell of the lax diagram as equality, and subset on powerset functor is a good order structure, then what is the counter-example number 4 that you have?!}
+\end{proof}
 \begin{prop}
 	Assuming that $\relar$ is a difunctionally functorial relator, then the symmetrization of the relator that takes $r\c X\rto Y$ to $\relar r\comp\appr$ is a sound relator. 
 \end{prop}
@@ -2427,7 +2463,6 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \begin{proof}
 	\todo{Finish.}
 \end{proof}
-
 \end{document}