Когда у пространств когерентности есть откаты и отжимания?

$\newcommand{\symp}{\Bumpeq}$

$\symp_X$$X$$(X, \symp_X)$$f : X \to Y$$f \subseteq X \times Y$$(x,y) \in f$$(x',y') \in f$

1. если то и$x \symp_X x'$$y \symp_Y y'$
2. если и то .$x \symp_X x'$$y = y'$$x = x'$

Категория пространств когерентности является как декартовой, так и моноидально замкнутой. Я хотел бы знать, когда существуют откаты или откаты для этой категории, и когда существует какой-либо моноидальный аналог откатов или откатов (и как его определить, если это понятие имеет смысл).

Теперь я вижу, как определить эквалайзеры для пространств когерентности, что означает, что откаты всегда существуют (так как продукты делают). Я не знаю, как это сделать, на самом деле ....

Напомним, что композиция - это обычная реляционная композиция, поэтому если и , то:$f : A \to B$$g : B \to C$

$f ; g = \{(a,c) \in A \times C \;|\; \exists b \in B.\; (a,b) \in f \land (b,c) \in g\}$

(В этом определении экзистенциал фактически подразумевает уникальное существование. Предположим, что у нас есть такое, что и . Поскольку мы знаем, что , это означает, что . Тогда это означает, что у нас есть и и , поэтому .)$b' \in B$$(a,b') \in f$$(b', c) \in g$$a \Bumpeq_A a$$b \Bumpeq_B b'$$b \Bumpeq_B b'$$(b,c) \in g$$(b',c) \in g$$b = b'$

Теперь мы строим эквалайзеры. Предположим , что мы имеем когерентные пространства и , и морфизмов . Теперь определите эквалайзер следующим образом.$A$$B$$f, g : A \to B$$(E, e : E \to A)$

1. Для сети возьмите Это выбирает подмножество лексем из , на которых либо и согласны (до согласования - я имел это неправильно в моей первой версии ) или оба не определены.

   $$E = \left\{ \begin{array}{l|c} & \forall b.\; (a,b) \in f \implies \exists a' \Bumpeq_A a.\; (a',b) \in g \\ a \in A & \land \\ & \forall b.\; (a,b) \in g \implies \exists a' \Bumpeq_A a.\; (a',b) \in f \\ \end{array} \right\}$$ $A$$f$$g$

2. Определите отношение когерентности для . Это просто ограничение когерентности отношения на к подмножеству . Это будет рефлексивным и симметричным, поскольку есть.$\Bumpeq_E = \{ (a,a') \in \Bumpeq_A \;|\; a \in E \land a' \in E\}$$A$$E$$\Bumpeq_A$

3. Отображение эквалайзера - это просто диагональ .$e$$e : E \to A = \{(a, a)\;|\;a \in E\}$

Так как я испортил свою первую версию доказательства, я предоставлю свойство универсальности явно. Предположим, что у нас есть любой другой объект и морфизм такой, что .$X$$m : X \to A$$m;f = m;g$

Теперь определим как . Очевидно, что , но чтобы показать равенство, нам нужно показать обратное .$h : X \to E$$\{(x,a) \;|\; a \in E\}$$h;i \subseteq m$$m \subseteq h;i$

Итак, предположим . Теперь нам нужно показать, что и .$(x,a) \in m$$\forall b.\; (a,b) \in f \implies \exists a' \Bumpeq_A a.\; (a',b) \in g$$\forall b.\; (a,b) \in g \implies \exists a' \Bumpeq_A a.\; (a',b) \in f$

Сначала предположим, что и . Итак, мы знаем, что и , поэтому . Следовательно, , и поэтому существует такое, что и . Поскольку , мы знаем , и поэтому существует такой, что .$b \in B$$(a,b) \in f$$(x,a) \in m$$(a,b) \in f$$(x,b) \in m;f$$(x,b) \in m;g$$a' \in A$$(x,a') \in m$$(a',b) \in g$$x \Bumpeq x$$a \Bumpeq a'$$a' \Bumpeq a$$(a',b) \in g$

Симметрично предположим, что и . Итак, мы знаем, что и , поэтому . Следовательно, , и поэтому существует такое, что и . Поскольку , мы знаем , и поэтому существует такой, что .$b \in B$$(a,b) \in g$$(x,a) \in m$$(a,b) \in g$$(x,b) \in m;g$$(x,b) \in m;f$$a' \in A$$(x,a') \in m$$(a',b) \in f$$x \Bumpeq x$$a \Bumpeq a'$$a' \Bumpeq a$$(a',b) \in f$