This commit is contained in:
partowp 2026-05-06 17:43:16 +01:00
parent c62bf13250
commit 88a05b3653

View File

@ -2228,11 +2228,11 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
&\iff s\;F\pi_2\comp\sappr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\sappr\comp(F\pi_2)^\op)^\op\;t\\
&\iff s\;F\pi_2\comp\sappr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t
\end{align*}
Since $F\pi_1$ is a function, then $(F\pi_1)^\op$ is an injective map, so there exist exactly one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and:
Since $F\pi_1$ is a surjective function, then exists at least one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and:
\begin{gather*}
w\;F\pi_2\comp\sappr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t
\end{gather*}
And similarly, since $F\pi_2$ is also a function we have exactly one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and:
And similarly, since $F\pi_2$ is also a surjective function we have at least one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and:
\begin{align*}
&w\;\sappr\; v \qquad\&\qquad w\;\appr\; v\\
\iff&(F\pi_1)^\op(s)\;\sappr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\