From 81da58d639ccc49a3a7bc1612b60aa1b4e749dfc Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 17 Jul 2026 15:56:49 +0100 Subject: [PATCH] order --- draft/draft.tex | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/draft/draft.tex b/draft/draft.tex index b82273e..003d259 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2319,8 +2319,18 @@ So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alph \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.} +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.} %Although even in the context that we are at the moment, it does not seem plausible to prove that a symmetric simulation is a bisimulation without having an operator like $\join$ in~\autoref{prop:sym-sim-bis-maybe} that takes two morphisms of the same type and gives one. +Assuming $f,g\in\Hom(X,Y+1)$, and that $f'\c X_f\rightarrowtail X$ and $g'\c X_g\rightarrowtail X$, and $X_f$ and $X_g$ are pullbacks of $f$ and $\inl$, and $g$ and $\inl$ accordingly, then $f\appr g$ if there exists $h\c X_f\rightarrowtail X_g$ that commutes in the following diagram: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + {X_g} \& X \\ + {X_f} + \arrow["{g'}", tail, from=1-1, to=1-2] + \arrow["h", dashed, tail, from=2-1, to=1-1] + \arrow["{f'}"', tail, from=2-1, to=1-2] + \end{tikzcd} +\end{equation*} \begin{lemma}\label{lem:maybe-lif-abs} The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order. \end{lemma}