From 1a3e7ec1a940bbb6ba5a0f818ba1d72407525a4c Mon Sep 17 00:00:00 2001 From: partowp Date: Tue, 26 May 2026 16:25:28 +0100 Subject: [PATCH] proof and counter-example --- draft/draft.tex | 89 ++++++++++++++++++++++++++++++++++--------------- 1 file changed, 62 insertions(+), 27 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 33f7263..b7cc2c4 100644 --- a/draft/draft.tex +++ b/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} - 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} - \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$ - \end{enumerate} -\end{prop} -\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$. - - Assuming $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that - \begin{gather*} - z \mathrel{(F\pi_i)} x,\\ - z \mathrel{\appr} z',\\ - z'\mathrel{(F\pi_j)} y. - \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$. - - 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*} - z\mathrel{(F\pi_i)} x,\\ - z \mathrel{(F\pi_j)} y',\\ - y' \mathrel{\appr} y. - \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 a cogood order structure $\appr$, the following propositions hold: +% \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_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$ +% \end{enumerate} +%\end{prop} +%\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$. +% +% Assuming $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that +% \begin{gather*} +% z \mathrel{(F\pi_i)} x,\\ +% z \mathrel{\appr} z',\\ +% z'\mathrel{(F\pi_j)} y. +% \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$. +% +% 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*} +% z\mathrel{(F\pi_i)} x,\\ +% z \mathrel{(F\pi_j)} y',\\ +% y' \mathrel{\appr} y. +% \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{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}