Injections dans les topos
Dans un livre essentiellement consacré aux topos, on trouve en appendice la définition de morphisme $I$-injectif: un morphisme $f: X \to Y$ est $I$-injectif si, pour tous morphismes $x_1, x_2: I \to X$ tels que $f \circ x_1 = f \circ x_2$, on a $x_1 = x_2$.
Cette définition n'est pas vraiment motivée (elle n'est jamais utilisée). Elle permet de reformuler la notion d'injection (ou de monomorphisme) en disant que c'est un morphisme I-injectif pour tout I et on peut montrer que si on a une classe $\mathcal{C}$ séparante, alors il suffit que $f$ soit $I$-injectif pour tout $I \in \mathcal{C}$ pour que $f$ soit un monomorphisme.
Je me demandais s'il y avait une signification "profonde". Ca me fait en effet penser à la sémantique de Kripke-Joyal (d'ailleurs, c'est pour ça que j'ai légèrement reformulé ainsi la définition du livre, lequel utilise explicitement le connecteur $\Rightarrow$): $f$ est $I$-injectif ssi, pour tous $x_1, x_2: I \to X$ tels que $I$ force $f \circ x_1 = f \circ x_2$, on a que $I$ force $x_1 = x_2$ (ce qui est plus faible que: pour tous $x_1, x_2: I \to X$, on a que $I$ force $(f \circ x_1 = f \circ x_2 \Rightarrow x_1 = x_2)$ - c'est pour ça que j'ai enlevé l'implication). On a une inclusion externe: $\{ (x_1, x_2) \in \mathsf{Hom}(I, X)^2 \: \vert \: f \circ x_1 = f \circ x_2 \} \subseteq \{ (x_1, x_2) \in \mathsf{Hom}(I, X)^2 \: \vert \: x_1 = x_2 \}$. Ce type d'inclusion externe a-t-il une "signification"? Peut-on l'internaliser? S'exprime-t-elle dans la sémantique de Kripke-Joyal?
J'ai bien conscience que ma question est un peu floue, mais je m'étonne que les auteurs aient pris la peine de rajouter cette définition en appendice s'il n'y avait pas de sérieuses motivations pour l'introduire.
Cette définition n'est pas vraiment motivée (elle n'est jamais utilisée). Elle permet de reformuler la notion d'injection (ou de monomorphisme) en disant que c'est un morphisme I-injectif pour tout I et on peut montrer que si on a une classe $\mathcal{C}$ séparante, alors il suffit que $f$ soit $I$-injectif pour tout $I \in \mathcal{C}$ pour que $f$ soit un monomorphisme.
Je me demandais s'il y avait une signification "profonde". Ca me fait en effet penser à la sémantique de Kripke-Joyal (d'ailleurs, c'est pour ça que j'ai légèrement reformulé ainsi la définition du livre, lequel utilise explicitement le connecteur $\Rightarrow$): $f$ est $I$-injectif ssi, pour tous $x_1, x_2: I \to X$ tels que $I$ force $f \circ x_1 = f \circ x_2$, on a que $I$ force $x_1 = x_2$ (ce qui est plus faible que: pour tous $x_1, x_2: I \to X$, on a que $I$ force $(f \circ x_1 = f \circ x_2 \Rightarrow x_1 = x_2)$ - c'est pour ça que j'ai enlevé l'implication). On a une inclusion externe: $\{ (x_1, x_2) \in \mathsf{Hom}(I, X)^2 \: \vert \: f \circ x_1 = f \circ x_2 \} \subseteq \{ (x_1, x_2) \in \mathsf{Hom}(I, X)^2 \: \vert \: x_1 = x_2 \}$. Ce type d'inclusion externe a-t-il une "signification"? Peut-on l'internaliser? S'exprime-t-elle dans la sémantique de Kripke-Joyal?
J'ai bien conscience que ma question est un peu floue, mais je m'étonne que les auteurs aient pris la peine de rajouter cette définition en appendice s'il n'y avait pas de sérieuses motivations pour l'introduire.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Ce que je veux dire c'est qu'il n'y a pas de raison qu'il y ait d'interprétation, puisque l'information que tu veux interpréter est "globale" (relativement à $I$, mais il est fixé donc je me permets de dire "global"), alors que Kripke-Joyal c'est local.
Donc j'ai pas de réponse définitive à t'apporter (de "non" affirmatif :-D ) parce que je ne m'y connais pas assez; mais je serais partisan d'un "non" (s'il y avait des partis à avoir)
Avec un peu de chance, GBZM passera par là et nous expliquera pourquoi je raconte n'importe quoi et qu'il y a une interprétation interne (ou donnera une meilleure justification à pourquoi "non")
Par exemple, (en notant $S$ le topos) est-ce que ça dit quelque chose du morphisme $I \times f$ de $\pi_1: I \times X \to I$ vers $\pi_1: I \times Y \to I$ dans le "slice" topos $S/I$?
A nouveau, en termes de local vs global, ça nous dit que $I\times f$ est "injective sur les sections globales" (je rappelle que dans un topos $Sh(X)$, les morphismes $1\to F$ sont précisément les sections globales $F(X)$) - et donc la différence entre ça et un monomorphisme est exactement une question de localité.
Evidemment "injectif sur les points" ne s'interprète pas dans Kripke-Joyal comme "$\forall x, y : 1\to X, f\circ x = f\circ y \implies x= y$", ce serait trop beau.
Je pense que ça suggère une motivation éventuelle de la définition : si tu remplaces $I$ par la classe $\mathcal C$ des sous-objets de $1$, ça te donne peut-être quelque chose ?
(ou des sous-objets de $I$, si tu veux une interprétation relative à $I$)
Mais si on prend par exemple le topos des $G$-ensembles ($G$ un groupe), l'objet terminal est le singleton avec l'unique action possible de $G$, qui n'a pour sous-objet autre que lui-même que le vide. Les sous-objets de $1$ ne voient donc pas grand chose des $G$-ensembles : juste les points fixes.
Je ne vois pas de formule du langage interne (dont la valeur de vérité serait un sous-objet de 1) qui voudrait dire "f est injectif sur les points".
edit: Je viens de me rendre compte pourquoi ça n'a pas de sens!
Si ça ne vous prends que quelques instants de (je ne connais pas les notations avec des slash)??
Pour la notation, si tu fais allusion à mon $\varphi(f/h)$, j'ai juste voulu indiquer la formule $\varphi$ dans laquelle $f$ remplace la variable $h$.
- la formule est satisfaite dans le monde déterminé par $I$;
- la formule est forcée par $I$.
La seconde relation est ce qui est souvent appelée "la sémantique de Kripke-Joyal", mais je ne trouve pas mention de la première - ça a pourtant bien un sens, non?
edit: $p$ -> $I$, comme signalé par GaBuZoMeu
Ètant donné une formule $\phi$ de $\mathcal L$, tu peux l'interpréter dans la structure $S$ ou dans la structure ensembliste $\mathrm{Hom}_E(I,S)$ pour chaque $I$. La sémantique de Kripke-Joyal est un "forcing" qui te permet de récupérer la première à partir de la collection des secondes.
Petite question : le $p$ dans ton message, c'est $I$, non ?
Parmi les structures $\mathrm{Hom}_E(I,S)$, tu as la structure "sections globales" $\mathrm{Hom}_E(1,S)$. Et $\mathrm{Hom}_E(I,S)$ est la structure "sections globales" de $S\times I\to I$ dans le topos $E/I$.
Les structures sections globales, je pense qu'on en parle tout de même. Par exemple, pour les problèmes de représentation : du genre, représenter un anneau avec certaines propriétés comme anneau des sections globales d'un espace annelé (ou d'un topos annelé) en anneaux avec des propriétés plus riches (anneau commutatif/anneau local, anneau commutatif von Neumann régulier/corps ....).
Oui, je corrige mon message pour qu'il soit plus compréhensible.
Le fait que $f$ est injective sur les points est alors l'interprétation de la formule $(\forall x, y: X) (f \circ x = f \circ y \Rightarrow x = y)$ dans la structure $Hom_E(1, S)$ des sections globales (où $S$ est le langage interne de $E$).
On parle de "sémantique externe" pour la sémantique de Kripke-Joyal, mais ça me semblerait plus approprié pour celle dans les les $Hom_E(I, S)$. Ceci étant dit, j'ai cherché un exemple où l'on aurait que $f$ est injective sur les points sans avoir $1$ force $(f \circ x = f \circ y \Rightarrow x = y)$ pour tous $x, y: 1 \to X$ (pour bien comprendre la différence), je n'y suis pas arrivé.
Je prends par exemple $E= Sh(S^1)$, et $X =$ le faisceau des sections de $\R\to S^1$ (qui correspond à l'espace étale...$p: \R\to S^1$ :-D). Il n'a pas de points, donc évidemment toute flèche qui en part est injective sur les points. Mais prenons par exemple $Y =$ le faisceau des sections de $S^1\overset{2}\to S^1$ (même blabla sur l'espace étale - je vais appeler la projection $f$ pour la suite), et $X\to Y$ l'unique flèche de revêtements qui envoie $0$ sur $1$ disons.
Alors cette flèche n'est pas un monomorphisme : je prends un petit ouvert connexe $U$ de $S^1$ tel que $f^{-1}(U) = V_0\sqcup V_1$ avec chaque $f_{\mid V_i}: V_i\to U$ un homéomorphisme; et $p^{-1}(U) = \sqcup_{n\in \Z} W_n$, avec chaque $p_{\mid W_n} : W_n\to U$ des homéomorphismes aussi. Alors $\Gamma(X,U) \cong \Z$ et $\Gamma(Y,U) \cong 2$, donc naturellement la flèche $X(U)\to Y(U)$ n'est pas injective.
Bon, pour trouver une contre-exemple écrivons simplement les choses :
Que $1$ force ça, ça veut dire que pour tout $s: U\to 1$, si $U$ force $f\circ x \circ s = f\circ y \circ s$, alors $x\circ s = y\circ s$.
Bon, quitte à remplacer $s$ par l'inclusion de son image, on peut supposer que $U$ est un sous-objet de $1$.
Plaçons-nous par défaut pour notre contre-exemple dans un topos de faisceaux $Sh(X)$ (je changerai du coup tes notations $ f:\mathcal{F\to G}$). Je rappelle que dans ce cas-là un sous-objet de $1$, c'est exactement un ouvert de $X$. Donc on cherche $f$ telle que $f_X : \mathcal F(X)\to \mathcal G(X)$ est injective, mais qu'il existe un ouvert $U$ et des sections globales $x,y$ dont la restriction à $U$ vérifie $f_U(x_{\mid U}) = f_U(y_{\mid U})$, sans pour autant que $x_{\mid U} = y_{\mid U}$
Je vais prendre un exemple un peu pathologique, mais bon, il donne un truc. Je prends pour espace $X=\mathbb N$ muni de la topologie dont les ouverts sont $\emptyset$ et les $[n,+\infty[, n\in \mathbb N$; je prends pour $\mathcal F$ le faisceau qui vaut $2$ sur tout ouvert sauf $\emptyset$, avec les restrictions égales à l'identité; et pour $\mathcal G$ le faisceau qui vaut $2$ en $\mathbb N$, et $1$ partout ailleurs.
Il est facile de vérifier que c'est des faisceaux (il y a pas beaucoup de recouvrements d'ouverts !) ; de plus on a un morphisme évident $f:\mathcal{F\to G}$ qui est l'identité en $X$, et l'unique morphisme en $U\neq X$. En particulier, si je prends $x,y$ les deux sections globales de $\mathcal F$, on a bien que $[1,+\infty[$ force $f\circ x = f\circ y$ sans forcer $x=y$; pourtant $f_X$ est injective.
N'hésite pas à me dire si je raconte encore n'importe quoi mais là ça m'a l'air d'aller
Le $F$ de Maxtimax raccourci est $\mathrm{Id}_2 : 2\to 2$, le $G$ est $2\to 1$ et $f$ est $(\mathrm{Id}_2 , 2\to 1)$.
$x$ est $(0,0)$ et $y$ est $(1,1)$. Donc $fx=(0,0)$ et $fy=(1,0)$.
La valeur de vérité de $x=y$ est $0\to 0$, celle de $fx=fy$ est $0\to 1$. Donc la valeur de vérité de $fx=fy \implies x=y$ est $0\to 0$ (le faux).
C'est juste que c'est l'exemple pathologique que je prends en général pour construire des contre-exemples avec des faisceaux :-D
Le document de GBZM si tu peux le retrouver donnait une définition; sinon si tu ne l'as pas tu peux aussi regarder ici (de la slide 14 à la slide 20) qui donne une définition des formules et du forcing, dans le cadre un peu plus simple d'un topos de faisceaux (il a juste oublié $\forall$ :-S mais si tu as une question à ce sujet on pourra répondre)
Je ne comprends vraiment pas pourquoi on va s’embarrasser de topos et de toute cette usine à gaz alors que ce truc définit tout d'un coup. Quand je pense aux dizaines d'heures que j'ai dû gâcher à tenter de traduire dans ma perception ce qu'étaient les topos et tout le tutti quanti :-X
Gros MERCI à toi max!!
En plus, je trouve ça vraiment rigolo. Quand je pense au pauvre Martial qui va devoir se coltiner tous les évitements des $\int(adh(U)) \setminus U$ pour garder la logique classique à son cours de M2.
+ les topos sont des catégories très sympathiques qu'on utilise pour d'autres raisons (géométrie algébrique), et donc avoir un point de vue algébrique peut être utile à cet égard
Mais je suis d'accord que jusqu'à voir ce document j'ai toujours eu une perception un peu biaisée de la description de la sémantique de Kripke-Joyal (je pense que la première fois que j'ai vu le poly de GBZM, je n'étais pas encore prêt pour comprendre ce qu'il y avait dedans, même si en m'y replongeant récemment je me suis rendu compte qu'il disait la même chose)
Mais du coup (pour que tu saches) on peut définir une sémantique (qui se spécialise en celle-ci pour les topos de faisceaux) pour tout topos.
On manque, dans nos réseaux scientifiques du métier "interprétariat" qui fournirait des pros de même nature que les diplomates ont dans leurs bâtiments de réunion. Mais évidemment, on n'a pas les mêmes crédits que les chefs d'état :-D
non, ça pour moi, c'est "gratuit", je pourrai même écrire à la volée un cours pour le faire. J'ai bien compris que ce n'est pas le "topologique" qui compte mais l'ordre (donc le catégorique: une catégorie n'est qu'un ordre dont on a multiplié et coloré en différentes couleur l'ancienne flèche qui annonçait $x\leq y$.
Mais du coup, j'ai deux questions:
1/ Dans la géométrie synthétique (le livre lien à l'edit), on utilise quel "poset"?
2/ Ca me revient, un jour tu avais dit à quelqu'un sur le forum qu'on pouvait construire des modèles où tout est récursif. J'avais dû laissé passer voyant ça comme "des encouragements publicitaires pas bien méchants à la personne destinataire pour qu'elle travaille pluss sur le sujet". Je n'ai jamais entendu personnellement parler de ce genre de structure (en tant que logicien qui n'a pas bouffé depuis des décennies à des cantines de collègues non ensemblistes en plein travail, donc c'est très peu significatif), du moins qui soit "efficiente". Mais du coup, ce que tu dis est que tu as entendu parler de ça par le présent paradigme et non que tu l'as lu dans je ne sais moi "un article de pour la science écrit par Delahaye"?
0/ Non mais ce que je voulais dire c'est que ce n'est même pas juste une définition qui marche pour les faisceaux sur un site (ou un ensemble ordonné, whatever) : les topos les plus généraux ne sont pas forcément de cette forme là ! Mais après peut-être que tu saurais quand même t'en sortir.
1/ Si par géométrie synthétique tu entends la même chose que moi, je ne sais plus exactement, mais on prend une catégorie qui est liée à celle des variétés différentielles (je viens de jeter un oeil et apparemment il y a aussi un truc comme les algèbres de Weil qui apparait; j'avoue que je n'ai jamais regardé les détails).
2/ Oui oui j'ai entendu parler de ça, tu peux chercher les mots clés "topos effectif" (enfin tu auras sûrement plus de résultats en anglais : "effective topos") . C'est un exemple de ce que j'entendais par 0/ : ce n'est pas un topos de Grothendieck, donc en particulier on ne peut pas décrire sa logique interne si naïvement puisque tu n'as pas d' "ouverts" (ou d'ordre, ni même de catégorie) sur lequel te baser. Il faut travailler plus, d'où l'usine à gaz qu'on trouve dans les documents sur les topos en général.
(regarde par exemple le deuxième paragraphe dans "Idea" ici : il y a un théorème qui dit que dans la logique interne de ce topos "toute fonction $\N\to \N$ est récursive" est valide)
(ce document devrait contenir les énoncés voulus, mais je ne l'ai pas lu)
(finalement, tu peux aussi regarder ici, où Andrej Bauer explique comment faire de la calculabilité "synthétique", en se basant sur des axiomes qui sont en particulier vérifiés dans le topos effectif - notamment des trucs de type "tout est récursif")
(Même remarque pour Alesha : si ça te dérange, on pourra déplacer cette discussion !)
$$ (A\to := \{x\mid \forall y\in A: \in xy\in B\} $$
qui marche pour tous ces domaines (forcing, topos).
En fait, j'ai un peu simplifié la définition, puisque la réalité est:
$Agression(\forall xA(x)): = \{x\mid \exists y: x\in Agression(A(y))\}$
$Agression(A\to := \{ \sigma[x,s) \mid$ $s\in Agression(B) $ et $x\in Garanties(A)\}$
$Garanties(A) := \{x\mid \forall y \in Agression(A): \tau(x,y) \in Harmonie\}$
mais peu importe. On retrouve cette dualité "essentielle" dans à peu près toute la science, cela provient de ce que les preuves de science (à la différence d'autres domaines), doivent offrir des garanties matérielles.
Les cas platoniciens (ie internes aux maths, forcing, topos, mécanismes appliqués, etc) permettent souvent la dédualisation (où garantir veut dire agresser le contraire), et les cas les plus simples (les plus platoniciens), rendent $\tau$ souvent triviale*** (inf ou produit), ie associative (=triviale ici).
Je vais manger, mais je te mettrai un lien pour le livre géométrie synthétique, Poirot l'a trouvé récemment, et lirai tes liens. MERCIIII
*** ne pas confondre avec le sens habituel de ce mot.
J'ai quand même compris l'exemple donné par GaBuZoMeu où un morphisme $f: X \to Y$ est $1$-injectif (injectif sur les points) mais où $1$ ne force pas la formule $(f(x) = f(y) \Rightarrow x = y)$ pour tous $x, y: 1 \to X$.
J'aurais aimé comprendre ce qu'a écrit GaBuZoMeu ici:
Je n'ai pas osé demander car c'est "évident". Maxtimax a donné en lien un .pdf qui semble l'illustrer: Slide 21, $L$ est le langage des anneaux, $S$ est le faisceau d'anneaux sur $R$ qui associe avec chaque ouvert $U$ de $R$ l'anneau des fonctions continues de $U$ vers $R$; mais les topos ne sont introduits que plus tard, donc il n'y a pas de $E$ ici, donc je n'ai pas réussi à comprendre.
Pour tout objet $I$ de $E$, on a une $L$-structure ensembliste d'univers l'ensemble $\mathrm{Hom}_E(I,A)$ et où le symbole $0$ est interprété par $I\to 1\stackrel{0_A}\longrightarrow A$, etc. La collection de ces $L$-structures ensemblistes s'organise en fait en un préfaisceau sur $E$, c.-à-d. un foncteur contravariant de $E$ dans la catégorie des $L$-structures ensemblistes (il y a des problèmes de petite et grosse catégorie, mais passons).
C'est tout ce que je voulais dire, et l'abus de notation était de noter de la même façon la structure ensembliste et son univers.
Quelques compléments. Si $A$ est un anneau commutatif, alors tous les $\mathrm{Hom}_E(I,A)$ sont des anneaux commutatifs. Mais si $A$ est un anneau local (tout $I$ force $\forall x\ \exists y\ (x\times y=1 \vee (1-x)\times y=1)$ en plus des axiomes d'anneau commutatif), alors les $\mathrm{Hom}_E(I,A)$ ne sont pas en général des anneaux locaux.
Par contre, si $E$ est le topos des faisceaux sur un espace topologique $X$, on a une autre collection de structures ensemblistes induite par $A$ : les structures fibres $A_x$ pour tous point $x$ de $X$. Et là, $A$ est un anneau local si et seulement si toutes les fibres $A_x$ sont des anneaux locaux.
Ce que ça illustre c'est que la satisfaction des formules par chaque $Hom_E(I,A)$ est très différente de la satisfaction des formules par $A$ (à commencer par l'évident problème : $A$ ne satisfait pas forcément $p\lor \neg p$, alors qu'une structure ensembliste, si)
Alesha : je ne sais pas si c'est ça qui te gêne (je suis peut-être à côté de la plaque), mais le point de vue "un foncteur dans les $L$-structures c'est pareil qu'une $L$-structure dans les foncteurs" est essentiellement démarré (si je ne m'abuse) par Lawvere dans sa thèse Functorial semantics of algebraic theories. Au-delà d'être un plaisir à comprendre, si tu comprends ce cas de base ("un groupe dans $Fun(C,Ens)$ c'est un élément de $Fun(C,Grp)$"), tu comprendras tout ça immédiatement.
Je te conseille donc ladite thèse si c'est ça le point qui bloque (enfin je te la conseille de toute manière, mais si ce point là ne bloque pas, tu n'apprendras pas forcément grand chose)
J'avance lentement; GaBuZoMeu m'a donné plusieurs exercices:
Est-ce que c'est parce que la théorie est équationnelle? On a: si on a un modèle $A$ d'une théorie équationnelle $T$ dans un topos $E$, alors, pour tout objet $I$ de $E$, $\mathrm{Hom}_E(I,A)$ est un modèle ensembliste de $T$?
Cette définition d'anneau local dans un topos $E$, dans le cas où $E$ est le topos des ensembles, est équivalente à: $A$ est un anneau commutatif dans lequel il y a un unique idéal maximal? Ce qui est étonnant ici, c'est que cette définition quantifie sur tous les objets du topos alors que l'autre est de la forme: il existe un unique sous-ensemble de $A$ tel que...
Pour la seconde question, attention, GBZM a mis une quantification non bornée parce qu'il écrivait cette formule dans le langage de la théorie des anneaux, mais les quantifications sont en principe bornées : $\forall x\in A, \exists y \in A, ...$
L'équivalence entre ça et l'existence d'un unique idéal maximal se fait effectivement pour les ensembles; mais ça utilise l'axiome du choix (enfin cette propriété implique l'existence d'un unique idéal maximal, la réciproque utilise le théorème de Krull il me semble - en tout cas la preuve naïve y fait appel), donc ça ne marche pas dans un autre topos
Je pense que tu réponds à ta propre question juste après du coup.
Mais n'a-t-on pas que:
a) pour toute formule $\varphi$, $I$ force $\varphi$ implique que $Hom_E(I,E)$ satisfait $\varphi$?
b) pour toute formule $\varphi$ dont les variables sont de sorte $A$, $I$ force $\varphi$ implique que $Hom_E(I,A)$ satisfait $\varphi$?
b) Bah du coup non, comme on vient de le dire : prend $(X,O_X)$ un espace localement annelé (par exemple un anneau); alors dans $Sh(X)$, $X\Vdash \lceil O_X$ est un anneau local $\rceil$; mais pour autant $Hom_{Sh(X)}(h_X, O_X) = O_X(X)$ n'a aucune raison d'en être un - par exemple $Spec(A)$ avec $A$ non local (la raison est notamment que quand tu as un $\lor$ ou un $\exists$, dans la notion de forcing tu as le droit de prendre un recouvrement !! Dans $Hom_E(I,A)$, tu n'auras pas le droit, tu es coincé avec $I$, donc si ton $\exists$ est vrai avec des sections locales, mais aucune section globale, tu es bloqué)
$E$ est un topos donc un modèle $S$ de son langage interne. Pourquoi acceptes-tu la notation $Hom_E(I, A)$ quand $A$ est un anneau et pas la notation $Hom_E(I, E)$? L'interprétation d'une variable de type $A$ dans $Hom_E(I, E)$ est un morphisme de $I$ dans $A$.
Pour moi, ton intuition est parfaitement correcte. $[x$ est après $y]$ se note $y\leq x$ par contre assez souvent. Vue la définition de Max de "force", c'est bien cet ordre-là qui a été pris pour les espaces topologiques (et généralisations).
C'est d'ailleurs marrant car en forcing TDE, il y a de moins en moins de mondes "dans $p$" (à noter que $p$ doit être vu comme un ensemble de mondes et non une seul monde), et plus les $p$ sont petits, plus ils sont considérés comme "exigeants/ précieux, etc" bref tout ce que tu veux qui indique une valeur élevée.
Apparemment en toposerie intuitionniste, c'est TOTALEMENT inversé paradigmatiquement, on est sur des gens qui veulent recoller des trucs qui sont faciles localement et qui mènent des guerrillas contre le global difficile à recoller.
A moins que je ne fasse une lourde erreur, c'est tout de même assez génial cette belle opposition entre pôle sud et pôle nord.
C'est ce qui se passe habituellement dans les maths courantes.
-La catégorie des variétés diférentielles est triviale localement (ce sont juste des ouverts de $\R^d$ avec $d\geq 1$, on pourrait même se contenter de boules). Le passage au global fait apparaître une industrie pléthorique (cohomologie etc).
-La catégorie des schémas affines sur un anneau commutatif $k$ est juste l'opposée de la catégorie des $k$-algèbres. La catégorie des $k$-schémas plus généraux (qui en sont des recollements dans un sens à préciser) fait engendrer une science géante (géométrie algébrique depuis Grothendieck).
$Hom_E(I,A)$ est une $L$-structure classique, et quand tu interprètes disons $\varphi \lor \psi$, tu te demandes "est-ce que $\varphi$ est vraie dans $Hom_E(I,A)$ ou est-ce que $\psi$ est vraie dans $Hom_E(I,A)$ ?" : c'est beaucoup plus restrictif que de te demander "est-ce que je peux trouver 'un recouvrement' de $I$ tel que $\varphi$ est vraie sur l'une des parties de ce recouvrement, et $\psi$ vraie sur l'autre ?" : en particulier le fait que la réponse au second soit "oui" ne dit rien de la réponse au premier !!
Je prends un exemple plus simple que les espaces localement annelés, une variation sur un exemple que j'ai déjà donné sur le forum : tu prends $X= \{0,1\}$ muni de la topologie discrète, et dans $Sh(X)$ tu prends le faisceau constant $2$. Tu lui mets un ordre dessus : tu dis que $0\leq 1$ est vrai sur $\{0\}$ et $1\leq 0$ est vrai sur $\{1\}$. En particulier, $X\Vdash (\forall x, \forall y, x\leq y \lor y\leq x)$, précisément parce que tu peux trouver un recouvrement sur lequel ça marche ! Au contraire, si tu regardes $Hom_{Sh(X)}(h_X, 2)$, c'est un ensemble ordonné à quatre éléments $f: \{0,1\}\to \{0,1\}$ et par exemple $0\mapsto 0,1\mapsto 0$ et $0\mapsto 1, 1\mapsto 1$ sont incomparables dans cet ensemble ordonné, donc la formule n'y est pas valable.
Pour ta deuxième question: $A$ est un objet du topos $E$, donc $Hom_E(I,A)$ fait sens : c'est un hom-set du topos $E$ entre deux objets de $E$.
$E$ n'est pas un objet de $E$, donc $Hom_E(I,E)$ n'a pas de sens (qu'est-ce qu'un morphisme entre un objet d'une catégorie et cette catégorie elle-même ?)
Voici comment je vois les choses: Etant donné $p$, l'ensemble des formules $\varphi$ telles que $p$ force $\varphi$ détermine une théorie complète ("les formules vraies à $p$"): si $\gamma$ atomique est forcée par $p$, alors $\gamma$ est vraie, sinon $\gamma$ est fausse; la valeur de vérité sur les formules atomiques détermine la valeur de vérité sur l'ensemble des formules; je fais donc une distinction entre "$p$ force $\varphi$" et "$\varphi$ est vraie à $p$" (je ne suis pas sûr que ce soit standard).
On devrait avoir a que $p$ force $\varphi$ implique que $\varphi$ est vraie dans tout monde $q \geq p$.
Maintenant, étant donné un topos $E$ et un objet $I$ de $E$, on a:
- l'ensemble $A$ des formules $\varphi$ du langage interne de $E$ qui sont forcées par $I$;
- l'ensemble $B$ des formules $\varphi$ qui "sont vraies en $I$" (avec la définition que j'ai donnée au-dessus: on a forcément $\varphi$ est vraie ou $\neg \varphi$ est vraie pour tout $\varphi$);
- l'ensemble $C$ des formules $\varphi$ qui sont vraies dans ce que je notais $Hom_E(I, E)$ (tu peux choisir la notation qui te convient).
On a $A \subseteq B$. Je croyais qu'on avait $B = C$, mais tu me dis qu'on n'a même pas $A \subseteq C$, c'est bien ça? Y a-t-il un modèle canonique de $B$ (que j'imaginais être $Hom_E(I, E)$)?
Par exemple si je te donne une constante du langage interne de $E$ (donc un objet $x\in E$), comment il est interprété dans "$Hom_E(I,E)$" ? Ou bien tu te fixes une interprétation de ce langage dont les objets sont ceux de $I/E$ ?
"l'ensemble des formules $\varphi$ telles que $p$ force $\varphi$ forme une théorie complète" : je ne suis pas d'accord.
Il se peut très bien que $p$ ne force par exemple ni $\varphi$ ni $\neg \varphi$. ça se saurait si "$p$ force machin" était classique :-D (d'ailleurs même dans le bon vieux forcing à la Cohen ce n'est pas vrai !)
J'ai pas compris ta définition de "vraie en $p$" (ou en $I$), tu peux préciser ?
Sinon pour la suite, comme je n'ai pas compris ton $Hom_E(I,E)$, je ne peux pas répondre :-S
En forcing canal historique, personne n'en a strictement rien à f..tre des grands éléments du poset (c'est même $1_B$ pour tout dire, une fois qu'on passe à l'algèbre de Boole canoniquement attachée..
Du coup, ce qui aurait peut-être été mieux c'est d'appeler ça un "anti-forcing", pour bien signaler qu'on fait le chemin inverse.
Une variable de type $A$ est interprétée par un morphisme de $I$ dans $A$. Une constante de type $A \to B$ (c'est-à-dire un morphisme de $A$ vers $B$ dans $E$) est interprétée comme la fonction de $Hom_E(I, A)$ vers $Hom_E(I, $ qui envoie chaque $g$ vers $f \circ g$; une constante qui est un objet $A$ dans $E$ est interprétée par l'ensemble des morphismes de $I$ vers $A$.
C'est pour ça que je distingue "$\varphi$ est vraie en $p$" et "$p$ force $\varphi$" et que l'inclusion de l'ensemble des formules forcées en $p$ dans l'ensemble des formules vraies en $p$ peut être stricte.
Une fois que tu connais les valeurs de vérité pour les formules atomiques, l'extension à l'ensemble des formules se fait par induction: si tu connais la valeur de vérité de $P$ et de $Q$, tu as celle de $(P \Rightarrow Q)$, etc... La valeur de vérité pour les formules atomiques est: $\varphi$ est vraie en $p$ ssi elle est forcée en $p$.