From 6847f3ec7b013da1a971fa9351928eab4cc573bb Mon Sep 17 00:00:00 2001 From: partowp Date: Thu, 13 Aug 2026 17:07:02 +0100 Subject: [PATCH] bluh --- draft/draft.tex | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/draft/draft.tex b/draft/draft.tex index 8d931b7..373e08b 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -476,6 +476,16 @@ We want to say that a natural order structure entails an order over a functor de $\appr$ being a liftable order structure on $F$ means that for morphisms $g\c Y\to Z$, $k\in\Hom(X,FY)$, and $h\in\Hom(X,FZ)$ that $g$ is epic, if $h\appr Fg\comp k$ then exists $k'\in\Hom(X,FY)$, such that $k\appr k'$ and $h=Fg\comp k'$. %Now, assuming $\alpha\c Y\to Z$, $\mu\in\Hom(X,FGY)$, and $\nu\in\Hom(X,FGZ)$ that $\alpha$ is epic, we need to prove that exists some $\mu'\in\Hom(X,FGY)$ such that $\mu'\appr\mu$ and $\nu=FG\alpha\comp\mu'$. Since $G$ preserves epimorphisms and $\alpha$ is epic, then $G\alpha$ is also epic. Furthermore, since $\appr$ is a liftable order structure on $F$, then the mentioned $\mu'$ exists.\qed Now, assuming $\alpha\c Y\to Z$, $\mu\in\Hom(X,FGY)$, and $\nu\in\Hom(X,FGZ)$ that $\alpha$ is epic. Since $G$ is assumed to preserve epimorphisms, $G\alpha$ is epic. Since $\appr$ is a liftable order structure on $F$, then there exists some $\mu'\in\Hom(X,FGY)$ such that $\mu'\appr\mu$ and $\nu=FG\alpha\comp\mu'$. So, $\appr$ is a liftable order structure for $FG$ as well.\qed \end{proof} +\begin{rem} + For every regular category $\BC$ with the axiom of choice, every functor $G\c\BC\to\BC$ preserves epimorphisms. Assuming $e\c X\to Y$ is epic, then it has a section $s\c Y\to X$. Applying $G$ on both of them we have $Ge\c GX\to GY$ and $Gs\c GY\to GX$ that + \begin{align*} + Ge\comp Gs&\\ + =&G(e\comp s)\\ + =&G(\id_Y)\\ + =&\id_{GY} + \end{align*} + that means that $Gs$ is a section for $Ge$ that entails that $Ge$ is epic. +\end{rem} \todo{It seems too much, but perhaps you can study if you can derive an order structure from $F$ to $G$ and consequently $GF$, by the following rule: \begin{gather*} \infer{Gh\appr GFg\comp Gk}{h\appr Fg\comp k} @@ -3672,6 +3682,14 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat \todo{Write it down. You have it in your notes.} \end{proof} \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. See if~\autoref{prop:lax-relator-full-comm} or~\autoref{lem:lax-relator-str} can help!} +% +%\begin{prop} +% For every functor $F\c\Set\to\Set$, assuming $\relar$ is the left-lax Barr relator for $F$, then for every relation $r\subseteq X\times Y$, we have $\hat{\relar}r\subseteq \bar{F}r$. +%\end{prop} +%\begin{proof} +% +%\end{proof} +% \subsection{Symmetric relation} \begin{prop} Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a coalgebra $(X,\alpha)$, then $r$ is an $\hat{\relar}$-bisimulation. @@ -3687,6 +3705,9 @@ Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a \end{align*} Now, assuming $x\mathrel{r}y$ gives us $x\mathrel{(\alpha^\op\comp\relar r\comp \alpha)} y$ that is equivalent with saying that exist $x'$ and $y'$ such that $x\mathrel{\alpha}x'$, $y\mathrel{\alpha}y'$, and $x'\mathrel{\relar r}y'$. Since $r$ is symmetric, we have $y\mathrel{r} x$ that means that exist $x''$ and $y''$ such that $x\mathrel{\alpha}x''$, $y\mathrel{\alpha}y''$, and $y''\mathrel{\relar r}x''$. On the other hand since $\alpha$ is a function, we have $x''=x'$ and $y''=y'$, so we have $y'\mathrel{\relar r}x'$ that ultimately gives $x\mathrel{(\alpha^\op\comp\hat{\relar}r\comp\alpha)}y$. So, $r$ is an $\hat{\relar}$-bisimulation as well.\qed \end{proof} +\begin{cor} + For a functor $F\c\Set\to\Set$, assuming that for a relation $r$ we have $\appr\comp\bar{F}r\leq\bar{F}r$, if $r$ is symmetric, and it is a $\appr\comp\bar{F}$-simulation, then it is a $\hat{\appr\comp\bar{F}}$-bisimulation.\ppnote{This is a bad notation for lax Barr-relators. Switch them with $F^\rightarrow$, $F^\leftarrow$, and $F^\leftrightarrow$.} +\end{cor} \end{document}