From a888ed095a07f4ef53978e7ddfcefac678767bd1 Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 17 Apr 2026 19:27:15 +0100 Subject: [PATCH] the abstract proof --- draft/draft.tex | 124 ++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 120 insertions(+), 4 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 82c605d..5260171 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -949,6 +949,59 @@ We can define $(-)^\dagger$ as a functor from $\gra(\BC)\to\rel(\BC)$, then we d \arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2] \end{tikzcd} \end{equation*} +\begin{lemma}\label{lem:norm-simp} + Assuming that we have the following commutative diagram: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \\ + FX \& FR \& FX + \arrow["\alpha"', from=1-1, to=2-1] + \arrow["{{p_1}}"', from=1-2, to=1-1] + \arrow["{{p_2}}", from=1-2, to=1-3] + \arrow["{{\sigma}}", from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["{Fp_1}", from=2-2, to=2-1] + \arrow["{Fp_2}"', from=2-2, to=2-3] + \end{tikzcd} + \end{equation*} + Then there exists $\sigma^\dagger\c R\to(FR)^\dagger$ in the following diagram that is also commutative: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \\ + FX \& {(FR)^\dagger} \& FX + \arrow["\alpha"', from=1-1, to=2-1] + \arrow["{{p_1}}"', from=1-2, to=1-1] + \arrow["{{p_2}}", from=1-2, to=1-3] + \arrow["{{\sigma^\dagger}}", from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["{Fp_1^\dagger}", from=2-2, to=2-1] + \arrow["{Fp_2^\dagger}"', from=2-2, to=2-3] + \end{tikzcd} + \end{equation*} +\end{lemma} +\begin{proof} + The proof is trivial considering that $\sigma^\dagger=e_{FR}\comp\sigma$, where $e_{FR}$ is the epimorphism in the epi-mono factorization of $\brks{Fp_1,Fp_2}$, as depicted in the following diagram: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \\ + FX \& FR \& FX \\ + FX \& {(FR)^\dagger} \& FX + \arrow["\alpha"', from=1-1, to=2-1] + \arrow["{{p_1}}"', from=1-2, to=1-1] + \arrow["{{p_2}}", from=1-2, to=1-3] + \arrow["{{\sigma}}", from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["\id"', from=2-1, to=3-1] + \arrow["{Fp_1}", from=2-2, to=2-1] + \arrow["{Fp_2}"', from=2-2, to=2-3] + \arrow["{e_{FR}}", from=2-2, to=3-2] + \arrow["\id", from=2-3, to=3-3] + \arrow["{Fp_1^\dagger}", from=3-2, to=3-1] + \arrow["{Fp_2^\dagger}"', from=3-2, to=3-3] + \end{tikzcd} + \end{equation*} + \qed +\end{proof} We show this relation with $F_\rel(R,X)$. \begin{definition}[Simulation]\label{def:sim} A coalgebra $\sigma\c R\to (FR)^\dagger$ is a simulation over the $F$-coalgebra $\alpha\c X\to FX$ iff the following diagram is lax-commutative: @@ -1757,8 +1810,8 @@ At the moment we have limited the discussion to the category of sets and we are \arrow["{p_2}", from=1-2, to=1-3] \arrow["\sigma", dashed, from=1-2, to=2-2] \arrow["\alpha", from=1-3, to=2-3] - \arrow["{{\mathcal{P}p_1^\dagger}_\subseteq}", from=2-2, to=2-1] - \arrow["{{\mathcal{P}p_2^\dagger}_\subseteq}"', from=2-2, to=2-3] + \arrow["{{\mathcal{P}p_1}_\subseteq}", from=2-2, to=2-1] + \arrow["{{\mathcal{P}p_2}_\subseteq}"', from=2-2, to=2-3] \end{tikzcd} \end{equation*} It is defined as $\sigma(x_1,x_2)=(\alpha(x_1),\alpha(x_2))$. @@ -1792,8 +1845,8 @@ Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\d \arrow["id"', from=2-1, to=3-1] \arrow["\delta", from=2-2, to=3-2] \arrow["id"', from=2-3, to=3-3] - \arrow["{{\mathcal{P}p_1^\dagger}_\subseteq}", from=3-2, to=3-1] - \arrow["{{\mathcal{P}p_2^\dagger}_\subseteq}"', from=3-2, to=3-3] + \arrow["{{\mathcal{P}p_1}_\subseteq}", from=3-2, to=3-1] + \arrow["{{\mathcal{P}p_2}_\subseteq}"', from=3-2, to=3-3] \end{tikzcd} \end{equation*} $\delta$ is defined as the following: @@ -1804,6 +1857,69 @@ $\delta$ is defined as the following: w & \mathsf{o.w} \end{cases} \end{gather*} +Now, we want to prove an abstraction of this statement. First, we need to spell out what $\appr;(FR)^\dagger;\appr$ is. We define relation compositions with pullbacks, so we have the following diagram: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + {\appr;(FR)^\dagger;\appr} \& {\appr;(FR)^\dagger} \& {\appr} \& {FX} \\ + \& (FR)^\dagger \& {FX} \\ + {\appr} \& {FX} \\ + {FX} + \arrow["{{{{{{{\pi_1}}}}}}}", from=1-1, to=1-2] + \arrow["{{{{{{{\pi_2}}}}}}}"', from=1-1, to=3-1] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-2] + \arrow["{{{{{{{\varphi_1}}}}}}}", from=1-2, to=1-3] + \arrow["{{{{{{{\varphi_2}}}}}}}", from=1-2, to=2-2] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] + \arrow["{{{{{{{i_1}}}}}}}", from=1-3, to=1-4] + \arrow["{{{{{{{i_2}}}}}}}", from=1-3, to=2-3] + \arrow["{{{{{{{Fp_1^\dagger}}}}}}}", from=2-2, to=2-3] + \arrow["{{{{{{{Fp_2^\dagger}}}}}}}"', from=2-2, to=3-2] + \arrow["{{{{{{{i_1}}}}}}}"', from=3-1, to=3-2] + \arrow["{{{{{{{i_2}}}}}}}"', from=3-1, to=4-1] + \end{tikzcd} +\end{equation*} +Additionally, we make the abbreviations that ${Fp_1}_\appr=i_1\comp\varphi_1\comp\pi_1$ and ${Fp_2}_\appr=i_2\comp\pi_2$. +\begin{prop} + Assuming we have a morphism $\sigma'\c R\to(FR)^\dagger$ then exists $\delta\c(FR)^\dagger\to(\appr;(FR)^\dagger;\appr)^\dagger$ such that $\sigma=\delta\comp\sigma'$ that commutes in the following diagram: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \\ + {FX} \& {(FR)^\dagger} \& {FX} \\ + {FX} \& {(\appr;(FR)^\dagger;\appr)^\dagger} \& {FX} + \arrow["\alpha"', from=1-1, to=2-1] + \arrow["{p_1}"', from=1-2, to=1-1] + \arrow["{p_2}", from=1-2, to=1-3] + \arrow["{\sigma'}", from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["id"', from=2-1, to=3-1] + \arrow["\delta", from=2-2, to=3-2] + \arrow["id"', from=2-3, to=3-3] + \arrow["{({Fp_1}_\appr)^\dagger}", from=3-2, to=3-1] + \arrow["{({Fp_2}_\appr)^\dagger}"', from=3-2, to=3-3] + \end{tikzcd} + \end{equation*} +\end{prop} +\begin{proof} + Ultimately, we need to define $\delta'\c(FR)\to\appr;(FR)^\dagger;\appr$, where $\delta=e_{\appr;(FR)^\dagger;\appr}\comp\delta'$, and $e_{\appr;(FR)^\dagger;\appr}\c\appr;(FR)^\dagger;\appr\to(\appr;(FR)^\dagger;\appr)^\dagger$ is the epimorphism in the epi-mono factorization of $\brks{{Fp_1}_\appr,{Fp_2}_\appr}$ because by~\autoref{lem:norm-simp} it suffices to show that the following diagram commutes: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \\ + FX \& {(FR)^\dagger} \& FX \\ + FX \& {\appr;(FR)^\dagger;\appr} \& FX + \arrow["\alpha"', from=1-1, to=2-1] + \arrow["{{p_1}}"', from=1-2, to=1-1] + \arrow["{{p_2}}", from=1-2, to=1-3] + \arrow["{{\sigma'}}", from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["id"', from=2-1, to=3-1] + \arrow["{\delta'}", from=2-2, to=3-2] + \arrow["id"', from=2-3, to=3-3] + \arrow["{{{Fp_1}_\appr}}", from=3-2, to=3-1] + \arrow["{{{Fp_2}_\appr}}"', from=3-2, to=3-3] + \end{tikzcd} + \end{equation*} + So, we need to define $\delta'$. +\end{proof} \end{document}