From e32d1eabb1d5dba132b8d3d501ba1396222d7c74 Mon Sep 17 00:00:00 2001 From: partowp Date: Tue, 9 Jun 2026 20:32:16 +0100 Subject: [PATCH] sound and complete! --- draft/draft.tex | 66 +++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 59 insertions(+), 7 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 3093ada..59c763c 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2468,6 +2468,16 @@ The following example justifies why the $g$ in~\autoref{def:cogood-ord} should b \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{definition}[Relaional Connector] + A natural $F$-relator $\relar$ is a \emph{relational connector}, whenever for every set $X$, $\id_{FX}\subseteq\relar\id_X$. +\end{definition} +\begin{definition}[Normal Relator] + An $F$-relator $\relar$ is \emph{normal}, whenever for every set $X$, $\id_{FX}=\relar\id_X$. +\end{definition} +\begin{prop} + Every normal relational connect is difunctionally functorial.\qed +\end{prop} + \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} @@ -2475,17 +2485,59 @@ The following example justifies why the $g$ in~\autoref{def:cogood-ord} should b \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) + =&\appr\comp(Fg^\op)\comp Fr\comp Ff\\ + =&(Fg^\op)\comp\appr\comp Fr\comp Ff&\by{\autoref{lem:good}}\\ + =&(Fg^\op)\comp\relar r\comp Ff + \end{align*}\qed +\end{proof} +\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 may not be the case because the surjectivity condition on the $g$ in~\autoref{def:cogood-ord} prevents the same reasoning. +\end{remark} +\begin{prop} + Symmetrization of a natural relator, is natural. +\end{prop} +\begin{proof} + Assuming $\relar$ is a natural $F$-relator, we prove that $\hat{\relar}$ is natural as well. Assuming $r\c X\rto Y$, $f\c A\to X$, and $g\c B\to Y$, by naturality of $\relar$ we have $\relar (g^\op\comp r\comp f)=Fg^\op\comp \relar r\comp Ff$. Then we have: + \begin{align*} + \hat{\relar}(g^\op\comp r\comp f)&\\ + =&\relar(g^\op\comp r\comp f)\cap(\relar(f^\op\comp r^\op\comp g))^\op\\ + =&Fg^\op\comp\relar r\comp Ff\cap(Ff^\op\comp\relar r^\op\comp Fg)^\op\\ + =&Fg^\op\comp\relar r\comp Ff\cap Fg^\op\comp(\relar r^\op)^\op\comp Ff + \end{align*} + So we are left to prove + \begin{gather*} + Fg^\op\comp\relar r\comp Ff\cap Fg^\op\comp(\relar r^\op)^\op\comp Ff=Fg^\op\comp(\relar r\cap(\relar r^\op)^\op)\comp Ff + \end{gather*} + because then we will have $\hat{\relar}(g^\op\comp r\comp f)=Fg^\op\comp\hat{\relar}\comp Ff$. We have + \begin{align*} + (t,s)\in &Fg^\op\comp\relar r\comp Ff\cap Fg^\op\comp(\relar r^\op)^\op\comp Ff,\\ + &\iff(t,s)\in Fg^\op\comp\relar r\comp Ff\quad\&\quad (t,s)\in Fg^\op\comp(\relar r^\op)^\op\comp Ff,\\ + &\iff Ff(t) \mathrel{(\relar r)} Fg(s) \quad\&\quad Ff(t) \mathrel{(\relar r^\op)^\op} Fg(s),\\ + &\iff Ff(t) \mathrel{(\relar\cap(\relar r^\op)^\op)} Fg(s),\\ + &\iff t\mathrel{(Fg^\op\comp(\relar\cap(\relar r^\op)^\op)\comp Ff)} s. + \end{align*} + It worth noting that when we have $(t,s)\in Fg^\op\comp\relar r\comp Ff$, it mean that there exist $t'$ and $s'$ that $(t,t')\in Ff$, $(t',s')\in \relar r$, and $(s',s)\in Fg^\op$. Since $Ff$ and $Fg$ are functions, then $t'=Ff(t)$ and $s'=Fg(s)$, and these are unique elements. The uniqueness enables us in the above reasoning to go from the second line to the third line.\qed +\end{proof} +\begin{prop} + If $\appr$ is an order structure on $F$ that for every sets $X$ and $Y$, $(\Hom(X,FY),\appr)$ is antisymmetric as well (making the posets), then the symmetrization of the left-lax Barr relator of $F$ and $\appr$ is normal. +\end{prop} +\begin{proof} + We show the left-lax Barr relator with $\relar$. We have: + \begin{align*} + \hat{\relar}\id&\\ + =&\relar\id\cap(\relar\id^\op)^\op\\ + =&\appr\comp F\id\cap (\appr\comp F\id^\op)^\op\\ + =&\appr\cap\sappr\\ + =&\id \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. + Since the symmetrization of left-lax Barr relator is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator. \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{cor} + By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is good, then the mid-lax Barr relator is a normal relation connector, and thus a sound and complete relator as well. +\end{cor} +Perhaps if we can relax the definition of good by allowing $g$ to be a relation rather than a function, we can have a lax Barr relator that its symmetrization is a normal lax extension.\todo{Investigate!} \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}