pouya/coalgebraic-simulation
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

minor

Browse Source
This commit is contained in:
partowp
2026-08-03 20:29:50 +01:00
parent 99d6862e12
commit 51b64cc427
1 changed files with 9 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+9 -9
View File
@@ -577,24 +577,24 @@ The definition derives the ordering on morphisms of each hom-set $\Hom(X,\sub Y)
\end{cases}
\end{gather*}
First, we need to prove that $\mu'$ is a subdistribution.
For every $x \in X$, $\mu'(x) \ge 0$. The total mass of $\mu'$ is
For every $x \in X$, $\mu'(x) \ge 0$. We have:
\begin{align*}
\sum_{x \in X} \mu'(x)&\\
=& \sum_{x \in X} \frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)\\
=& \sum_{y \in Y} \sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)\\
=& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)\\
=& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)\\
=& \sum_{x \in X} \frac{\nu(g(x))}{Sg(\mu)(g(x))} \comp \mu(x)&(Sg(\mu)(g(x))\neq 0)\\
=& \sum_{y \in Y} \sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)&(Sg(\mu)(g(x))\neq 0)\\
=& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)&(Sg(\mu)(g(x))\neq 0)\\
=& \sum_{y \in Y} \frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)&(Sg(\mu)(g(x))\neq 0)\\
=& \sum_{y \in Y} \nu(y)\\
\leq& 1
\end{align*}
Thus $\mu'$ is a subdistribution. Now, we prove $Sg(\mu') = \nu$.
As for every $x\in X$ that $Sg(\mu)(g(x))=0$, $\mu'(x)=0$, it does not have effect the inequality. Thus $\mu'$ is a subdistribution. Now, we prove $Sg(\mu') = \nu$.
For any $y \in Y$, we have:
\begin{align*}
Sg(\mu')(y)&\\
= &\sum_{x \in g^{\mone}(y)} \mu'(x)\\
= &\sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)\;\;(Sg(\mu)(y)\neq 0)\\
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)\;\;(Sg(\mu)(y)\neq 0)\\
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)\;\;(Sg(\mu)(y)\neq 0)\\
= &\sum_{x \in g^{\mone}(y)} \frac{\nu(y)}{Sg(\mu)(y)} \comp \mu(x)&(Sg(\mu)(y)\neq 0)\\
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp \sum_{x \in g^{\mone}(y)} \mu(x)&(Sg(\mu)(y)\neq 0)\\
= &\frac{\nu(y)}{Sg(\mu)(y)} \comp Sg(\mu)(y)&(Sg(\mu)(y)\neq 0)\\
= &\mu(y)
\end{align*}
(If $Sg(\mu)(y) = 0$, then $\nu(y) = 0$, and the sum is $0$ as well, so the equality still holds.) \\