Quand les espaces de cohérence ont-ils des retraits et des poussées?

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

Une relation de cohérence sur un ensemble est une relation réflexive et symétrique. Un espace de cohérence est une paire , et un morphisme entre les espaces de cohérence est une relation telle que pour tout et , $\symp_X$ $X$ $(X, \symp_X)$ $f : X \to Y$ $f \subseteq X \times Y$ $(x,y) \in f$ $(x',y') \in f$

si $x \symp_X x'$ alors $y \symp_Y y'$ , et
si $x \symp_X x'$ et $y = y'$ alors $x = x'$ .

La catégorie des espaces de cohérence est à la fois cartésienne et monoïdale fermée. Je voudrais savoir quand des retraits ou des poussées existent pour cette catégorie, et quand il existe un analogue monoïde de retraits ou de poussées (et comment le définir, au cas où cette notion aurait du sens).

pl.programming-languages ct.category-theory domain-theory linear-logic Neel Krishnaswami
la source

D'où vient cette définition? Celui de Girard, Lafont & Taylor est très différent.

Charles Stewart

Les deux définitions sont équivalentes. Je prends juste le Web comme primitif, à partir duquel l'ensemble des cliques peut être dérivé.

Neel Krishnaswami

Je trouve le choix de définition de Neel beaucoup plus compréhensible que l'original.

Dave Clarke

Je vais poser la question évidente: savez-vous qu'ils n'existent pas toujours? En d'autres termes, connaissez-vous des exemples de foncteurs dans des relations de cohérence qui n'ont pas de limite / colimite?

Ohad Kammar

Les deux définitions sont équivalentes - D'accord, mais avez-vous inventé cette définition, ou l'avez-vous obtenue de quelqu'un d'autre? Grande question, btw, je suis surpris que personne ne semble savoir si les égaliseurs existent toujours.

Charles Stewart

~~Je vois maintenant comment définir des égaliseurs pour les espaces de cohérence, ce qui signifie que les retraits existent toujours (puisque les produits existent).~~ Je ne sais pas comment faire ça, en fait ...

Rappelons que la composition est la composition relationnelle habituelle, donc si et , alors: $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\}$

(Dans cette définition, l'existentiel implique en fait une existence unique . Supposons que nous ayons tel que et . Puisque nous savons que , cela signifie que . Alors cela signifie que nous avons et et , donc par conséquent .) $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'$

Nous construisons maintenant des égaliseurs. Supposons que nous ayons espaces de cohérence et , et morphisms . Définissez maintenant l'égaliseur comme suit. $A$ $B$ $f, g : A \to B$ $(E, e : E \to A)$

Pour le Web, prenez Ceci sélectionne le sous-ensemble de jetons de sur lequel soit et sont d'accord (jusqu'à la cohérence - je me suis trompé dans ma première version ), ou ne sont pas tous deux définis.
$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$
Définissez la relation de cohérence sur . Ceci est juste à la limitation de la relation de cohérence sur au sous - ensemble . Ce sera réflexif et symétrique puisque est. $\Bumpeq_E = \{ (a,a') \in \Bumpeq_A \;|\; a \in E \land a' \in E\}$ $A$ $E$ $\Bumpeq_A$
La carte d'égalisation n'est que la diagonale . $e$ $e : E \to A = \{(a, a)\;|\;a \in E\}$

Depuis que j'ai foiré ma première version de la preuve, je donnerai explicitement la propriété d'universalité. Supposons que nous ayons tout autre objet et morphisme tels que . $X$ $m : X \to A$ $m;f = m;g$

Définissez maintenant comme . Évidemment , mais pour montrer l'égalité, nous devons montrer l'inverse . $h : X \to E$ $\{(x,a) \;|\; a \in E\}$ $h;i \subseteq m$ $m \subseteq h;i$

Supposons donc . Nous devons maintenant montrer que et . $(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$

Supposons d'abord et . Nous savons donc que et , donc . Donc , et donc il y a tel que et . Depuis , nous connaissons , et donc il y a tel que . $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$

Symétriquement, supposons et . Nous savons donc que et , donc . Donc , et donc il y a tel que et . Depuis , nous connaissons , et donc il y a tel que . $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
la source

Je ne vois pas comment vous pouvez prouver universelle. Il n'y a qu'une seule façon de factoriser n'importe quel , et c'est en définissant comme . Évidemment , mais je ne vois pas pourquoi l'inverse est : prenez un peu , et un , avec . Alors nous avons , donc du choix de nous avons . D'après la définition de la composition, il en existe tel que et . On peut en déduire qu'un

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'$ , mais nous ne connaissons que et , donc nous ne pouvons pas vraiment déduire que et terminer.

a f b

$afb$

a^{'} g b

$a'gb$

a = a^{'}

$a=a'$

Ohad Kammar

Oui, vous avez raison - le sous-ensemble choisi par l'égaliseur doit être à la cohérence, pas à l'égalité. J'ai changé la définition pour refléter cela, et étant donné la preuve que le diagramme commute explicitement.

Neel Krishnaswami

Ah ... Mais maintenant, n'égale pas le diagramme. En effet, supposons . Puis, par « s définition, nous avons , par conséquent , il existe un certain telle que . Mais nous n'avons pas , donc nous ne pouvons pas montrer que . Vous semblez rencontrer les mêmes problèmes que j'ai rencontrés la nuit dernière, d'où ma question évidente ci-dessus. Mais vous réussirez peut-être là où j'ai échoué! Ma prochaine étape était de prendre un plus sophistiqué , disons quelque chose comme , mais n'est pas un morphisme valide, donc un choix plus prudent est requis.

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

Je me souviens maintenant pourquoi j'espérais que la réponse se trouvait déjà dans la thèse de quelqu'un. :) Quoi qu'il en soit, j'y penserai davantage - il peut y avoir une astuce possible via le fait que les images inverses sont incohérentes par paire.

Neel Krishnaswami

Quand les espaces de cohérence ont-ils des retraits et des poussées?

Réponses: