From d87ecf12fb59f4b36c57d612aaa820d1d985685d Mon Sep 17 00:00:00 2001 From: partowp Date: Wed, 15 Jul 2026 13:12:14 +0100 Subject: [PATCH] The concrete proof for maybe revisited --- draft/draft.tex | 145 +++++++++++++++++++++++++++++++----------------- 1 file changed, 93 insertions(+), 52 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 03d1f1f..4c8a3ea 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2206,7 +2206,7 @@ Now, we prove that the given order on the maybe functor is a liftable one. \end{itemize} \end{proof} \begin{lemma}\label{lem:maybe-colif} - The order structure on the set-functor $FX=X+1$ is a liftable order. + The order structure on the set-functor $FX=X+1$ is a coliftable order. \end{lemma} \begin{proof} By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $Fg(k)\appr h$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k\appr k'$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases: @@ -2217,64 +2217,106 @@ Now, we prove that the given order on the maybe functor is a liftable one. \end{itemize} \end{proof} So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra $(X,\alpha)$ of the maybe functor, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=Fp_1\comp\sigma$. -\begin{lemma}\label{lem:maybe-func-set} - Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ - \begin{gather*} - \alpha(x_1)\in X\Rightarrow \alpha(x_2)\in X\\ - \alpha(x_1)=\bot \Rightarrow \alpha(x_2)=\bot - \end{gather*} -\end{lemma} -\begin{proof} - By~\autoref{prop:alph-prod-dubut} and~\autoref{lem:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $Fp_1\comp\sigma=\alpha\comp p_1$. Since $R$ is symmetric, for every $(x_1,x_2)\in R$ we have the following\sgnote{Consider noting which facts come from the pair $(x_1,x_2)$ (namely \eqref{eq:maybe-func-set-1} and \eqref{eq:maybe-func-set-4}) and which from $(x_2,x_1)$ (namely \eqref{eq:maybe-func-set-2} and \eqref{eq:maybe-func-set-3}); it saves the reader from reconstructing it.}: - \begin{enumerate} - \item $\alpha(x_1)=Fp_1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1} - \item $\alpha(x_2)=Fp_1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2} - \item $\alpha(x_1)\sappr Fp_2\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3} - \item $\alpha(x_2)\sappr Fp_2\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4} - \end{enumerate} - Now, we have two cases: - \begin{itemize} - \item Assuming $\alpha(x_1)\in X$ then by~\eqref{eq:maybe-func-set-1} we have $Fp_1\comp\sigma(x_1,x_2)\in X$, thus $\sigma(x_1,x_2)\in R$. So, we have $Fp_2\comp\sigma(x_1,x_2)\in X$ that by~\eqref{eq:maybe-func-set-4} means $\alpha(x_2)\in X$. - \item Assuming $\alpha(x_1)=\bot$ then by~\eqref{eq:maybe-func-set-3} we have $Fp_2\comp\sigma(x_2,x_1)=\bot$, thus $\sigma(x_2,x_1)=\bot$. So, we have $Fp_1\comp\sigma(x_2,x_1)=\bot$ that by~\eqref{eq:maybe-func-set-2} means $\alpha(x_2)=\bot$ as well.\qed - \end{itemize} -\end{proof} -%\begin{proof} -% We assume that $\sigma\c R\to R+1$ is the witness that we have for $R$ to be an AM-simulation. We prove the statement by contradiction. If the statement is false, then we either have +%\begin{lemma}\label{lem:maybe-func-set} +% Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ % \begin{gather*} -% \alpha(x_1)\in X\quad\&\quad \alpha(x_2)=\bot, +% \alpha(x_1)\in X\Rightarrow \alpha(x_2)\in X\\ +% \alpha(x_1)=\bot \Rightarrow \alpha(x_2)=\bot +% \end{gather*} +%\end{lemma} +%\begin{proof} +% By~\autoref{prop:alph-prod-dubut} and~\autoref{lem:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $Fp_1\comp\sigma=\alpha\comp p_1$. %Since $R$ is symmetric, for every $(x_1,x_2)\in R$ we have the following\sgnote{Consider noting which facts come from the pair $(x_1,x_2)$ (namely \eqref{eq:maybe-func-set-1} and \eqref{eq:maybe-func-set-4}) and which from $(x_2,x_1)$ (namely \eqref{eq:maybe-func-set-2} and \eqref{eq:maybe-func-set-3}); it saves the reader from reconstructing it.}: +%% \begin{enumerate} +%% \item $\alpha(x_1)=Fp_1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1} +%% \item $\alpha(x_2)=Fp_1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2} +%% \item $\alpha(x_1)\sappr Fp_2\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3} +%% \item $\alpha(x_2)\sappr Fp_2\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4} +%% \end{enumerate} +% For every $(x_1,x_2)$ we have +% \begin{enumerate} +% \item $\alpha(x_1)=Fp_1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}, +% \item $\alpha(x_2)\sappr Fp_2\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\ +%% \end{enumerate} +% and since $R$ is symmetric, we have +%% \begin{enumerate} +% \item $\alpha(x_2)=Fp_1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}, +% \item $\alpha(x_1)\sappr Fp_2\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3}, +% \end{enumerate} +% Now, we have two cases: +% \begin{itemize} +% \item Assuming $\alpha(x_1)\in X$ then by~\eqref{eq:maybe-func-set-1} we have $Fp_1\comp\sigma(x_1,x_2)\in X$, thus $\sigma(x_1,x_2)\in R$. So, we have $Fp_2\comp\sigma(x_1,x_2)\in X$ that by~\eqref{eq:maybe-func-set-4} means $\alpha(x_2)\in X$. +% \item Assuming $\alpha(x_1)=\bot$ then by~\eqref{eq:maybe-func-set-3} we have $Fp_2\comp\sigma(x_2,x_1)=\bot$, thus $\sigma(x_2,x_1)=\bot$. So, we have $Fp_1\comp\sigma(x_2,x_1)=\bot$ that by~\eqref{eq:maybe-func-set-2} means $\alpha(x_2)=\bot$ as well.\qed +% \end{itemize} +%\end{proof} +%%\begin{proof} +%% We assume that $\sigma\c R\to R+1$ is the witness that we have for $R$ to be an AM-simulation. We prove the statement by contradiction. If the statement is false, then we either have +%% \begin{gather*} +%% \alpha(x_1)\in X\quad\&\quad \alpha(x_2)=\bot, +%% \end{gather*} +%% or +%% \begin{gather*} +%% \alpha(x_1)=\bot\quad\&\quad \alpha(x_2)\in X. +%% \end{gather*} +%% Assuming $\alpha(x_1)\in X\;\&\; \alpha(x_2)=\bot$, then since $R$ is an AM-simulation, by~\eqref{eq:diag-lax-sim}$(p_2+1)\comp \sigma(x_1,x_2)\appr\alpha(x_2)$, we have $(p_2+1)\comp \sigma(x_1,x_2)=\bot$ that entails $\sigma(x_1,x_2)=\bot$. So, we have $(p_1+1)\comp \sigma(x_1,x_2)=\bot$, while $\alpha(x_1)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark +%% +%% Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)\in X$, since $R$ is symmetric, then we have $(x_2,x_1)\in R$ as well. So, by~\eqref{eq:diag-lax-sim} we have $(p_2+1)\comp \sigma(x_2,x_1)\appr\alpha(x_1)$ that entails $\sigma(x_2,x_1)=\bot$. So, we have $(p_1+1)\comp\sigma(x_2,x_1)=\bot$, while $\alpha(x_2)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark\qed +%%\end{proof} +% +%\begin{prop}\label{prop:sym-sim-bis-maybe} +% For a $F$-coalgebra $(X,\alpha)$ in $\Set$, such that $FX=X+1$, a symmetric AM-simulation relation $R$ on $X$ is an AM-bisimulation. +%\end{prop} +%\begin{proof} +% By~\autoref{lem:maybe-func-set} for every $(x_1,x_2)\in R$, we either have +% \begin{gather*} +% \alpha(x_1)=\bot\quad\&\quad \alpha(x_2)=\bot, % \end{gather*} % or % \begin{gather*} -% \alpha(x_1)=\bot\quad\&\quad \alpha(x_2)\in X. +% \alpha(x_1)\in X\quad\&\quad \alpha(x_2)\in X. % \end{gather*} -% Assuming $\alpha(x_1)\in X\;\&\; \alpha(x_2)=\bot$, then since $R$ is an AM-simulation, by~\eqref{eq:diag-lax-sim}$(p_2+1)\comp \sigma(x_1,x_2)\appr\alpha(x_2)$, we have $(p_2+1)\comp \sigma(x_1,x_2)=\bot$ that entails $\sigma(x_1,x_2)=\bot$. So, we have $(p_1+1)\comp \sigma(x_1,x_2)=\bot$, while $\alpha(x_1)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark -% -% Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)\in X$, since $R$ is symmetric, then we have $(x_2,x_1)\in R$ as well. So, by~\eqref{eq:diag-lax-sim} we have $(p_2+1)\comp \sigma(x_2,x_1)\appr\alpha(x_1)$ that entails $\sigma(x_2,x_1)=\bot$. So, we have $(p_1+1)\comp\sigma(x_2,x_1)=\bot$, while $\alpha(x_2)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark\qed +% We define $\beta$ as a witness for $R$ to be an AM-bisimulation as follows: +% \begin{gather*} +% \beta(x_1,x_2)= +% \begin{cases} +% \bot & \alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot \\ +% (\alpha(x_1),\alpha(x_2)) & \alpha(x_1)\in X\;\&\;\alpha(x_2)\in X +% \end{cases} +% \end{gather*} +% Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $Fp_i\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$. +% Now, we are left to prove that if $\alpha(x_1)\in X$ and $\alpha(x_2)\in X$ then $\beta(x_1,x_2)\in R$ that means that the codomain of $\beta$ is indeed $R+1$. We assume $\alpha(x_i)\in X$. Since $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$ we have $\beta(x_1,x_2)\in R$. +% \qed %\end{proof} -\begin{prop}\label{prop:sym-sim-bis-maybe} +\begin{prop}\label{prop:sym-sim-bis-may} For a $F$-coalgebra $(X,\alpha)$ in $\Set$, such that $FX=X+1$, a symmetric AM-simulation relation $R$ on $X$ is an AM-bisimulation. \end{prop} \begin{proof} - By~\autoref{lem:maybe-func-set} for every $(x_1,x_2)\in R$, we either have - \begin{gather*} - \alpha(x_1)=\bot\quad\&\quad \alpha(x_2)=\bot, - \end{gather*} - or - \begin{gather*} - \alpha(x_1)\in X\quad\&\quad \alpha(x_2)\in X. - \end{gather*} - We define $\beta$ as a witness for $R$ to be an AM-bisimulation as follows: - \begin{gather*} - \beta(x_1,x_2)= - \begin{cases} - \bot & \alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot \\ - (\alpha(x_1),\alpha(x_2)) & \alpha(x_1)\in X\;\&\;\alpha(x_2)\in X - \end{cases} - \end{gather*} - Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $Fp_i\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$. - Now, we are left to prove that if $\alpha(x_1)\in X$ and $\alpha(x_2)\in X$ then $\beta(x_1,x_2)\in R$ that means that the codomain of $\beta$ is indeed $R+1$. We assume $\alpha(x_i)\in X$. Since $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$ we have $\beta(x_1,x_2)\in R$. - \qed + We prove that $\sigma$ also is a witness for $R$ to be an AM-bisimulation. For every $(x_1,x_2)\in R$ we have + \begin{enumerate} + \item $\alpha(x_1)=p_1+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}, + \item $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\ + % \end{enumerate} + and since $R$ is symmetric, we have + % \begin{enumerate} + \item $\alpha(x_2)=p_1+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}, + \item $\alpha(x_1)\sappr p_2+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3}, + \end{enumerate} + Followed by $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$ we have the following cases: + \begin{itemize} + \item $\alpha(x_2)=p_2+1\comp\sigma(x_1,x_2)$: In this case, we already have $\sigma$ as a witness for $R$ to be a bisimulation. + \item $Fp_2\comp\sigma(x_1,x_2)=\bot$: In this case, we have + \begin{align*} + p_2+1\comp\sigma(x_1,x_2)=\bot,&\\ + \Rightarrow&\sigma(x_1,x_2)=\bot,\\ + \Rightarrow&p_1+1\comp\sigma(x_1,x_2)=\bot,\\ + \Rightarrow&\alpha(x_1)=\bot,&\eqref{eq:maybe-func-set-1}\\ + \Rightarrow&p_2+1\comp\sigma(x_2,x_1)=\bot,&\eqref{eq:maybe-func-set-3}\\ + \Rightarrow&\sigma(x_2,x_1)=\bot,\\ + \Rightarrow&p_1+1\comp\sigma(x_2,x_1)=\bot,\\ + \Rightarrow&\alpha(x_2)=\bot,&\eqref{eq:maybe-func-set-2}\\ + \Rightarrow&\alpha(x_2)=p_1+1\comp\sigma(x_1,x_2)\bot. + \end{align*} + \end{itemize}\qed \end{proof} Now, we want to abstract the given proof for an extensive category that has terminal objects (so that we have the maybe functor). We assume a natural order structure $\appr$ for the maybe functor. For every objects $X$ and $Y$, we define $\appr$ on each $\Hom(X,Y+1)$ by saying that for $f,g\in\Hom(X,Y+1)$ we have $f\appr g$ whenever either $f=g$ or $f=\bot$.\sgnote{This abstract order is coarser than (not the concretisation of) the pointwise Set order at \autoref{lem:set-ord-str}: here the \emph{whole} map must be $\bot$, whereas pointwise a map may be $\bot$ on some points and agree elsewhere. Please check the two agree on the hom-sets you actually use, or justify why the coarser order suffices.} @@ -3049,9 +3091,7 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat \begin{proof} \todo{Finish.} \end{proof} -\begin{lemma} - The non-trivial order on the maybe functor $FX=X+1$ is a liftable order. -\end{lemma} +\subsection{Symmetrization of a Barr relator} \begin{prop} Assuming $F$ is the maybe functor $FX=X+1$, then the syemmetrization of the left-lax Barr relator of $F$ is a Barr-relator. \end{prop} @@ -3073,6 +3113,7 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat \begin{remark} With a similar argument we can prove that the symmetrization of a right-lax Barr-relator of $F$ is a Barr-relator. \end{remark} +\todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion.} \end{document}