Kiedy przestrzenie spójności mają wycofania i wypychania?

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

Relacja koherencji $\symp_X$ na zbiorze $X$ jest relacją i symetryczną. Przestrzeń koherencji to para $(X, \symp_X)$ , a morfizm $f : X \to Y$ między przestrzeniami koherencji jest relacją $f \subseteq X \times Y$ taką, że dla wszystkich $(x,y) \in f$ i $(x',y') \in f$ ,

jeśli $x \symp_X x'$ to $y \symp_Y y'$ , i
jeśli $x \symp_X x'$ i $y = y'$ to $x = x'$ .

Kategoria przestrzeni koherencji jest zarówno kartezjańska, jak i monoidalna zamknięta. Chciałbym wiedzieć, kiedy dla tej kategorii istnieją wycofania lub wypychania i kiedy istnieje jakiś monoidalny analog wycofań lub wypychań (i jak to zdefiniować, na wypadek, gdyby to pojęcie miało sens).

— Neel Krishnaswami
źródło

Skąd ta definicja? Ten w Girard, Lafont i Taylor wygląda zupełnie inaczej.

— Charles Stewart,

Dwie definicje są równoważne. Po prostu biorę sieć za prymitywną, z której można uzyskać zestaw klików.

— Neel Krishnaswami,

Uważam, że wybór definicji Neela jest znacznie bardziej zrozumiały niż oryginał.

— Dave Clarke

Zadam oczywiste pytanie: czy wiesz, że nie zawsze istnieją? Innymi słowy, czy znasz jakieś przykłady funktora w relacjach koherencji, który nie ma limitu / limitu?

— Ohad Kammar 21.01.11

Dwie definicje są równoważne - prawda, ale czy wymyśliłeś tę definicję, czy otrzymałeś ją od kogoś innego? Świetne pytanie, przy okazji, jestem zaskoczony, że nikt nie wie, czy korektory zawsze istnieją.

— Charles Stewart

~~Widzę teraz, jak zdefiniować korektory dla przestrzeni koherencji, co oznacza, że zawsze istnieją niedociągnięcia (ponieważ produkty mają).~~ Właściwie to nie wiem jak to zrobić ...

Przypomnijmy, że kompozycja ma zwykle skład relacyjny więc jeśli i , a następnie: $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\}$

(W tej definicji egzystencjalność w rzeczywistości implikuje wyjątkowe istnienie. Załóżmy, że mamy tak że i . Ponieważ wiemy, że , oznacza to, że . To oznacza, że mamy i oraz , a zatem konsekwentnie .) $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'$

Teraz konstruujemy korektory. Załóżmy, że mamy przestrzenie spójność i oraz morfizmów . Teraz zdefiniuj korektor w następujący sposób. $A$ $B$ $f, g : A \to B$ $(E, e : E \to A)$

W przypadku sieci weź Wyodrębnia to podzbiór tokenów na który zgadzają się albo i (do spójności - pomyliłem się w mojej pierwszej wersji ) lub oba są niezdefiniowane.
$E = {\begin{array}{lc} \forall b . (a, b) \in f ⟹ \exists a^{'} ≎_{A} a . (a^{'}, b) \in g \\ a \in A & \land \\ \forall b . (a, b) \in g ⟹ \exists a^{'} ≎_{A} a . (a^{'}, b) \in f \end{array}}$ $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$
Zdefiniuj relację koherencji na . To jest po prostu ograniczenie relacji koherencji na do podzbioru . Będzie to zwrotne i symetryczne, ponieważ jest. $\Bumpeq_E = \{ (a,a') \in \Bumpeq_A \;|\; a \in E \land a' \in E\}$ $A$ $E$ $\Bumpeq_A$
Mapa korektora to tylko przekątna . $e$ $e : E \to A = \{(a, a)\;|\;a \in E\}$

Ponieważ pomieszałem moją pierwszą wersję dowodu, podam jawnie właściwość uniwersalności. Załóżmy, że mamy jakikolwiek inny obiekt i morfizm taki, że . $X$ $m : X \to A$ $m;f = m;g$

Teraz zdefiniuj jako . Oczywiście , ale aby pokazać równość, musimy pokazać odwrotność . $h : X \to E$ $\{(x,a) \;|\; a \in E\}$ $h;i \subseteq m$ $m \subseteq h;i$

Załóżmy więc . Musimy teraz pokazać, że oraz . $(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$

Najpierw załóżmy i . Wiemy, że i , SO . Dlatego , a więc nie jest tak że i . Ponieważ , wiemy'a więc nie jest takie, że . $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$

Symetrycznie załóżmy i . Wiemy więc, że oraz , więc . Dlatego , a więc istnieje takie jak oraz . Ponieważ , wiemy , a więc istnieje taki, że . $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$

— Neel Krishnaswami
źródło

Nie widzę, w jaki sposób można udowodnić, uniwersalne. Istnieje tylko jeden sposób na uwzględnienie dowolnego , a to poprzez ustawienie jako . Oczywiście , ale nie rozumiem, dlaczego zachodzi odwrotność: weź trochę i trochę , z . Mamy więc , stąd z wyboru mamy . Z definicji kompozycji istnieje pewne takie jak i . Możemy wywnioskować, że

e

$e$

m : X \to A

$m : X \rightarrow A$

h : X \to E

$h : X \rightarrow E$

h := {(x, a) : (x, a) \in m, a \in E}

$h := \{(x, a) : (x,a) \in m, a \in E\}$

h; e \subset m

$h;e \subset m$

x m a

$xma$

b \in B

$b \in B$

a f b

$afb$

x (m; f) b

$x(m;f)b$

m

$m$

x (m; g) b

$x(m;g)b$

a^{'}

$a'$

x m a^{'}

$xma'$

a^{'} g b

$a'gb$

a \symp a^{'}

$a \symp a'$ , ale wiemy tylko, że i , więc nie możemy naprawdę wydedukować, że i zakończyć.

a f b

$afb$

a^{'} g b

$a'gb$

a = a^{'}

$a=a'$

— Ohad Kammar

Tak, masz rację - podzbiór wybierany przez korektor musi być spójny, a nie równy. Zmieniłem definicję, aby to odzwierciedlić, i podając dowód, że diagram dojeżdża do pracy.

— Neel Krishnaswami

Ach ... Ale teraz nie wyrównuje schematu. Rzeczywiście, załóżmy . Następnie przez 's definicji mamy , stąd istnieje kilka takie, że . Ale nie mamy tego , więc nie możemy pokazać, że . Wygląda na to, że napotykasz te same problemy, na które wpadłem zeszłej nocy, stąd moje oczywiste pytanie powyżej. Ale może odniesiesz sukces tam, gdzie mi się nie udało! Moim następnym krokiem było przyjęcie bardziej wyrafinowanego , powiedzenie czegoś w rodzaju , ale wtedy nie jest prawidłowym morfizmem, więc wymagany jest bardziej ostrożny wybór.

e

$e$

a (e; f) b

$a(e;f)b$

e

$e$

a f b

$afb$

a^{'} \symp a

$a'\symp a$

a^{'} g b

$a'gb$

a e a^{'}

$aea'$

a (e; g) b

$a(e;g)b$

e

$e$

a e a^{'} ⟺ a \symp a^{'}

$aea' \iff a\symp a'$

e

$e$

— Ohad Kammar 21.01.11

Teraz pamiętam, dlaczego miałem nadzieję, że odpowiedź była już w czyjejś tezie. :) W każdym razie pomyślę o tym więcej - może istnieć pewna sztuczka polegająca na tym, że odwrotne obrazy są niespójne parami.

— Neel Krishnaswami