Cours 7: Espace cohérents

Espaces cohérents

Ex:

Bool := 0   1

Produit d’espaces cohérents

Le produit $A_1 \& A_2$ de deux esp. coh. est défini de la façon suivante:

  • \[\vert A_1 \& A_2\vert = \underbrace{\vert A_1 \vert + \vert A_1 \vert}_{\text{union disjointe}} = \lbrace 1 \rbrace × \vert A \vert ∪ \lbrace 2 \rbrace × \vert A_2 \vert\]
  • \[(i, c) \sim_{A_1 \& A_2} (i', c') ⟺ (i ≠ i') \text{ ou } (i=i' \text{ et } c \sim_{A_i} c')\]

Ex: $Bool \& Bool$

  graph {
    rankdir=LR;
    0 -- "0'", "1'";
    1 -- "0'", "1'";
  }

$f: A ⟶ B$

\[x∈ Cl(A) ⟹ f(x) = \bigcup_{d ⊆_{fin} x} \lbrace b \mid (d, b) ∈ tr(f) \rbrace\] \[tr(f) = \lbrace (d, b) ∈ Cl_{fin}(A) × \vert B \vert \mid b ∈ f(d)\rbrace\]

Ex:

\[\text{parallel or} ≝ por: Bool \& Bool ⟶ Bool\] \[tr(por) = \lbrace (\lbrace 0, 0' \rbrace, 0), \underbrace{(\lbrace 1 \rbrace, 1), (\lbrace 1' \rbrace, 1)}_{\text{spécifique au "ou prallèle"}}, (\lbrace 1, 1' \rbrace, 1), (\lbrace 1, 0' \rbrace, 1), (\lbrace 0, 1' \rbrace, 1) \rbrace\]

NB: \(por(\lbrace 0 \rbrace) = \lbrace b \mid (∅, b) ∈ tr(por) \text{ ou } (\lbrace 0 \rbrace, b) ∈ tr(por) \rbrace = ∅\)

Stabilité

Notion de stabilité ⟶ pas une notion topologique, mais une notion relative à l’ordre. C’est pour cela qu’on a abandonné la topologie au cours précédent… :-(

Une fonction continue $f: A ⟶ B$ entre espaces cohérents est stable:

ssi \(∀x, x' ∈ Cl(A), x ∪ x' \text{ clique } ⟹ f(x ∩ x') = f(x) ∩ f(x') \text{ (préserve les infs)}\)

Prop: Une fonction $f:A⟶ B$ continue est stable ssi

\[∀(d, b), (d', b) ∈ tr(f), d ∪ d' \text{ clique } ⟹ (d∩d', b) ∈ tr(f)\]

NB:

  • dès qu’on a deux informations finies justifiant un même $b$, alors leur intersection est une justification.

  • le ou parallèle n’est pas stable, à cause de $(\lbrace 1 \rbrace, 1), (\lbrace 1’ \rbrace, 1)$ : $\lbrace 1, 1’ \rbrace$ est bien une clique, mais la clique vide pose problème: $(∅ = \lbrace 1 \rbrace ∩ \lbrace 1’ \rbrace, 1) ∉ tr(por)$

    • si on supprime l’un des deux ($(\lbrace 1 \rbrace, 1), (\lbrace 1’ \rbrace, 1)$), on récupère la stabilité

Preuve:

⟹

Si $(d, b), (d’, b’) ∈ tr(f)$, alors

\[b ∈ f(d) ∩ f(d') = f(d ∩ d')\]

Donc $(d∩d’, b) ∈ tr(f)$

⟸

Soit $f: A ⟶ B$ continue, et soient $x, x’ ∈ Cl(A)$ tq $x ∪ x’ ∈ Cl(A)$.

⊆

$b ∈ f(x ∩ x’)$, donc par continuité:

\[∃d ⊆_{fini} x ∩ x'; b ∈ f(d)\]

Mais $d ⊆ x, x’$, donc par monotonie:

\[b ∈ f(x), f(x')\]

$\supseteq$

$b ∈ f(x) ∩ f(x’)$, donc par continuité:

\[∃ \begin{cases} d ⊆_{fini} x \\ d' ⊆_{fini} x' \\ \end{cases}; b ∈ f(d) ∩ f(d')\]

Donc par définition:

\[(d, b), (d', b) ∈ tr(f)\]

On sait que $x ∪ x’$ est une clique, et $d ∪ d’ ⊆ x ∪ x’$, donc $d ∪ d’$ est une clique.

On applique la propriété et on a $(d ∩ d’, b) ∈ tr(f)$, d’où $b ∈ f(d ∩ d’)$.

Mais $d∩d’ ⊆ x ∩ x’$, donc par monotonie:

\[b ∈ f(x ∩ x')\]

La catégorie des espaces cohérents est une CCC

Soit $Stab$ la catégorie des espaces cohérents et fonctions stables.

Observation préliminaire:

\[Stab(Γ \& A, B) ≃ Stab(Γ, A ⇒ B)\]

où $A ⇒ B$ est le hom-interne de la catégorie, i.e.

\[Stab(⊤, A ⇒ B) ≃ Stab(A, B)\]

où $⊤$ est l’objet terminal de $Stab$, avec

\[\vert ⊤ \vert = ∅\]

Maintenant, qu’est-ce qu’un “point” d’un espace cohérent $A$?

\[t: ⊤ ⟶ A\]

c’est juste une clique de $A$, puisque $⊤$ ne contient qu’une clique: la clique vide.

⟶ Les “points” d’un espace cohérent $A$ sont exactement les cliques de $A$.

De ce fait:

\[Stab(⊤, A) = Cl(A)\]

Donc on cherche:

\[Cl(A ⇒ B) = Stab(⊤, A ⇒ B) ≃ Stab(A, B)\]

Regardons, par hasard, les traces? Ne seraient-elles pas les cliques d’un espace cohérent?

Si $f: A ⟶ B$,

\[tr(f) ⊆ Cl_{fin}(A) × \vert B \vert\]

Structure de CCC

Pour un espace cohérent $A$, on définit la

cohérence stricte $a \frown_A a’$:

ssi $a \sim_A a’$ et $a ≠ a’$

Soient $A, B$ des espaces cohérents. On définit

\[\vert A ⇒ B \vert ≝ Cl_{fin}(A) × \vert B \vert\]

Avec la caractérisation précédente des fonctions continues stables:

\[(d, b) \sim_{A ⇒ B} (d', b') \text{ ssi } d∪d' \text{ clique } ⟹ b \frown_B b'\]

Trace stable

Dans la trace “classique” (dite “trace continue” $tr_{cont}$), il est possible d’avoir $(d, b)$ et $(d’, b)$, où $d ∪ d’$ est une clique.

Mais par clôture par intersection, on sait alors que $(d ∩ d’, b)$ appartient à la trace.

Trace stable:
\[tr_{stable}(f) ≝ \left\lbrace (δ, b) \mid b ∈ \vert B \vert, \; δ = \bigcap_{(d, b) ∈ tr_{cont}(f) \text{ deux à deux compatibles}} d \right\rbrace\]

(deux-à-deux compatibles: i.e $d ∪ d’$ est une clique)

Rappel:

\[f(x) = \lbrace b \mid ∃ (d, b) ∈ tr(f), d ⊆ x \rbrace\]

Soit $f: A ⟶ B$ stable.

On va maintenant montrer que chaque clique correspond exactement à une fonction stable.

C’est-à-dire qu’on veut définir une fonction bijective:

\[tr: Stab(A, B) ⟶ Cl(A ⇒ B)\]

$Stab(A, B) ⟶ Cl(A ⇒ B)$

On veut vérifier que tous $(d, b), (d’, b’) ∈ tr(f)$ sont cohérents.

Si $d ∪ d’$ est une clique.

On a $b ≠ b’$, car quitte à prendre l’intersection, on peut supposer $d$ minimal (par définition de trace stable (i.e. la trace où on a pris la plus petite de toutes les informations compatibles $d$ qui donnent le même $b$)).

On sait que $b ∈ f(d)$ et $b’ ∈ f(d’)$ par définition de la trace.

Par monotonie,

\[b, b' ∈ f(d ∪ d')\]

et donc

\[b \frown_B b'\]

car $f(d ∪ d’)$ est une clique.

$fun ≝ trace^{-1}: Cl(A ⇒ B) ⟶ Stab(A, B)$

\[fun ≝ \begin{cases} Cl(A ⇒ B) &⟶ Stab(A, B) \\ t &\mapsto fun \, t ≝ \begin{cases} Cl(A) &⟶ Cl(B) \\ x &\mapsto \lbrace b ∈ \vert B \vert \mid ∃(d, b) ∈ t, d ⊆ x \rbrace \end{cases} \end{cases}\]

La catégorie des espaces cohérents est donc cartésienne close.

Naissance de la logique linéaire

C’est de là qu’est née la logique linéaire, avec Girard.

Problème: il n’y a pas de coproduit dans la catégorie $Stab$.

On voudrait définir $A_1 \oplus A_2$ de manière duale à $A_1 \& A_2$, c’est à dire prendre la bête union disjointe:

  • \[\vert A_1 \oplus A_2 \vert = \vert A_1 \vert + \vert A_2 \vert\]
  • \[(i, c) \sim_{A_1 \oplus A_2} (i', c') ⟺ i=i' et c \sim_{A_i} c'\]

On voudrait avoir la propriété universelle du coproduit (définition par cas), mais il y a un problème les cliques vides de $A_1$ et de $A_2$ coïncident dans $A_1 \oplus A_2$ !!!

MAIS….. le problème serait réglé si les fonctions étaient linéaires !!! En effet, la clique vide serait sytématiquement envoyée sur la clique vide, donc on se ficherait bien que les cliques vides de $A_1$ et $A_2$ coïncident dans $A_1 \oplus A_2$ !

Linéarité

Une fonction stable $f: A ⟶ B$ est linéaire:

si

  • $f(∅) = ∅$
  • \[∀x, x', \; x ∪ x' ∈ Cl(A) ⟹ f(x ∪ x') = f(x) ∪ f(x')\]

Prop: Soit $f: A ⟶ B$ stable. $f$ est linéaire ssi

\[∀(d, b) ∈ tr(f), \; d \text{ est un singleton}\]

⟹

Soit $f$ linéaire et $(d, b) ∈ tr(f)$.

Trivilement, $d ≠ ∅$, car sinon $b ∈ f(d) = f(∅) = ∅$.

Supposons $d = d’ ∪ d’’$ avec $a’ ∈ d’ \backslash d’’, a’’ ∈ d’’ \backslash d’$.

On a $b ∈ f(d’ ∪ d’’) = f(d’) ∪ f(d’’)$.

Si $b ∈ f(d’) ∩ f(d’’) = f(d’ ∩ d’’)$ (par stabilité), on contredirait la minimlité de $d$ (dans la trace stable).

Donc soit $b ∈ f(d’)$, soit $b ∈ f(d’’)$, ce qui est aussi impossible par minimalité de $d$.

⟸

Soit $f$ stable vérifiant la propriété.

On veut démontrer:

  1. $f(∅) = ∅$

  2. $f(x ∪ x’) = f(x) ∪ f(x’)$

1) vient du fait que

\[f(x) = \lbrace b ∈ \vert B \vert \mid ∃ (d, b) ∈ tr(f), d ⊆ x \rbrace\]

et que les $d$ sont des singletons: aucun d’eux n’est inclus dans $x = ∅$.

Pour 2):

$\supseteq$

triviale, par monotonie, puisque $f(x), f(x’) ⊆ f(x ∪ x’)$

$⊆$

$b ∈ f(x ∪ x’)$: on sait qu’il existe $(d, b) ∈ tr(f)$ tq

  • $d ⊆ x ∪ x’$
  • $b ∈ f(d)$

Mais $d = \lbrace a \rbrace$, donc $a ∈ x ∪ x’$, soit:

  • si $a ∈ x$, alors $b ∈ f(x)$
  • si $a ∈ x’$, alors $b ∈ f(x’)$

NB: $b ∈ f(x)$ ⟶ $(d, b)$ tel que

  • $b ∈ f(d)$
  • $d ⊆_{fin} x$

⟹

  1. Pour les fonctions continues: $d$ est fini
  2. Pour les fonctions stables: $d$ est minimal
  3. Pour les fonctions linéaires: $d$ est un singleton

Leave a comment