naif.tex

% r         -- n-uplet
% \alpha    -- la relation d'équivalence
% R         -- une lettre de relation/un atome
% f,g,h     -- une flèche dans la catégorie de \Sigma
% \phi,\psi -- une formule syntaxique
% [\phi]    -- une formule dans la catégorie de \Sigma
% x,y,z     -- une variable d'une formule syntaxique
% v         -- une variable dans la catégorie (un élément de \C(\star,[\phi])
% bf{x},    -- une solution (ie un objet de F[\phi])
% bb{x},    -- une solution (ie un objet de \sem{\phi})
% F,G,H     -- un préfaisceau

\subsection{Définition de $\C$}

Afin de simplifier, on va essayer de donner une représentation des formules indépendante
du renommage des variables (pour éviter les problèmes d'alpha-équivalence) et qui réduit
la structure d'une formule à son plus simple.

La donnée d'une formule est alors un $n$-uplet $r\in\N^n$, avec $r_1$ qui indique le
nombre d'occurence du prédicat $R_1$, $r_2$ le nombre d'occurences du prédicat $R_2$,
\dots On ne dit pour l'instant rien sur les variables, et on appelle $r$ le 
\emph{squelette} de la formule.

\begin{defi}{Emplacement}
    Étant donné $r\in\N^n$ un squelette de formule, on va définir l'ensemble des
    \emph{emplacements} de la façon suivante~:

    \[ \E(r):= \{(i,j,k)\in\N^3 |        1\leq i\leq n
                                  \wedge 1\leq j\leq r_j
                                  \wedge 1\leq k\leq a_j\} \]

    Intuitivement, un triplet $(i,j,k)\in\E(r)$ désigne un endroit où une variable peut
    aller dans la formule, plus précisément cela désigne le $k$-ième argument de la
    $j$-ième instance d'un prédicat $R_i$.
\end{defi}

Dans une formule, tous les emplacement possibles ne sont pas nécessairement remplis
par des variables différentes, il faut donc un moyen d'assimiler les lieux de variable
qui sont occupés par la même variable. On fait ça de façon brutale en se munissant d'une
relation d'équivalence sur $\E(r)$.

\begin{defi}{Formule}
    Une \emph{formule} est alors un couple $(r,\alpha)\in\N^n\times\P(\E(r)^2)$
    où $\alpha$ est une relation d'équivalence. On nomme une \emph{variable} de
    $(r,\alpha)$ une classe d'équivalence de lieux, c'est à dire un élément de
    $\E(r)/\alpha$.
\end{defi}

La catégorie $\C$ va alors avoir comme objets les formules telles que définit ci-dessus,
plus un objet spécial $\star$.

Il faut maintenant définir une notion de morphisme sur $\C$. On va distinguer les
morphismes entre formules, et les morphismes depuis $\star$, qui a un rôle particulier.
Commençons par les morphismes depuis $\star$. Ces morphismes sont simples~: ils 
représentent les variables de la formule visée.

\begin{defi}{Morphismes depuis $\star$}
    On pose $\C(\star,\star) = \{\text{id}_\star\}$ (cet objet n'a pas d'intérêt autre
    que d'être nécessaire). Plus intéressant, on pose~:

    \[\C(\star, (r,\alpha)) = \E(r)/\alpha) \]
\end{defi}

Maintenant, il faut définir les morphismes entre formules. L'idée est qu'un morphisme
d'une formule vers une autre est une instance de la première formule dans la deuxième.
Intuitivement, ça indique que la première formule est une sous-formule de la deuxième,
et de quelle manière. Pour cela, il faut un moyen d'indiquer où vont les anciennes
instances des relations. On fait ça à l'aide d'un \emph{déplacement}.

\begin{defi}{Déplacement}
    Un \emph{déplacement} de $r$ vers $r'$ est un n-uplet de fonctions $f$, tel que
    $\forall 1\leq i\leq n, f_i : r_i\hookrightarrow r_i'$.

    On note l'ensemble des déplacements de $r$ vers $r'$ $\D(r,r')$
\end{defi}

\begin{rem}
    On remarque que $\D(r,r')\neq\emptyset\implies r\leq r'$ où $\leq$ est l'ordre
    partiel point par point.
\end{rem}

On va maintenant définir l'action d'un déplacement sur une relation.

\begin{defi}{Déplacement d'une relation}
    Soient $(r,\alpha)$ et $(r',\alpha')$ deux formules. Soit $f\in\D(r,r')$. On pose~:

    \[ \begin{array}{rccl}
          f(\alpha) &:= & & \{ ((i,f_i(j), k), (i', f_{i'}(j'), k'))
                              ~|~ ((i,j,k), (i',j',k'))\in \alpha \} \\
                    &   & \cup &\{ ((i,j,k), (i,j,k)) ~|~ (i,j,k)\in\V(r') \} \\
    \end{array} \]
\end{defi}

On peut vérifier que cette définition a bien un sens~:

\begin{lem}
    Soient $(r,\alpha)$ et $(r',\alpha')$ deux formules. Soit $\phi\in\D(r,r')$.
    Alors $\phi(\alpha)$ est une relation d'équivalence sur $\E(r')$.
\end{lem}

On a maintenant tout en main pour définir les morphismes entre formules.

\begin{defi}{Morphismes entre formules}
    Soient $(r,\alpha)$ et $(r',\alpha')$ deux formules. On pose~:

    \[\C((r,\alpha),(r',\alpha')) := \{ f\in\D(r,r') ~|~
                                        f(\alpha)\subseteq \alpha' \}\]
\end{defi}

\begin{rem}\begin{itemize}
    \item $\C((r,\alpha), (r',\alpha'))\neq\emptyset \implies r\leq r'$, ce qui
        est cohérent avec l'intuition derrière la définition des morphismes.
    \item $\C((r,\alpha), (r,\alpha))$ n'est jamais vide, il contient toujours le $n$-uplet
        des identités des $r_i$. Ce sera d'ailleurs la flèche identité pour la loi
        de composition que l'on définira plus bas.
    \item $\star$ n'a aucune flèche entrante en dehors de son identité.
\end{itemize}\end{rem}

On a maintenant besoin de quelques définitions et lemmes préliminaires pour pouvoir
définir proprement la composition de morphismes dans $\C$.

\begin{lem}
    Soient $(r,\alpha)$, $(r',\alpha')$ et $(r'',\alpha'')$ des formules.
    Soient $f\in\C((r,\alpha),(r',\alpha'))$
        et $g\in\C((r',\alpha'),(r'',\alpha''))$.
    Alors $g\circ f\in\C((r,\alpha),(r'',\alpha''))$ où $\circ$ est compris
    terme à terme.
\end{lem}

\begin{pv}
    Comme la composition de deux injections est un injection, on a que
    $g\circ f\in\D(r,r'')$.

    On sait que l'on a $f(\alpha)\subseteq \alpha'$ et $g(\alpha')\subseteq \alpha''$. Or
    les déplacements sont immédiatement croissants pour l'inclusion lorsque pensés
    comme fonctions de relations.
    Donc $g\circ f(\alpha)\subseteq g(\alpha')\subseteq \alpha''$.
\end{pv}

\begin{defi}{Déplacement d'un lieu de variable}
    Soient $(r,\alpha)$ et $(r',\alpha')$ des formules, et $f\in\D(r,r')$.
    Soit $(i,j,k)\in\E(r)$. On définit $f((i,j,k)) = (i, f_i(j), k)\in\V(r')$.
\end{defi}

\begin{lem}
    Soient $(r,\alpha)$ et $(r',\alpha')$ des formules, et
    $f\in\C((r,\alpha),(r',\alpha'))$.
    On a que~:
    
    \[\forall e_1,e_2\in\E(r), (e_1,e_2)\in\alpha\implies (f(e_1),f(e_2))\in \alpha'\]
\end{lem}

\begin{defi}{Déplacement d'une variable}
    Soient $(r,\alpha)$ et $(r',\alpha')$ des formules, et
    $f\in\C((r,\alpha),(r',\alpha'))$.
    Soit $v\in\E(r)/\alpha$. Soit $e\in v$. On pose $f(v) = [\phi(e)]\in\V(r')/\alpha'$.

    Le lemme précédent nous assure que c'est bien définit.
\end{defi}

On a maintenant tout en main pour définir la composition de morphismes.

\begin{defi}{Composition dans $\C$}
    Il y a trois cas à considérer~:\begin{itemize}
        \item $id_\star\in\C(\star,\star)$ et $f\in\C(\star, x)$ où $x$ est n'importe
            quel objet de $\C$. Alors $f\circ id_\star := f$.
        \item $v\in\C(\star, (r,\alpha))$ et $f\in\C((r,\alpha), (r',\alpha'))$. Alors
            on pose $f\circ v := f(v)$.
        \item $f\in\C((r,\alpha),(r',\alpha'))$ et $g\in\C((r',\alpha'),(r'',\alpha''))$.
            Alors on pose $g\circ f$ définit terme à terme, comme dans le lemme
            précédent.
    \end{itemize}
\end{defi}

\begin{lem}
    Pour toute formule $(r,\alpha)$, on a que
        $f=(id_{r_1},\dots id_{r_n})\in\C((r,\alpha),(r,\alpha))$.
    De plus, $\forall g\in\C(x, (r,\alpha)), f\circ g = g$
    et $\forall g\in\C((r,\alpha), (r',\alpha')), g\circ f = g$.
\end{lem}

\begin{lem}
    Soient $(r,\alpha)$, $(r',\alpha')$ et $(r'',\alpha'')$ trois formules.
    Soit $v\in\C(\star,(r,\alpha))$,
    $f\in\C((r,\alpha), (r',\alpha'))$ et $g\in\C((r',\alpha'), (r'',\alpha''))$.

    Alors $(g\circ f)\circ v = g\circ (f\circ v)$.
\end{lem}

\begin{lem}
    Soient $(r_1,\alpha_1)$, $(r_2,\alpha_2)$, $(r_3,\alpha_3)$ et $(r_4,\alpha_4)$
    quatre formules.
    Soient $f\in\C((r_1,\alpha_1), (r_2,\alpha_2))$,
    $g\in\C((r_2,\alpha_2), (r_3,\alpha_3))$ et $h\in\C((r_3,\alpha_3),(r_4,\alpha_4))$.

    Alors $h\circ(g\circ f) = (h\circ g)\circ f$.
\end{lem}

\begin{pv} Les trois lemmes sont immédiats. Il suffit d'écrire la définition de $\circ$
    dans chacun des cas pour que ça marche.
\end{pv}

\begin{theo}{Définition de $\C$}
    $\C$ est une catégorie.
\end{theo}

\begin{pv} Conséquence immédiate des trois lemmes précédents.
\end{pv}

\subsection{Représentation des formules}
% TODO est-ce qu'on veut faire les preuves en détail ici ?

\begin{lem}
    On considère $\phi$ une formule de la logique régulière sur l'alphabet
    $\Sigma$.  Il est possible d'écrire $\phi$ de manière logiquement
    équivalente sous forme d'une conjonction d'atomes, avec toutes les
    existentielles en tête et sans utiliser ni l'égalité, ni le faux (si la
    formule est différentes de juste la formule fausse).

    On appelle une telle écriture la forme normale de $\phi$.
\end{lem}

\begin{pv} Induction sur la structure de la formule.
\end{pv}

On suppose désormais que toutes les formules sont sous forme normale.

\begin{defi}{Variables}
    On note $\V(\phi)$ l'ensemble des variables d'une formule.
\end{defi}

\begin{rem}
    Soient $\phi$ et $\psi$ deux formules. On dit que $\phi$ est une sous-formule
    de $\psi$ si l'on peut associer chaque atome de $\phi$ à un atome de $\psi$, de
    manière injective et de façon que si des variables sont égales au depart, elles
    le sont à l'arrivée (les variables de $\phi$ sont \emph{plus libres} que celles
    de $\psi$).

    On dispose alors d'une assimilation des variables
    $\iota : \V(\phi)\rightarrow \V(\psi)$ qui donne l'envoi des variables de $\phi$
    dans celle de $\psi$ selon l'assimilation des atomes.
\end{rem}

\begin{defi}{Représentation catégorique}
    Soit $\phi$ une formule. On définit $[\phi]\in\C_\Sigma$ comme le couple $(r,\alpha)$
    où $r$ compte les occurences des atomes dans $\phi$ et $\alpha$ regroupe les
    emplacements qui correspondent aux même variables dans $\phi$.
\end{defi}

On va montrer que cette représentation contient toute l'information qui nous intéresse.

\begin{lem}
    Soit $\phi$ une formule.

    Alors il existe une bijection naturelle entre $\C_\Sigma(\star, [\phi])$ et
    $\V(\phi)$.
\end{lem}

\begin{defi}{Variable associée}
    Soit $\phi$ une formule.

    Soit $v\in\C_\Sigma(\star, [\phi])$. On note $v^*\in\V(\phi)$ la variable qui
    lui est associée par la bijection définie ci-dessus.

    Réciproquement, pour $x\in\V(\phi)$, on note $[x]\in\C_\Sigma(\star, [\phi])$
    la flèche qui lui est associée par la bijection ci-dessus.
\end{defi}

\begin{lem}\label{concretCompIff}
    Soient $\phi$ et $\psi$ deux formules telles que $[\phi] = [\psi]$.

    Alors $\vdash \phi\iff\psi$
\end{lem}

\begin{lem}\label{varAlongSub}
    Soient $\phi$ et $\psi$ deux formules.
    
    Si $\phi$ est une sous-formule de $\psi$ avec $\iota$ l'assimilation de
    variables associée, alors il existe $f\in\C_\Sigma([\phi], [\psi])$ telle
    que le diagramme suivant commute~:

    \[\begin{tikzcd}
        \C_\Sigma(\star,[\phi]) \arrow[d, "f"] & \V(\phi) \arrow[d, "\iota"]
                                                          \arrow[l, "\brk{.}"] \\
        \C_\Sigma(\star,[\psi]) \arrow[r, ".^*"] & \V(\psi)
    \end{tikzcd}\]

    Réciproquement, pour chaque $f\in\C([\phi], [\psi])$ on peut montrer que $\phi$ est
    une sous formule de $\psi$ de façon à avoir l'égalité ci-dessus.
\end{lem}

\begin{defi}{Assimilation associée}
    Soit $f\in\C_\Sigma([\phi],[\psi])$. On note $f^*$ la fonction de $\V(\phi)$ dans
    $\V(\psi)$ donnée par le lemme ci-dessus.
\end{defi}

\begin{lem}\label{abstractExists}
    Soit $(r,\alpha)\in\C_\Sigma$.

    Alors il existe une formule $\phi$ telle que $[\phi] = (r,\alpha)$.
\end{lem}

Les lemmes ci-dessus montrent donc que $\C_\Sigma$ capture parfaitement la notion de
sous-formule et celle de variable. On assimilera désormais le $\iota$ avec le $f$ du
lemme ci-dessus lorsque l'on parlera de sous-formule.

\begin{defi}{Concrétisation}
    Soit $(r,\alpha)\in\C_\Sigma$.

    On note $\phi_{(r,\alpha)}$ une formule telle que $[\phi_{(r,\alpha)}] = (r,\alpha)$.
    C'est toujours possible d'après le lemme \ref{abstractExists} et le choix n'est
    pas important puisque toutes les formules sont équivalentes d'après le lemme
    \ref{concretCompIff}.
\end{defi}

\subsection{Structure de site}

\begin{defi}{Site}
    Soit $\C$ une catégorie quelconque. On donne, pour
    chaque $c\in\C$, d'un ensemble de familles $(f_i : c_i\rightarrow c)_{i\in I}$,
    dites couvrantes, telles que~:

    \begin{align*}
        \forall c\in\C, & \forall (f_i)_{i\in I} \text{ couvrante de } c,
          \forall h : d\rightarrow c, \exists (g_j)_{j\in J} \text{ couvrante de } d, \\
        & \forall j\in J, \exists i\in I,
          \begin{tikzcd}[ampersand replacement=\&]
            d \arrow[r, "h"] \& c \\
            g_j \arrow[u, "g_j"] \arrow[r, dotted] \& c_i \arrow[u, "f_i"] \\
          \end{tikzcd}
    \end{align*}

    La catégorie $\C$ munie de ces familles est appellée un \emph{site}.
\end{defi}

L'intuition est de définir une notion de recouvrement d'objets de $\C$ par des morphismes.
Cela permet de définir une notion de localité sur les objets de $\C$, sans pour autant
avoir de foncteur d'oubli vers $\Set$ et de topologie. Cela permet de définir des
faisceaux, qui sont intuitivement une manière d'associer une collection d'objets à
chaque objet de $\C$ qui soit essentiellement locale.

\begin{defi}{Famille cohérente}
    Soit $\C$ un site et $F : \C^{\text{op}}\rightarrow\Set$ un préfaisceau sur
    $\C$. Soit $c\in\C$ et $(f_i)_{i\in I}$ une famille couvrante de $c$.
    
    Soit $(a_i)_{i\in I}\in \Pi_{i\in I} Fc_i$. $(a_i)$ est dite \emph{cohérente} si~:

    \[\forall i,j\in I, \forall f : d\rightarrow c_i, \forall h : d\rightarrow c_j,
      \begin{tikzcd}
          d \arrow[r, "g"] \arrow[d, "h"] & c_i \arrow[d, "f_i"] \\
          c_j \arrow[r, "f_j"] & c \\
      \end{tikzcd}
      \implies Fg(a_i) = Fh(a_j) \]
\end{defi}

Si l'on pense une famille couvrante comme une notion de localité, une famille cohérente
est une information locale sur un objet $Fc$.

\begin{defi}{Faisceau}
    Un faisceau sur $\C$ un site est un préfaisceau sur $\C$ tel que~:

    \begin{align*}
        \forall c\in\C, & \forall (f_i)_{i\in I}\text{ couvrante de } c, \\
                        & \forall (a_i)_{i\in I}\in\Pi_{i\in I}Fc_i \text{ cohérente}, \\
                        & \exists ! a\in Fc, \forall i\in I, Ff_i(a) = a_i
    \end{align*}
\end{defi}

La condition de faisceau confirme l'intuition~: elle nous dit que l'information locale
correspont bien à un objet de $Fc$. Sans cette condition on ne pourrait pas nécessairement
obtenir l'existence d'un objet à partir d'une description locale.

Pourquoi s'intéresser à ça ? Parce que l'objectif est de montrer que les CSP
sur un alphabet de relation $\Sigma$ sont les faisceau sur la catégorie
$\C_\Sigma$, où $F[\phi]$ contient des témoins de satisfiabilité de $\phi$. La
construction de $\C_\Sigma$ et la condition de fonctorialité nous permettrons
de dire que chaque élément de $F[\phi]$ correspond bien à une solution de
$\phi$, mais ce n'est pas suffisant pour obtenir que $F[\phi]$ contient des
témoins pour toutes les solutions. Pour cela, il faut montrer que l'on peut
construire une solution de $\phi$ à partir de ses constituants~: c'est ce que
la condition de faisceau va nous donner.

On veut donc définir une notion de recouvrement sur $\C_\Sigma$. L'idée est
qu'un recouvrement d'une formule doit être suffisant pour obtenir toutes les
solutions de cette formule. Il faut donc avoir les solutions de chaque formule
atomique, directement ou via une formule plus compliqué. On va maintenant
formaliser ça, la preuve que ça fonctionne sera donnée dans la section
suivante.

\begin{defi}{Recouvrement d'une formule}
    Soit $(r,\alpha)$ une formule dans $\C_\Sigma$. Soit un $(f_i)_{i\in I}$ un ensemble
    de morphismes de formules de $\C_\Sigma$ (ne contient donc pas de flèche depuis
    $\star$). $(f_i)$ est dit \emph{couvrante} si~:

    \[ \bigcup_{i\in I} \im f_i = r \]

    Où l'image de $f$ est le $n$-uplet des images des fonctions constituantes et
    l'union est prise terme à terme.
\end{defi}

Cette définition revient exactement à dire que chaque formule atomique de la formule est
présente dans au moins une des formule du recouvrement.

\begin{defi}{Site sur $\C_\sigma$}
    On munit $\C_\Sigma$ d'une structure de site en lui donnant, pour chaque formule,
    tous les recouvrements définis tels que précédemment, et pour $\star$ le recouvrement
    $(\id_\star)$.
\end{defi}

Il faut prouver que cette définition donne bien un site. C'est l'objectif du
lemme suivant.

\begin{rem}
    Soit $(r,\alpha)$ une formule de $\C_\Sigma$. Alors cette formule possède un
    recouvrement constitué uniquement de formules atomiques avec une relation d'équivalence
    triviale. On appelle ce recouvrement le \emph{recouvrement fondamental}
    (il est unique à permutation de la famille près).
\end{rem}

\begin{lem}
    Cette définition est bien un site.
\end{lem}

\begin{pv}
    Traitons d'abords le cas de $\star$. Comme il existe une seule flèche
    entrante en $\star$, son identité, et un seul recouvrement, la propriété de
    site est immédiatement vraie.

    Soit $(r,\alpha)$ une formule et $(f_i)_{i\in I}$ un recouvrement de cette formule.
    
    Soit $h$ un morphisme de $(r', \alpha')$ dans $(r,\alpha)$. On prend
    $(g_j)_{j\in J}$ le recouvrement fondamental de $(r', \alpha')$. Soit $j\in
    J$. On a que $h\circ g_j$ est l'une des sous-formules atomiques de
    $(r,\alpha)$. Par définition d'un recouvrement, on a $i\in I$ tel que $f_j$
    identifie une sous-formule de $(r,\alpha)$ contenant la sous-formule
    atomique considérée. Le morphisme qui envoie cette formule atomique dans le
    départ de $f_j$ fait alors commuter le carré voulu.

    Soit $v$ un morphisme de $\star$ dans $(r,\alpha)$, autrement dit une
    variable de $(r,\alpha)$.  Cette variable apparait nécessairement dans une
    sous-formule du recouvrement. En prenant le morphisme depuis $\star$ vers
    cette sous-formule qui identifie l'une des variables qui est ensuite
    envoyée sur $v$, on fait commuter le carré voulu.
\end{pv}

\subsection{Correction de la définition}

\subsubsection{Tout CSP est un faisceau}

% TODO idéalement la définition de CSP viendra de la partie 1
\begin{defi}{CSP}
    Un CSP est une sémantique finie pour la logique régulière sur un alphabet de formules 
    $\Sigma = \{R_1, \dots R_n\}$. Concrètement, cela consiste en un domaine $D$ qui est
    un ensemble fini, et pour chaque $1\leq i\leq n$ une relation $\sem{R_i}$
    d'arité $a_i$ sur $D$.
\end{defi}

\begin{rem}
    Un relation d'arité $k$ sur $D$ peut être vue comme un ensemble de $k$-uplets
    d'éléments de $D$. De plus, un $k$-uplet d'éléments de $D$ est une fonction de
    $k$ dans $D$. Or ici on demande un $k$-uplet parce qu'on a une énumération canonique
    des variables de la formule, dans le cas où c'est un atome, ce qui n'est pas vrai
    dans le cas général. On va donc plutôt considérer des fonctions des variables de
    la formule dans $D$. On aura alors~:

    \[ \sem{\phi}\subseteq \fns(\V(\phi), D) \]
\end{rem}

\begin{defi}{Extension de domaine}
    Étant donné deux ensembles de variables $V_1$ et $V_2$ avec une fonction
    $\iota : V_1 \rightarrow V_2$ et une partie $E\subseteq\fns(V_1, D)$. On peut définir
    l'extension de $E$ par rapport à $\iota$ de la façon suivante~:

    \[ \ext_\iota(E) = \{\mathbf{x}\in\fns(V_2,D)
                        | \exists \mathbf{y}\in E, \mathbf{x}\circ\iota = \mathbf{y} \} \]
\end{defi}

Intuitivement, cela correspond à rajouter des variables qui n'apparaissent pas dans une
formule à sa sémantique. On dispose alors d'un moyen de définir la sémantique d'une
formule à partir de ses formules atomiques.

\begin{defi}{Sémantique d'une formule}\label{cspSem}
    Soit $\psi$ une formule quelconque. $\psi$ est une conjonction d'atomes~:

    \[ \psi = \exists x_1,\exists x_2,\dots
                  R_{j_1}(\dots)\wedge\dots\wedge R_{j_k}(\dots) \]

    Alors pour $1\leq i\leq k$, on prend $f_i$ l'assimilation de
    $R_{j_i}(x_1, x_2, \dots)$ (toutes les variables doivent être distinctes) comme
    sous formule de $\psi$. Elle induit une fonction de $\V(R_{j_i}(x_1, x_2, \dots))$
    dans $\V(\psi)$ d'après le lemme \ref{varAlongSub}

    On pose alors~:

    \[ \sem{\psi} = \bigcap_{1\leq i\leq k} \ext_{f_i}(\sem{R_{j_i}(x_1, x_2\dots)}) \]
\end{defi}

\begin{lem}
    Soit $\psi$ une formule. Alors $\sem{\psi}$ correspond bien à la sémantique de
    $\psi$ comme formule conjonctive.
\end{lem}

% TODO A-t-on envie de prouver ça ? Ça impliquerait une définition plus détaillée de CSP

\begin{defi}{Faisceau de CSP}
    On pose $F\star = D$ et $F(r,\alpha) = \sem{\psi_{(r,\alpha)}}$.

    Soit $v\in\C_\Sigma(\star, (r,\alpha))$, on peut lui associer une variable
    $v^*$ de manière naturelle dans $\V(\psi_{(r,\alpha)})$ d'après le lemme 
    \ref{varAlongSub}. Alors on pose~:
    
    \[ Fv = \left\{\begin{array}{ccc}
                       \sem{\psi_{(r,\alpha)}} & \rightarrow & D              \\
                             \mathbf{x}        & \mapsto     & \mathbf{x}(v^*) \\
    \end{array}\right.\]

    Soit $f\in\C_\Sigma((r,\alpha), (r',\alpha'))$. $f$ induit une fonction
    $f^* : \V(\psi_{(r,\alpha)})\rightarrow\V(\psi_{(r',\alpha')})$. On pose alors~:

    \[ Ff = \left\{\begin{array}{ccc}
                    \sem{\psi_{(r',\alpha')}} & \rightarrow & \sem{\psi_{(r,\alpha)}} \\
                           \mathbf{x}         & \mapsto     & \mathbf{x} \circ f^* \\
    \end{array}\right.\]

    Enfin, on pose $F\id_\star = \id_D$.
\end{defi}

Vérifions que c'est bien un faisceau.

\begin{lem}
    $F$ tel que défini ci-dessus est un préfaisceau sur $\C_\Sigma$ vers $\fset$.
\end{lem}

\begin{pv}
    On vérifie immédiatement que $F\id_x = \id_{Fx}$.

    L'image d'une composition de morphismes de formules est immédiatement la composition
    des images.

    Enfin, soit $v\in\C_\Sigma(\star, (r,\alpha))$ et
    $f\in\C_\Sigma((r,\alpha), (r',\alpha'))$.

    Alors~:
    
    \[\begin{array}{rcll}
        F(f\circ v) & = & F(f(v)) & \\
                    & = & \mathbf{x}\mapsto \mathbf{x}((f(v))^*) 
                            & \text{par définition de F} \\
                    & = & \mathbf{x}\mapsto (\mathbf{x}\circ f^*)(v^*)
                            & \text{d'après le lemme \ref{varAlongSub}} \\
                    & = & Fv \circ Ff & \text{par définition de F} \\
    \end{array}\]
\end{pv}

Il faut alors vérifier la condition de faisceau.

\begin{lem}
    $F$ tel que définit ci-dessus est un faisceau sur $\C_\Sigma$ vers $\fset$.
\end{lem}

\begin{pv}
    D'après de lemme précédent $F$ est un préfaisceau. Il reste vérifier la condition
    de faisceau.

    Dans le cas de $\star$, le cas est immédiat~: l'unique recouvrement est $(\id_\star)$
    et les seules flèches entrantes de $\star$ sont $\id_\star$.

    Soit $(r,\alpha)\in\C_\Sigma$ une formule. Soit $(f_i : (r_i,
    \alpha_i)\rightarrow (r,R))_{i\in I}$ une famille couvrante de
    $(r,\alpha)$.  Soit $(\mathbf{x_i})\in\Pi_{i\in I} F(r_i,\alpha_i)$ une
    famille cohérente.

    On définit l'ensemble des candidats solutions~:

    \[\mathscr{S} := \{ \mathbf{x}\in F(r,R)
                      | \forall i\in I, \mathbf{x}\circ f_i^* = \mathbf{x_i} \} \]

    On a par définition que $\mathbf{x}\in\mathscr{S}$ si et seulement si
    $\forall i\in I, Ff_i(\mathbf{x}) = \mathbf{x_i}$. On veut donc montrer que
    $\mathscr{S}$ est singleton.

    Montrons d'abord qu'il est au plus singleton. Soient $\mathbf{x},
    \mathbf{y}\in\mathscr{S}$. Soit $v\in\C_\Sigma(\star,(r,\alpha))$.
    Par définition du site il existe $i\in I$ tel que $v$ se factorise
    par $f_i$~: $\exists v'\in\C_\Sigma(\star,(r_i,\alpha_i)), v = f_i\circ v'$.
    Alors~:
    
    \[\begin{array}{rcll}
        \mathbf{x}(v^*) & = & \mathbf{x}((f_i\circ v')^*)
                                 & \text{par choix de } i \\
                        & = & \mathbf{x}(f_i^*(v'^*))
                                 & \text{d'après le lemme \ref{varAlongSub}} \\
                        & = & \mathbf{x_i}(v'^*)
                                 & \text{par définition de }\mathscr{S}\\
                        & = & \mathbf{y}(f_i^*(v'^*))
                                 & \text{par définition de }\mathscr{S}\\
                        & = & \mathbf{y}(v^*) & \\
    \end{array}\]

    Donc $\mathbf{x} = \mathbf{y}$.

    Pour montrer que $\mathscr{S}$ est non vide, il va falloir utiliser la condition de
    cohérence des $(\mathbf{x_i})$. Soit $v\in\C(\star, (r,\alpha))$ et $i,j\in I$ tels
    que $v$ se factorise par $f_i$ et $f_j$, ie
    il existe $v_1\in\C(\star, (r_i,\alpha_i))$ et $v_2\in\C(\star, (r_j,\alpha_j))$ tels
    que~:
    
    \begin{equation}\label{fact} v = f_i\circ v_1 = f_j\circ v_2 \end{equation}
    
    Il suffit de vérifier que $\mathbf{x_i}(v_1^*) = \mathbf{x_j}(v_2^*)$.
    On a que $\mathbf{x_i}(v_1^*) = Fv_1(\mathbf{x_i})$ et
    $\mathbf{x_j}(v_2^*) = Fv_2(\mathbf{x_j})$ par définition de $F$. On obtient alors
    l'égalité cherchée en appliquant la propriété de cohérence des $(\mathbf{x_i})$
    au carré commutatif~:

    \[\begin{tikzcd}
        \star \arrow[r, "v_1"] \arrow[d, "v_2"] & (r_i,\alpha_i) \arrow[d, "f_i"] \\
        (r_j,\alpha_j) \arrow[r, "f_j"] & (r,R) \\
    \end{tikzcd}\]

    Ce carré commute bien d'après l'égalité \ref{fact}.
\end{pv}

\subsubsection{Tout faisceau est un CSP}

On veut maintenant montrer qu'il est possible d'associer un CSP à chaque faisceau. Soit
$F$ un faisceau de $\C_\Sigma$. On commence par définir la sémantique d'une formule
selon $F$.

\begin{defi}{Sémantique de faisceau}\label{shSem}
    Soit $\psi$ une formule. La sémantique de $\psi$ selon $F$ est alors~:

    \[ \sem{\psi}_F := \left\{ f:\begin{array}{ccc}
            \V(\psi) & \rightarrow & F\star \\
            v        & \mapsto     & F[v](x) \\
    \end{array}\Large|~x\in F[\psi] \right\}\]
\end{defi}

La donnée d'un CSP est la donnée d'un domaine et d'une sémantique des atomes.

\begin{defi}{CSP d'un faisceau}
    On note $\csp_F$ le CSP de domaine $F\star$ et qui donne à
    $R_i$ la sémantique $\sem{R_i(x_1, \dots x_{\ar(R_i)})}_F$.
\end{defi}

Techniquement, on vient bien de définir un CSP. Mais on remarque maintenant que l'on a
deux définitions de la sémantique d'une formule $\psi$~: on a la sémantique selon le
faisceau $\sem{\psi}_F$ et la sémantique selon le CSP associé au faisceau $\sem{\psi}$.
On aimerait que ces deux sémantiques soient les mêmes. C'est en effet le cas, et c'est pour
cela que l'on considère des faisceaux et pas juste des préfaisceaux (les définitions
ci-dessus marcheraient aussi avec juste un préfaisceau).

\begin{theo}{Correction de la sémantique de faisceau}\label{shSemCorrect}
    Pour toute formule $\psi$, $\sem{\psi}_F = \sem{\psi}$.
\end{theo}

\begin{pv}
    Soit $\psi$ une formule.
    Soient $(j_i)_{1\leq i\leq k}$ les indices des formules atomiques de $\psi$
    et $(f_i)$ les morphismes de sous-formule associés.

    On va procéder par double inclusion.

    $\boxed{\subseteq}$ Soit $\mathbb{x}\in\sem{\psi}_F$.  Pour montrer que
    $\mathbb{x}\in\sem{\psi}$, il suffit de montrer que $\forall 1\leq i\leq k,
    \mathbb{x}\in\ext_{f_i}(\sem{R_{j_i}(x_1,\dots)}_F)$.

    Soit $1\leq i\leq k$. $\mathbb{x}\in\ext_{f_i}(\sem{R_{j_i}(x_1,\dots
    x_{a_{j_i}})}_F)$ si et seulement si $\mathbb{x}\circ f_i^*\in\sem{R_{j_i}(x_1,\dots
    x_{a_{j_i}})}_F$. Soit $\mathbf{x}\in F[\psi]$ tel que
    $\mathbb{x} = x\mapsto F[x](\mathbf{x})$.
    Alors~:
    
    \[\begin{array}{rll}
        \mathbb{x}\circ f_i^*(v^*) &= F([f_i^*(v^*)])(\mathbf{x}) & \\
         &= F(f_i\circ v)(\mathbf{x})
             & \text{d'après le lemme \ref{varAlongSub}} \\
         &= (Fv\circ Ff_i)(\mathbf{x}) & \text{par fonctiorialité de } F\\
         &= Fv(Ff_i(\mathbf{x})) & \\
    \end{array}\]

    Donc $\mathbb{x}\circ f_i = x\mapsto F[x](\mathbf{y})$ 
    avec $\mathbf{y} = Ff_i(\mathbf{x})$, d'où le résultat.

    $\boxed{\supseteq}$ Soit $\mathbb{x}\in\sem{\psi}$. On note $(r_i,R_i)$ la
    représentation de $R_{j_i}(x_1,\dots x_{a_{j_i}})$ dans $\C_\Sigma$. On
    remarque $\mathbb{x}\circ f_i^*\in\sem{R_{j_i}(x_1,\dots x_{a_{j_i}})}$, donc il existe
    $\mathbf{x_i}\in F(r_i,R_i)$ tel que
    $\mathbb{x}\circ f_i^* = x\mapsto F[x](\mathbf{x_i})$. De plus, on remarque que
    $((r_i,\alpha_i))_{i\in I}$ est une famille couvrante de $[\phi]$. On va alors utiliser
    la propriété de faisceau pour construire un $\mathbf{x}\in F[\phi]$ tel que
    $\mathbb{x} = x\mapsto F[x](\mathbf{x})$.

    Commençons par vérifier que $(\mathbf{x_i})_{i\in I}$ est une famille cohérente. Soient
    $i,j\in I$, soit $c\in\C_\Sigma$ un formule, soient
    $g:c\rightarrow (r_i,\alpha_i)$
    et $h:c\rightarrow (r_j,\alpha_j)$ telles que le diagramme suivant commute~:

    \[\begin{tikzcd}
        c \arrow[r, "g"] \arrow[d, "h"] & (r_i,\alpha_i) \arrow[d, "f_i"] \\
          (r_j,\alpha_j) \arrow[r, "f_j"] & \brk{\phi} \\
    \end{tikzcd}\]

    On veut alors montrer que $Fg(\mathbf{x_i}) = Fh(\mathbf{x_j})$. Ce qui va
    permettre à la preuve de marcher est le fait que $(r_i,\alpha_i)$ et
    $(r_j,\alpha_j)$ représentent des atomes avec toutes leurs variables
    libres. Il y a donc deux cas à traiter.

    Soit $c = \star$, auquel cas $g$ et $h$ sont des variables, qui plongées dans 
    $[\phi]$ s'identifient à la même variable $v$. Donc~:
    
    \[\begin{array}{rcll}
        Fg(\mathbf{x_i}) & = & \mathbb{x}\circ f_i^*(g^*)
                             & \text{par définition de } \mathbf{x_i} \\
                         & = & \mathbb{x}((f_i\circ g)^*)
                             & \text{d'après le lemme \ref{varAlongSub} } \\
                         & = & \mathbb{x}((f_j\circ h)^*)
                             & \text{par condition de cohérence} \\
                         & = & Fh(\mathbf{x_j})
                             & \text{par définition de } \mathbf{x_j} \\
    \end{array}\]

    Sinon, on a $(r_i,\alpha_i) = (r_j,\alpha_j) = \phi$ et $g = h = \id_c$. Auquel cas le
    résultat est immédiat.

    On peut donc appliquer la propriété de faisceau à cette famille pour créer un
    $\mathbf{x}\in F[\phi]$ tel que
    $\forall 1\leq i\leq n, Ff_i(\mathbf{x}) = \mathbf{x_i}$. Alors on a, pour
    $v\in\C_\Sigma(\star,[\phi])$~:

    \[\begin{array}{rcll}
        \mathbb{x}(v^*) & = & \mathbb{x}((f_i\circ v')^*)
                                & \text{car $(f_i)$ est couvrante} \\
                        & = & \mathbb{x}\circ f_i^*(v'^*)
                                & \text{d'après le lemme \ref{varAlongSub}} \\
                        & = & Fv'(\mathbf{x_i})
                                & \text{par définition de }\mathbf{x_i}\\
                        & = & Fv'(Ff_i(\mathbf{x}))
                                & \text{par définition de }\mathbf{x} \\
                        & = & F(f_i\circ v')(\mathbf{x})
                                & \text{par fonctorialité} \\
                        & = & Fv(\mathbf{x}) & \\
    \end{array}\]

    Donc $\mathbb{x} = x\mapsto F[x](\mathbf{x})$, d'où $\mathbb{x}\in\sem{\psi}_F$.
\end{pv}

\subsection{Canonicité}

Une propriété que l'on aimerait avoir sur notre site est la \emph{canonicité}. Cette
notion est définie en annexe \ref{appCanon}, avec quelques résultats que nous allons
utiliser.

Plus précisément, on va utiliser le résultat \ref{caracCanon} pour déterminer si
$\C_\Sigma$ est canonique.

Un problème apparaît alors ! Considérons la formule $\phi=R(x)\wedge R(y)\wedge S(z)$
recouverte par $f:R(x)\rightarrow\phi$ qui identifie le premier atome et
$g:R(x)\wedge S(y)\rightarrow\phi$ qui identifie le reste de la formule. Le diagramme
des spans contient uniquement $R(x)$ et $R(x)\wedge S(y)$ et aucune flèche. La
condition ci-dessus voudrait donc que $\phi$ soit le produit de ces deux formules dans
$\C_\Sigma$. Or on a le diagramme suivant~:

\[\begin{tikzcd}
    R(x) \arrow[r, "f"] \arrow[rd] & \phi \arrow[d, red] \\
    R(x)\wedge S(y) \arrow[ru, near end, "g"] \arrow[r] & R(x)\wedge S(y) \\
\end{tikzcd}\]

La flèche rouge est impossible puisque $R(x)\wedge S(y)$ a strictement moins d'atomes
que $\phi$. Ce recouvrement n'est donc pas effectif polymorphique~: $\C_\Sigma$ n'est pas
sous canonique~!

On pourrait manuellement essayer de corriger ça en modifiant les définitions, mais ce
serait fastidieux et pas trivial du tout. C'est cet échec qui nous a amené à changer
notre approche, et à utiliser celle présentée dans la section \ref{secCat}.