sheaves.tex

Soit $\Sigma = \{R_1, \dots R_n\}$ un alphabet de symboles de relations, avec
leurs arités $a_1, \dots a_n\in\N$.

L'objectif est de créer une catégorie $\C_\Sigma$, que l'on notera $\C$ en l'absence
d'ambiguïté sur $\Sigma$, telle que la donnée d'un problème CSP soit exactement la donnée
d'un faisceau sur $\C$ (à valeur dans $\fset$, puisqu'on se limite à ce cadre là). Pour
pouvoir parler de faisceau, il faudra munir $\C$ d'une structure de site.

\subsection{Intuition}

Qu'est-ce qu'un CSP
sur un alphabet de relation $\Sigma$~? C'est la donnée d'un domaine fini $D$ et
de relations sur $D$ de bonne arité pour chaque relation de $\Sigma$. Si
$\Sigma = \{R_1, \dots R_n\}$, on peut poser la catégorie qui a pour objets
$\{\star, R_1, \dots R_n\}$ et comme flèches les identités, ainsi que pour
tout $1\leq i\leq n$, autant de flèche de $\star$ vers $R_i$ que l'arité de
$R_i$. Un préfaisceau sur cette catégorie nous donne alors un CSP (et
vice-versa, par contre plusieurs préfaisceaux peuvent correspondre au même
CSP).

Pourquoi ne pas se contenter de ça ? Parce que cette catégorie n'est pas
intéressante pour travailler sur les CSP. En effet, elle ne contient comme
information que la liste des relations et leur arité, et rien d'autre. Nous la
noterons d'ailleurs $\Sigma$, puisque la donnée d'un alphabet de relation est
aussi exactement la donnée de leur liste et leurs arités. $\Sigma$ a donc la forme~:

\[\begin{tikzcd}
    & \star \arrow[ddl, shift right, swap, "f_1^1"]
            \arrow[ddl]
            \arrow[ddl, shift left, "f_{\text{ar}(R_1)}^1"]
            \arrow[ddr, shift right, swap, "f_1^m"]
            \arrow[ddr]
            \arrow[ddr, shift left, "f_{\text{ar}(R_m)}^m"]
            \\
    & & \\
    R_1 & \dots & R_m \\
\end{tikzcd}\]

C'est là que le résultat suivant entre en jeu.

\begin{prop}\label{canEq}
    Soit $Y : \psh(\C)\rightarrow\shc(\psh(\C))$ le plongement de Yoneda sur
    $\psh(\C)$.

    Notons $y : \C\rightarrow\psh(\C)$ le plongement de Yoneda sur $\C$. Posons~:

    \[L = \left\{\begin{array}{ccc}
             \shc(\psh(\C)) & \rightarrow & \psh(\C) \\
             F              & \mapsto     & F\circ y^\text{op} \\
    \end{array}\right.\]

    Alors $L\circ Y\cong\text{Id}_{\psh(\C)}$ et
    $Y\circ L\cong\text{Id}_{\shc(\psh(\C))}$. Cela fait de $Y$ une équivalence de
    catégories.
\end{prop}

\begin{pv}
    Admis.
\end{pv}

Par cet isomorphisme, $\shc(\psh(\Sigma))$ correspond aux CSP. On aimerait donc pouvoir
interpréter cette fois un préfaisceau sur $\Sigma$ comme une formule. C'est en fait assez
simple, on procède par analogie avec la façon de représenter un graphe dirigé. Un graphe
(au sens informatique) est un préfaisceau (fini) sur la catégorie $G$ suivante~:

\[\begin{tikzcd}
    v \arrow[r, bend right, "s"] \arrow[r, bend left, "t"] & e \\
\end{tikzcd}\]

Un tel préfaisceau $F : G^{\text{op}}\rightarrow\fset$ représente le graphe ayant pour
ensemble sous-jacent $Fe$ et pour arrêtes $Fv$. De plus, la source d'une arrête $a\in Fv$
est $Fs(a)$ et sa destination est $Ft(a)$. On peut aussi interpréter un graphe comme
étant une formule conjonctive, dont les variables sont les points et qui possède un
unique prédicat binaire qui marque les arrêtes. On remarque que la catégorie $G$ est
exactement celle d'un alphabet avec un seul prédicat binaire. On peut donc généraliser
l'interprétation.

\begin{defi}{Formule associée à un faisceau}
    Soit $A\in\psh(\Sigma)$. On note $\phi_A$ la formule suivante~:
    
    \[\bigwedge_{1\leq i\leq m} \bigwedge_{x\in AR_i}
            R_i(Af_1^i(x), \dots Af_{\ar(R_i)}^i(x)) \]

    Avec la règle qu'une conjonction vide est $\top$

    C'est une formule conjonctive sur $\Sigma$ et dont les variables sont prises dans
    l'ensemble $A\star$.
\end{defi}

On pose alors $\C_\Sigma = \psh(\Sigma)$ notre nouvelle catégorie des formules.

\subsection{Propriétés générales de $\C_\Sigma$}

\begin{lem}
    $\C_\Sigma$ possède toutes ses limites et colimites finies.
\end{lem}

\begin{pv}
    C'est une propriété générale des catégories de faisceaux.
\end{pv}

On peut alors étudier quelques limites particulières.

\begin{lem}
    Soit $\mathbf{0}$ l'objet inital de $\C_\Sigma$. Alors $\phi_\mathbf{0}\iff\top$.
\end{lem}

\begin{pv}
    Une limite sur une catégorie de faisceau se calcule point par point. Donc $\mathbb{0}$
    est le préfaisceau qui envoie tous les objets de $\Sigma$ sur $\emptyset$ et toutes
    les flèches sur $\id_\emptyset$.

    Alors $\phi_\mathbf{0} = \bigwedge_{1\leq i\leq m}\top \iff \top$.
\end{pv}

\begin{lem}
    Soit $\mathbf{1}$ l'objet final de $\C_\Sigma$. Alors~:

    \[\phi_\mathbf{1} \iff \bigwedge_{1\leq i\leq m}R_i(x,\dots x)\]
\end{lem}

\begin{pv}
    Même démarche que pour la proposition précédente.
\end{pv}

\begin{lem}
    Soient $A$ et $B$ deux objets de $\C_\Sigma$. On note $A\wedge B$ leur coproduit
    dans $\C_\Sigma$. On a alors~:

    \[\phi_{A\wedge B} \iff \phi_A\wedge\phi_B \]
\end{lem}

On donne aussi une représentation sous forme de séquents, qui est pratique
pour travailler.

\begin{defi}{Séquent associé à une formule}\label{formSeq}
    Soit $\phi$ une formule conjonctive que l'on suppose mise sous la
    forme canonique $\exists x_1,\dots\exists x_n, R(\dots)\wedge R(\dots)$. On
    y associe le séquent $\ml{\phi} = x_1,\dots x_n\vdash R(\dots), \dots, R(\dots)$.
\end{defi}

\begin{rem}
    L'habitué remarquera que la partie droite du séquent est utilisée de manière non
    canonique. En effet, elle sert usuellement à représenter une disjonction et
    l'on s'en sert ici pour représenter un conjonction. C'est lié au fait que
    les faisceaux partent de $\C_\Sigma^\text{op}$, et donc que le sens de lecture
    des règles de déduction est inversé lorsque pris par le faisceau. Ainsi, si l'on
    veut avoir des règles correspondant aux conjonctions à l'arrivée, il faut dualiser
    les règles, et cela nous donne les règles de disjonction, ce qui est cohérent avec
    l'interprétation standard des séquents.
\end{rem}


\subsection{Correction}

Le théorème \ref{canEq} nous dit que $\shc(\C_\Sigma)\cong \C_\Sigma$, et l'on a
une interprétation de $\C_\Sigma$ à la fois en terme de formules et en terme de
CSP.  On a donc qu'un faisceau sur $\C_\Sigma$, vu comme catégorie de formules,
est assimilé par ce théorème à un élément de $\C_\Sigma$, vu comme catégorie de
CSPs.  Cependant, en utilisant l'approche de sémantique de faisceaux de la
définition \ref{shSem}, on obtient deux sémantiques possibles pour une formule
d'après un faisceau $F$.  Soit on le fait selon sa structure de formule
conjonctive en utilisant le CSP donné par $LF$, soit on considère directement
son image par $F$. Il faut donc montrer que ces deux approches coïncident.

Soit $F$ un faisceau et $X\in\C_\Sigma$ une formule. On définit $\sem{X}$ comme
étant $\sem{\phi_X}$ d'après la définition \ref{cspSem} pour le CSP $LF$. Pour
définir $\sem{X}_F$, on a besoin du lemme suivant~:

\begin{lem}
    Soit $v\in X\star$ une variable de la formule $X$. Notons
    $\ast = y\star\in\C_\Sigma$. Alors il existe une unique transformation naturelle
    $\theta^v : \ast\rightarrow X$ telle que $\theta^v_\star(*) = v$.
\end{lem}

\begin{pv}
    On remarque que $y\star\star$ est singleton, donc
    $y\star\star\rightarrow X\star\cong X\star$ de manière canonique. On remarque que pour
    $R\in\C_\Sigma$ avec $R\neq\star$, $y\star R=\emptyset$. Donc il existe une unique
    fonction de $y\star R$ vers $X R$. 
\end{pv}

On peut alors définir la sémantique selon $F$.

\begin{defi}{Sémantique selon un faisceau}
    On pose~:

    \[\sem{X}_F = \left\{f:\begin{array}{ccc}
        X\star & \rightarrow & F\ast \\
        v      & \mapsto     & F\theta^v(x)
    \end{array} | x\in F X\right\}\]
\end{defi}

Le résultat qui nous intéresse est le suivant~:

\begin{prop}\label{shSemCorrect2}
    $\sem{X} = \sem{X}_F$
\end{prop}

\begin{pv}
    La preuve est exactement la même que celle du théorème \ref{shSemCorrect},
    avec $\ast$ qui joue le rôle de $\star$ et les $yR_i$ qui jouent le rôle
    des $R_i(x, y, \dots)$.
\end{pv}

\subsection{Comma catégories à la rescousse !}

Un problème apparait quand on essaye de transposer la définition de pp-interprétabilité
puisqu'on doit faire référence à des formules où seulement certaines variables sont
libres et certaines quantifiées. Or dans notre système toutes les variables d'une
formule sont au même niveau. Il faut donc introduire un moyen de \emph{sélectionner}
certaines variables.

Considérons la flèche suivante~:
$x_1,\dots, x_n\vdash \rightarrow x_1,\dots, x_k\vdash\Delta$ avec $k>n$ qui identifie
$n$ variables de $x_1,\dots x_k$. Alors si l'on regarde la sémantique de cette flèche,
elle prend une solution de $x_1,\dots x_k\vdash\Delta$ et donne une solution de
$x_1,\dots, x_n\vdash$ qui lui corresponds. Autrement dit, l'image de ce morphisme
correspond à des $n$-uplets solution de $\exists \dots:\Delta$ où les variables
quantifiées sont celles qui ne sont pas sélectionnées par le morphisme.

On a donc un moyen de représenter une formule avec certaines variables liées et certaines
variables libres~: ce sont des morphismes dans $\C_\Sigma$ d'une formule de la forme
$x_1,\dots x_n\vdash$ vers une autre formule. Cela fait donc penser à une comma
catégorie de la forme $F/\C_\Sigma$ où $F$ est un foncteur bien choisi.

\begin{defi}{Catégorie $\cf$}
    On note $\cf$ la catégorie squelette de $\fset$. Décrivons la plus explicitement.
    Ses objets sont les entiers naturels, et ses flèches les fonctions quelconques
    de l'un vers l'autre.
\end{defi}

On remarque l'égalité suivante~:

\begin{lem}
    Soit $n$ un entier naturel. Alors, en notant $n\ast$ le coproduit de $\ast$ pris
    $n$ fois avec lui-même si $n>0$ et $\mathbf{0}$ l'élément final sinon, on
    a~:

    \[ <\phi_{n\ast}> = x_1,\dots, x_n\vdash \]
\end{lem}

\begin{pv}
    Application directe du lemme \ref{seqStandarts}.
\end{pv}

On définit alors le foncteur suivant~:

\begin{defi}{Foncteur $\arf$}
    On crée un foncteur de $\cf$ vers $\C_\Sigma$. Il envoie $n$ sur $n\ast$ et
    $f : n\rightarrow m$ vers la transformation naturelle $\theta$ telle que
    $\theta_\star = f$ et $\theta_X = \emptyset$ pour $X\neq\star$. On nomme ce
    foncteur $\arf : \cf\rightarrow\C_\Sigma$.
\end{defi}

On peut alors effectuer la construction décrite ci-dessus.

\begin{defi}{Catégorie des formules avec variables liées}
    On pose $\tsigma = \arf/\C_\Sigma$ la catégories des formules avec variables
    liées.

    On dispose de deux foncteurs d'oubli canoniques $U_1 : \tsigma\rightarrow\cf$
    et $U_2 : \tsigma\rightarrow\C_\Sigma$.
\end{defi}

On peut munir $\tsigma$ d'une représentation sous forme de séquents de manière
similaire à ce qui est fait pour $\C_\Sigma$, mais c'est moins utile. La représentation,
ainsi que la représentation de quelques limites usuelles, sont disponibles en
annexe \ref{seqTSigma}.

\begin{defi}{Injection de $\C_\Sigma$ dans $\tsigma$}
    On définit le foncteur $\iota:\C_\Sigma\rightarrow\tsigma$ de la façon suivante~:

    \[ \iota := \left\{\begin{array}{ccc}
        \Sigma & \rightarrow & \tsigma \\
        X      & \mapsto     & \mid X\star\mid\ast\rightarrow X \\
        \theta : X\rightarrow Y & \mapsto &
            \begin{tikzcd}
                \mid X\star\mid\ast\arrow[d]
                                   \arrow[r, "\theta_\star"]
                    & \mid Y\star\mid\ast\arrow[d] \\
                X\arrow[r, "\theta"]
                    & Y \\
            \end{tikzcd} \\
    \end{array}\right. \]
\end{defi}

\begin{lem}
    $\iota$ est un foncteur plein et fidèle.
\end{lem}

\begin{cor}
    $\iota$ préserve les colimites finies.
\end{cor}

\begin{lem}
    On a une adjonction~:

    \[\begin{tikzcd}
        \cf\arrow[rr, bend right, swap, "\iota\circ\arf"] & \top
            & \tsigma\arrow[ll, bend right, swap, "U_1"] \\
    \end{tikzcd}\]
\end{lem}

\begin{pv}
    Soit $n\in\cf$ et $m\ast\rightarrow X\in\tsigma$. On veut montrer que~:

    \[\cf(n, U_1(m\ast\rightarrow X)) = \tsigma(\iota(\arf(n)), m\ast\rightarrow X)\]

    En développant les définitions, on cherche à obtenir une bijection entre
    les fonctions de $n$ vers $m$ et les carrés commutatifs de la forme suivante~:

    \[\begin{tikzcd}
        n\ast\arrow[r] & X \\
        n\ast\arrow[u, "\id"]\arrow[r] & m\ast\arrow[u] \\
    \end{tikzcd}\]

    C'est immédiat~: la flèche du bas est exactement une fonction de $n$ vers $m$,
    et celle du haut en entièrement déterminée par la flèche du bas.
\end{pv}

\begin{cor}\label{arfExact}
    $\arf$ préserve les colimites finies.
\end{cor}

\begin{theo}{Colimites de $\tsigma$}\label{commaCL}
    Soit $D : I\rightarrow\tsigma$ un foncteur avec $I$ une catégorie finie.

    Alors $D$ a une colimite. De plus, $U_1(\colim_I D) = \colim_I (U_1\circ D)$ et
    $U_2(\colim_I D) = \colim_I (U_2\circ D)$.

    De plus, $\arf\circ U_1\circ D : I\rightarrow\C_\Sigma$ a une colimite, qui
    est $\colim_I (\arf\circ U_1\circ D) = \arf(U_1(\colim_I D))$. Alors
    $U_2(\colim_I D)$ est sommet d'un cocône sur $\arf\circ U_1\circ D$, engendré
    par les flèches dans l'image de $D$. De plus la flèche de $\colim_I D$ est
    l'unique flèche allant de $\colim_I (\arf\circ U_1\circ D)$ vers $U_2(\colim_I D)$
    qui fait commuter ce cocône.
\end{theo}

\begin{pv}
    On note $x$ l'objet de $\tsigma$ décrit dans l'énoncé de ce théorème. Il existe
    bien car $\cf$ et $\C_\Sigma$ sont cocomplètes. On veut
    montrer que c'est la colimite de $D$.

    On remarque que l'égalité $\arf(\colim_I U_1\circ D) = \colim_I (\arf\circ U_1\circ D)$
    découle immédiatement du corrolaire \ref{arfExact}.

    La situation est la suivante~:

    \begin{center}\begin{tikzpicture}
        \draw[->] (0,0)   node[above] (d1a) {$\bullet$}
              -- (0,-1)   node[below] (d1b) {$\bullet$};
        \draw[->] (1,.5)  node[above] (d2a) {$\bullet$}
              -- (1,-.5)  node[below] (d2b) {$\bullet$};
        \draw[->] (3,-.5) node[above] (d3a) {$\bullet$}
              -- (3,-1.5) node[below] (d3b) {$\bullet$};
        \draw[->] (d1a) -- (d2a);
        \draw[->] (d1b) -- (d2b);
        \draw[dashed] (1.5,-0.5) ellipse (3 and 1.7);
        \draw (2.3,1.2) node[above] {$D$};

        \draw[->] (2,-3) node[above] (xa) {$\bullet$}
              -- node[left] {$x$} (2,-4)  node[below] (xb) {$\bullet$};
        \draw[->,blue]  (d1a) -- (xa);
        \draw[->,blue]  (d2a) -- (xa);
        \draw[->,blue]  (d3a) -- (xa);
        \draw[->,red]   (d1b) -- (xb);
        \draw[->,red]   (d2b) -- (xb);
        \draw[->,red]   (d3b) -- (xb);
        \draw[->,green] (d1a) edge[out=270, in=130] (xb);
        \draw[->,green] (d2a) edge[out=270, in=100] (xb);
        \draw[->,green] (d3a) edge[out=270, in=70]  (xb);
    \end{tikzpicture}\end{center}

    Les flèches bleues indiquent des flèches dans l'image de $\arf$ et les flèches
    rouges sont dans l'image de $\id_{\C_\Sigma}$. Pour montrer que l'on a un cocône,
    il faut montrer que les carrés verticaux sont commutatifs, ce qui est immédiat
    puisque la flèche de $x$ vient de la propriétés de colimite de
    $\arf(\colim_I U_1\circ f)$ appliquée au cocône formé par les flèches vertes.

    On prends maintenant un cocône $c$ sur $D$. En composant par $U_1$ et $U_2$ on obtient
    qu'il existe au plus une flèche de $x$ vers $c$. Pour vérifier qu'il en existe une,
    il faut montrer qu'on peut obtenir un carré commutatif à partir des flèches de
    colimites dans $\cf$ et $\C_\Sigma$, ce qui est direct.
\end{pv}

\begin{cor}
    $U_1$ et $U_2$ sont exacts à droite.
\end{cor}