Algèbre de Heyting et topoï

Pablo_de_retour · May 2019

Bonsoir à tous,

Comment montrer que pour tout espace $ X $, il existe un isomorphisme d'ensembles partiellement ordonnés ( En fait, un isomorphisme d'algèbres de Heyting ) comme suit :
$$ \mathcal{O} (X) \simeq \mathrm{Sub}_{ \mathrm{Sh} (X) } ( \mathrm{1} ) $$

- $ \mathrm{1} $ est le faisceau constant $ \mathrm{1} = \mathrm{Hom} ( - , X ) $ défini comme suit :
Pour tout espace $ X $, tout ouvert $ U $ de $ X $ détermine un préfaisceau $ \mathrm{Hom} ( - , U ) $ défini, pour tout ouvert $ V $ de $ X $, par,
$$ \mathrm{Hom} ( V , U ) = \begin{cases} 1 \ \ , \ \ \text{si} \ \ V \subset U \\ \emptyset \ \ , \ \ \text{sinon} \end{cases} $$
où $ 1 $ est l'ensemble à un élément unique.

- $ \mathcal{O} (X) $ est l'algèbre de Heyting formée des ouverts de $ X $.

Merci d'avance.

moduloP · May 2019

Salut,

Je tente un truc :

Si tu as un sous-faisceau $R$ de $\text{Hom}(\bullet,X)$, je pense qu'il faut regarder l'ouvert $U := \bigcup_{O \in \mathcal{O}_X \mid R(O)=1 } O $. Et voir que $\text{Hom}(\bullet,U) \simeq R$. Pour faire, ça et bien il faut regarder la valeur $R(U)$.

Comme $U$ est recouvert par les certains ouverts $O$ et que $R$ est un faisceau, il suffit de voir la compatibilité sur les intersection. Mais ici c'est simple, puisque si $R(O_1) = 1$ et $R(O_2)=1$ et bien $R(O_1 \cap O_2)=1$ (et donc la compatibilité est évidente). Bref $R(U) = 1$ et donc par Yoneda, tu as un morphisme $\text{Hom}(\bullet,U) \to R$. Il n'y a plus qu'a voir que c'est un isomorphisme, ce qui doit revenir à dire que si $R(V)=1$ alors $V \subset U$, ce qui est la définition de $U$. Donc, ton isomorphisme, c'est juste Yoneda qui te le donne.

Vérifie tous les détails car j'ai écrit vite fait en prenant mon café avant d'aller travailler :-D

Maxtimax · May 2019

ModuloP : tu as fini par te réconcilier avec Yoneda ? :-D

Pablo_de_retour · May 2019

Bonjour moduloP :

Merci pour la réponse. Je n'ai pas compris ta dernière affirmation lorsque tu dis que : l'isomorphisme $ \mathcal{O} (X) \simeq \mathrm{Sub}_{ \mathrm{Sh} (X) } ( \mathrm{1} ) $ n'est autre que l'application du lemme de Yoneda.
Yoneda, en toute généralité affirme que : $ \mathrm{Nat} ( h^X , G ) = G(X) $, ce qui n'est pas le cas pour l'isomorphisme : $ \mathcal{O} (X) \simeq \mathrm{Sub}_{ \mathrm{Sh} (X) } ( \mathrm{1} ) $. Ou bien, j'ai loupé quelques choses ?

Pablo_de_retour · May 2019

Tu voulais peut être affirmer que $ \mathrm{Hom} ( \bullet , U ) \simeq R $ est du à la représentabilité fonctorielle par $ U $ de $ R $, et non Yoneda. Yoneda, c'est autre chose, non ?

Maxtimax · May 2019

Relis le.message de moduloP, Pablo... Yoneda te fournit $\hom(-,U) \to R $ dont il est trivial de montrer que c'est un iso. "Dû à la représentabilité fonctorielle" : bah non, c'est pas dû à, c'est ça qu'on prouve

Pablo_de_retour · May 2019

D'accord. Merci Maxtimax.
Et comment montrer que la bijection établi par moduloP est un morphisme d'ensembles partiellement ordonnés ?
Merci d'avance.

edit :
On montre pour cela, que pour $ W \subset V $, le morphisme de faisceaux : $ \mathrm{Hom} ( \bullet , W ) \to \mathrm{Hom} ( \bullet , V ) $ est un morphisme injectif, c'est ça ? Comment le faire ?

edit :
Ah oui, c'est juste l'application du lemme de Yoneda : $ \mathrm{Hom} ( W,V ) \simeq \mathrm{Hom} ( h^W , h^V ) $. C'est à dire, si on choisit un morphism injectif dans $ \mathrm{Hom} ( W,V ) $ son élément correspondant dans $ \mathrm{Hom} ( h^W , h^V ) $ est injectif aussi. :-)

christophe c · May 2019

:-D à quand une loi pour écrire les maths en ligne, sans exposant ni indice ? :-D

Maxtimax · May 2019

Il n'y a pas de question d'injectivité ici Pablo.

Les $\hom(-,U)$ sont distincts et clairement ordonnés comme les $U$ : le seul point subtil était la surjectivité et c'est ce que moduloP établissait.

Christophe : je ne comprends pas ta remarque

christophe c · May 2019

Je blaguais. Je voulais dire que pour moi, c'est imbitable à cause du langage utilisé, que je ne parle pas. Mais en Espagne, je ne comprends rien non plus, ne parlant que très peu espagnol. Idem, une fois NoName et GBZM ont partagé, détendus, un argument diagrammatique qui rendait évident quelque chose, je n'ai pas pu en profiter, ne parlant pas leur langue.

Le multilinguisme est important, même en sciences. Mais ce n'est pas le sujet de ce fil. (Et je ne suis pas bon en langue par ADN j'ai l'impression).

christophe c · May 2019

Cela dit, pour faire semblant de rester dans le sujet, je peux signaler ce que je me rappelle de Yoneda (qui ne me passionne pas outre mesure, car s'occupe très exactement des choses que je dois éviter en tant qu'infinitiste):

La fonction $F1$ suivante va de $A$ dans $\prod X: ((A\to X)\to X)$ :

$$ a\mapsto [X\mapsto (f\mapsto f(a))]$$

La fonction $F2$ suivante va de $\prod X: ((A\to X)\to X)$ dans $A$ :

$$ \phi \mapsto \phi(A)(id) $$

Et modulo une hypothèse supplémentaire de commutativité qui dit qu'on ne regarde que les "naturelles", elles sont réciproques l'un de l'autre.

Comme tu t'en doutes, vue la taille de $\prod X: ((A\to X)\to X)$, ce ne sont pas les "fonctions naturelles" qui sont le plus passionnantes pour moi.

Jadis, quand tu n'étais pas encore inscrit sur le forum, j'avais même tapé le chti calcul, mais là, au taf, je serais bien en peine de le retrouver, même s'il est très formel.

christophe c · May 2019

Je chercherai à retrouver le lien éventuellement. Mais ça doit avoir au moins 3-4ans, je pense.

Pablo_de_retour · May 2019

De toute façon, moi, je ne suis pas d'origine espagnol. Je suis bien sûr un peu familier avec la langue espagnole vu que j'ai passé une bonne partie de mon enfance à regarder des chaînes espagnoles à la télé. Mon choix du pseudonyme : Pablo a été fait au pif, j'ignore pourquoi. Comme je te l'ai dit. Les séries Mexicaines qui passaient à la télé et qui me plaisait regarder dans mon temps libre ont eu probablement une grande influence sur mon choix du pseudo : Pablo. Donc, s'il te plaît Christophe, ne me confonds pas à un espagnol, bien que je sois issu d'un pays du sud frontalier ( Juste par la Mer. Devine lequel ! ;-) ) à l'Espagne que je ne citerai pas.

christophe c · May 2019

J'ai retrouvé le lien de conclusion, où des gens très généreux avaient tout tenté pour arriver à me faire apprendre Yoneda. Mais je suis un tête de pioche à ma manière et quand ça veut pas ça veut pas, donc au prix des TONNES de minutes qu'ils m'avaient consacrées, voilà, ils avaient "réussi" à me faire accoucher de cette conclusion:

http://www.les-mathematiques.net/phorum/read.php?3,664888,665017#msg-665017

à mon avis loin d'être très élégante (euphémisme)

moduloP · May 2019

Christophe : Le problème c'est vraiment de faire le dictionnaire. Je te traduit le truc, pour l'exercice, en espérant ne pas me planter (mais si je me plante tu devrais le sentir direct).

Soit $(X,\mathcal{T})$ un espace topologique. On dit qu'une application $\Phi : \mathcal{T} \to \{0,1\}$ est un "machin" lorsqu'elle vérifie les deux conditions suivantes :

1. Pour $U,V \in \mathcal{T}$, tel que $U \subset V$ si $\Phi(V) = 1$ alors $\Phi(U) = 1$.
2. Pour tout $S \subset \mathcal{T}$ tel que pour tout $x \in S$, $\Phi(x) = 1$ alors $\Phi\left( \bigcup_{x \in S} x \right) = 1$.

Maintenant, tu as une manière classique de construire des "machins", tu prends un ouvert de $X$, disons $U$ et tu considères l'ensemble $\mathcal{U} := \{ V \in \mathcal{T} \mid V \subset U\}$, et bien tu prends $\Phi_\mathcal{U} :=$ " la fonction caractéristique de $\mathcal{U}$". Le $1$ pour vrai et le $0$ pour faux.

Et Pablo demande pourquoi il n'y en a pas d'autre !

Pablo_de_retour · May 2019

moduloP a écrit:

Et Pablo demande pourquoi il n'y en a pas d'autre !

D'où, c'est une bijection. :-)
Merci moduloP.

christophe c · May 2019

Merci modulo pour la traduction. Et ça a un intérêt autre que linguistique de le formuler en les termes ultra savanto-categoriques qu'il a utilisé ou c'est juste lui qui "à décidé" ça?

Et pourquoi évoquer Yoneda pour cette évidence? (Quoique non à la rigueur là j'imagine la reponse)

christophe c · May 2019

Aux lecteurs de mon téléphone qui n'y connaissent rien de rien en catégories Yoneda dit juste que les seules fonctions qui à chaque X associe un élément de X^(X^A) et sont "naturelles" sont les

a |----> (X |---->[f |----> f(a)]) pour un a de A.

christophe c · May 2019

En caricaturant vraiment très très très peu.

Maxtimax · May 2019

Bah c'est simplement que les "machins" de moduloP sont précisément les sous-objets de $1$ dans le topos des faisceaux sur $X$; et que l'argument de moduloP montre que l'algèbre de ces machins est isomorphe à l'algèbre des ouverts de $X$ : donc pour tout espace $X$, il y a un topos dont l'algèbre de Heyting des valeurs de vérité est celle des ouverts de $X$. Après l'intérêt des topoi, je vais pas développer, mais ça a des applications en logique et en géométrie algébrique...

Quant à l'utilisation de Yoneda, c'est juste pour ne pas avoir à justifier en plus de détails qu'on a un morphisme de machins $\hom(-,U) \to R$.

Tu caricatures quand même un peu Yoneda :-D qui peut par exemple aider à prouver que certains objets existent en donnant des formules explicites; ou à prouver qu'il existe des isomorphismes sans avoir à les écrire (un peu en mode calculs bêta de primaire); ou encore à prouver sans trop se casser les pieds que la faisceau-tification est monoïdale (ce qui a un intérêt pour les géomètres algébristes); ou encore qui se généralise pour prouver des théorèmes intéressants en topologie algébrique, etc. etc.

christophe c · May 2019

Je ne connais pas tes mots savants mais si tu évoques la monoidalite comme étant le fait que

A otimes B = forall X : (A=>(B=>X))=>X

Pourquoi s'enfermer dans la verbosité catégorique pour le dire?

Mais loin de moi l'idée de critiquer ce que je ne connais pas. Mon interrogation porte plutôt sur l'optimisation. Mais je ne fais que rapporter un expérience PERSONNELLE. À chaque fois que j'ai fini par comprendre (et c'est dur !!!!) une traduction d'un lemme portant un nom pompeux il S'EDT TROUVÉ que c'était "une souris". Mais ATTENTION je suis le mec qui a prouvé que tout théorème est cas particulier d'évidence donc LOIN DE MOI l'idée de m'etonner de ce.vide apparent.

Par contre comme une courbe qui monte ... puis va redescendre un jour je suis triste de ne voir que la montée (donc de rester sur le tire fesses) en ce sens que j'aimerais voir un truc difficile rendu facile par les catégories (je n'ai pour l'instant croisé que l'inverse, des évidences traduites en chinois interminable). Mais je ne dis pas que ca n'existe pas. Il semble qu'elles soient utiles dans des domaines très très spécifiques et algébriques. Où effectivement un zippage d'évidences puisse devenir possible à partir d'une certaine complexité.

christophe c · May 2019

Je m'interroge un peu dans le brouillard, mais en gros, je rappelle que rajouter l'axiome

$$ A\to ((A\to

\to

$$

la rend commutative (ie permutabilité des hypothèses).

Partant d'une preuve on peut par exemple s'amuser à remplacer toutes les déductions

$$ \begin {array} {ccc}
A\to B & + & B\to C \\
\hline
& A\to C &
\end{array}$$

par

$$ \begin {array} {ccc}
A\to B & + & B\to C \\
\hline
& ((A\to

\to

\to C &
\end{array}$$

ce qui permet d'éviter les coupures (pas de les éliminer, mais juste de les "éviter"), en proposant une relecture où on insiste bien sur un "quasi" axiome qui dirait:

$$ A\subseteq ((A\to

\to

$$

Ensuite, si on veut on peut s'amuser à le programmer et in fine, on obtient une preuve "sans axiome non glissant" du même truc, où les spectateurs qui la liront diront "waaaaouuuuuu, il ne se passe rien et à la fin on a tout gagné, quel ce tour de passe-passe?"

Sauf que attention, les $(A\to

\to B$ (par exemple $(A\to 2)\to 2$ pour les ultrafiltres) vont itérer sans modération les passage à l'ensemble des parties. Donc on va se faire applaudir à peu de frais.

En logique classique $(A\to

\to B$ signifie juste [A ou B], et il suffit d'ajouter $((A\to

\to

\to ((B\to A)\to A)$, c'est à dire $[A\vee B]\to [B\vee A]$ à la logique intuitionniste pour obtenir la classique. Par contre, on n'aura quasiment jamais:

$$[(A\to

\to B] \to A$$

car en ajoutant ça, on se retrouve, même sans les autres axiomes logiques, avec $a-(a-b) = b$, qui devient du simple calcul formel dans un groupe commutatif.

Or Yoneda c'est quoi (en caricaturant, j'avoue)?

C'est le fait que si on suppose que $\forall f\in (A\to X),g\in (X\to Y): \phi(Y)(g\circ f) = g(\phi(X)(f))$ alors en particulier, on a

$$ \phi(Y)(g) = g(\phi(A)(id)) $$

avec $(X,f) := (A,id_A)$

Tu avoueras (mais je le répète tout théorème est un CP d'évidence, je suis le dernier à me moquer!!!!! Je peux même défendre que ça donne du jus si un jour j'ai une révélation) que bcp d'esprits grincheux te répondront en première approche "ah bin, on doit en faire des choses avec ça!"

Il y a une heuristique qui doit m'échapper. Même si je vois comme précédent à ça le fait bien connu que la règle:

$$ \begin{array}{ccc}

A & + & B\to C \\

\hline

& (A\to

\to C &
\end{array}$$

utilisée seulement avec $A=B$ (qui s'appelle alors le modus ponens) suffit à faire toutes les maths (au prix d'une mise en blanc tout de même des $A\to A$ qui borderont). Autement dit, il faudra faire $Machin (id)(id)(id)(id)...(id)$ pour avoir le théorème exact.

Pablo_de_retour · May 2019

Bonsoir à tous
On dit souvent que :
- Une algèbre de Boole est une caractérisation de la logique classique (Exemple : $ \mathcal{P} (X) $ : l'ensemble des parties d'un espace $ X $)
et que :
- Une algèbre de Heyting est une caractérisation de la logique intuitionniste (Exemple : $ \mathcal{O} (X) $ : l'ensemble des ouverts d'un espace $ X $)

Qu'est-ce que ça veut dire ça ?
Qu'est-ce que ça veut dire aussi le vocable : ''caractérisation'' dans ces deux phrases ci-dessus ?

Merci d'avance.

Maxtimax · May 2019

Mais du coup tu devrais adorer les catégories parce qu'un de leurs rôles c'est justement de trouver les "bonnes évidences" dont les théorèmes qu'on aime sont des cas particuliers. Exemple : le produit tensoriel commute avec $\oplus$ est un cas particulier d'une évidence catégorique (un adjoint à gauche préserve les colimites si tu veux les mots savants); et en fait de la même évidence qui fait que $\land$ est distributif sur $\lor$ : si c'est pas beau d'avoir deux trucs qui n'ont a priori rien à voir qui deviennent des cas particuliers d'une même évidence, et si ça ne met pas en exergue ton principe, je ne comprends pas ce que tu cherches.

Autre exemple : $A\to -$ est adjoint à droite donc préserve les produits : en cas particulier on a $(A\to (B\land C)) = (A\to

\land (A\to C)$
Et il s'avère que c'est un cas particulier... de la même évidence ! etc. etc. (je pourrais continuer des heures; par exemple le fait que si $f$ est surjective alors $f^{-1}$ est injective et réciproquement est aussi un cas particulier d'évidence catégorique, à vrai dire de la même évidence catégorique qui fait que un morphisme de groupes simplifiable à gauche est injectif)

Autrement dit, tu affirmes que chaque théorème est un cas particulier d'évidence : les catégories donnent des évidences qui nous intéressent pour des théorèmes qui nous intéressent, c'est donc un super compris, et une super instanciation de ton affirmation, non ?

Pablo : tu devrais ouvrir un autre fil pour ça, c'est une autre question. La réponse rapide c'est que les théorèmes classiques sont précisément ceux qui sont "satisfaits" (et la complication est dans la définition de "satisfait") dans $\mathcal{P}(X)$ pour tout $X$, et les intuitionnistes ceux qui sont satisfaits dans $O(X)$ pour tout $X$.

Pablo_de_retour · May 2019

Maxtimax :

J'ai ouvert un autre nouveau fil où j'ai posté ces nouvelles questions de mon dernier message figurant ici, mais AD l'a fusionné avec ce fil. Je ne peux rien faire. Ce n'est pas moi le chef ici. :-)
Je n'ai pas tout de meme pas compris ta réponse Maxtimax concernant ces nouvelles questions. Peux tu étayer tes propos s'il te plaît ?

Merci d'avance.

Poirot · May 2019

Christophe a écrit:

un lemme portant un nom pompeux il S'EDT TROUVÉ que c'était "une souris"

Le lemme du serpent ? :-D

christophe c · May 2019

@max: je peux me tromper mais ce que tu signales je n'appelle pas ça des cas particuliers mais des "équivalences". Voire souvent des généralisations car les maths sont formelles et un calcul sans type GENERALISE pour moi un calcul restreint aux contextes typés qui m'apparaissent souvent une paralysie issue de vieux complexes liés à la recherche de consistance (non contradiction).

Ensuite pour moi (et je suis bien placé puisque j'ai prouvé ce phénomène), il n'y a pas d'évidence à trouver, ladite étant toujours X=>X.

Le SEUL progrès possible est DE LA ZIPPER (elle et la descente vers ses CP) autrement que par le recours aux formalismes probant. En effet, "une fois qu'on sait" qu'on est en train de zipper (E,P) avec E évident et P qui est CP de E , on peut se permettre de rechercher des langage crypté MAIS RACCOURCISSANT.

Mais bien qu'incompetent en catégories après des années à en parler avec leur promoteurs ce que vois surtout c'edt le mécanisme suivant :

1/ on est face à un raisonnement R
2/ on recense ce qui n'est pas justifié dans R et on le met en préambule précédé par le titre "axiomes:".

La partie2 est souvent exigée par le scolaire alors que par exemple moi j'annonce souvent "lisez R, de toute façon ce qui n'y est pas justifié est AUTOMATIQUEMENT suppose donc pas besoin de préambuler.

On me le reproche souvent et j'argue contre le gaspillage d'encre.

Et bien les catégories m'apparaissent jusqu'à aujourd'hui comme l'équivalent sémantique de ce besoin névrotique de doubler les choses. Mais je ne trouve pas ça trop pretteur car c'est servir une mauvaise tendance qui est celle de donner du sens alors qu'à niveau recherche il est important de voir les mécanismes comme des suites de lettres et rien de plus.

Mais je peux me tromper et je reconnais que si le besoin de verbaliser ce qu'on voit avec flèches et diagrammes est voulu ce n'est pas moi qui vais le critiquer tant j'ai pu constater chez les élèves que le fait de ne pas extraire psychanalytiquement ce qu'ils SAVENT DEJA les handicapé. Mais pour l'heure je maintiens que c'est au fond encourager une faiblesse ... chez des chercheurs donc que ca ne va pas sans poser des soucis.

Par exemple le fait que certains ne soir t pas conscients qu'en écrivant R(x,x) ils AFFIRMENT eux mêmes y=x => R(x,y) et que l'utilisation d'une même lettre plusieurs fois fait partie DES AXIOMES qu'ils ne justifient pas me semble encouragé si on leur mache le travail en créant des cadres où cette "névroses/rigidité" peut s'épanouir.

christophe c · May 2019

De mon téléphone pardon pour les typos.

christophe c · May 2019

Je vais essayer de préciser un peu plus froidement avec un autre exemple: on a parfois l'impression que certains promoteurs cat estiment généraliser en passant d'un univers ensembliste à une cat cartésienne fermée.

Ce malentendu me paraît assez grave puisque relève d'un manque social de communication. S'ils avaient pris la peine de parler avec n'importe quel ensembliste ils réaliseraient que C'EST L'OPPOSÉ : ils particulariser par "besoin de se rassurer" alors que n'importe quel logicien depuis les années 30, VOIR DEPUIS HILBERT , utilise l'opération Ap sans contrainte ni besoin de se rassurer puissue ce dont juste des symboles et qu' on RECENSE APRÈS ce qu'on a supposé (et il se trouve que c'est 95% du temps un calcul dans une ccc même si de temps à autre on introduit (et on d'en fout) un "classificateur de sous objet".

Je prends un exemple simple: si on avait procédé autrement on aurait 1000 ans à prouver l'indépendance de l'axiome de Martin voire le forcing (vu qu'il fallait un topos BOOLEEN et non pas un topos "tout court")

Mais heureusement Cohen ne s'est pas "embarrassé de ça". Sinon il y serait encore le pauvre. Mais attention je ne dis pas qu'en algèbre ca ne donne pas de jus, mais j'avoue qu'on ne m'a jamais présenté un vrai résultat dont sans ambiguïté ce paradigme recensant de flèches à fait la différence. Je n'ai jusqu'ici que vu des reformulations de trucs bien connus.

christophe c · May 2019

Comme je l'ai souvent dit si un jour on associativise les maths je serai converti. Mais pour l'heure remplacer : X ap Y par X rond (Constante Y) me paraît très largement sous estimer l'appel à Dieu avec l'admission gratuite de l'opérateur "Constante".

Maxtimax · May 2019

Les CCC ne sont pas là pour formaliser l'opérateur "app", loin de là; elles sont là pour être un modèle au lambda-calcul; en particulier montrer des résultats de cohérence ou de complétude, comme en théorie des modèles usuelles : je ne vois pas ton problème avec ça; c'est bêtement avoir une sémantique pour notre syntaxe.
Pareil, les topoi ont un rôle de sémantique pour la logique intuitionniste d'ordre supérieure (sais-tu prouver autrement que l'axiome "tout est calculable" n'est pas contradictoire en LI ? Ou "tout est différentiable" ? etc. etc. Et ensuite appliquer les résultats obtenus avec ces axiomes supplémentaires en logique classique !) . Les topoi pour le forcing c'est plus un détail qu'autre chose, c'est dire "regardez, on n'a pas du tout regardé les topoi pour ça, mais il s'avère qu'en particulier on peut retrouver les résultats de Cohen". Similairement, les catégories peuvent donner une sémantique à la logique linéaire.

On ne t'a jamais présenté de tels résultats : en logique, certainement (pas grand monde travaille là dessus : il faut trouver des gens qui à la fois s'intéressent à la logique, aux catégories et trouvent des postes dans ce domaine), mais as-tu regardé du côté de la topologie algébrique ou de la géométrie algébrique ? (Exemple de théorème simplifié : Il y a un théorème compliqué de Grothendieck sur les faisceaux de type fini (peut-être quasi-cohérent, enfin des hypothèses de type géométrie algébrique) qui est trivialisé quand on se rend compte qu'il découle d'un résultat d'algèbre linéaire intuitionniste et que donc il est valable en particulier dans le topos des faisceaux. Autre exemple : la réalisation géométrique d'un ensemble simplicial n'est pas un caprice d'enfant, on peut la retrouver en 3 lignes si on connait des trucs en catégories, alors que c'est un truc concret de chez concret. Exemple d'applications plus générales : la théorie des foncteurs dérivés, de la cohomologie plus généralement - qui ont des applications concrètes)

Mais j'ai l'impression que tu as décidé que tu ne serais jamais convaincu :-D donc je vais arrêter d'essayer de te convaincre, ça n'aurait pas grand intérêt (je ferai juste remarquer que tu n'as pas réagi au caractère unificateur que j'ai souligné : voir la distributivité du produit tensoriel sur $\oplus$ comme instance du même phénomène que celle de $\land $ sur $\lor$ , que celle de $f^{-1}$ sur les unions et les intersections, que celle de $\land$ sur $\to$ (à droite) etc. me semble déjà super intéressant)

Pablo, pour ta nouvelle question : Tu pars du langage suivant : tu as un ensemble $V$ de variables propositionnelles, et les connecteurs (qu'on suppose distincts et pas dans $V$) $\bot, \top, \land, \lor, \to$ (rappelle $\neg X$ est une abréviation de $X\to \bot$ donc on ne s'encombre pas du connecteur $\bot$), et à partir de ça tu formes des formules comme d'habitude : tu pars des éléments de $V\cup \{bot,\top\}$ et tu les relies par des connecteurs et tu construis tes formules comme ça par récurrence (exemple : si $a,b,c,d\in V$, $a$, $a\lor (b\to c)$, $\bot\land d$, $(a\lor b)\land (c\lor d)$ sont des formules). Si tu veux plus de détails là-dessus je peux en donner, mais là je fais comme si c'était clair ce que je veux dire.

Si tu as un ensemble $X$, et une application $f:V\to \mathcal{P}(X)$ (plus généralement : une application vers une algèbre de Boole) tu peux l'étendre à l'ensemble des formules en déclarant (récursivement) que $f(\top) = X, f(\bot) =\emptyset, f(a\land b) = f(a)\cap f(b), f(a\lor b) = f(a)\cup f(b), f(a\to b) = f(a)^c \cup f(b)$ (où $Y^c$ désigne le complémentaire de $Y$ dans $X$, pour $Y\subset X$). Il faut vérifier que c'est bien défini, à nouveau je ne le fais pas ici.
Etant donnée une telle $f$ tu peux regarder quelles sont les formules $p$ telles que $f(p) = X$. Par exemple $\top$ est une telle formule, mais aussi $a\to a$ pour n'importe quelle formule $a$. Si $p$ vérifie ça on dit que $p$ est satisfaite par $f$.
Bah tu as un théorème qui te dit que : si $p$ est prouvable classiquement, alors $p$ est satisfaite par $f$, quelle que soit $f$; et que réciproquement si quelle que soit $f$, $p$ est satisfaite par $f$, alors $p$ est prouvable classiquement.

Maintenant je fais la même chose en remplaçant "$X$ ensemble" par "$X$ espace topologique", $\mathcal{P}(X)$ par $\mathcal{O}(X)$ ("algèbre de Boole" par "algèbre de Heyting") et "$f(a\to b) = f(a)^c \cup f(b)$" par "$f(a\to b) = \mathrm{Int}(f(a)^c\cup f(b))$" (bah oui, faut que ça reste ouvert ) et j'obtiens un autre théorème qui me dit que si $p$ est prouvable intuitionnistement alors $p$ est satsifaite par toute $f$; et qu'inversement si quelle que soit $f$, $p$ est satisfaite par $f$ alors $p$ est prouvable intuitionnistement.

moduloP · May 2019

Salut Christophe,

Concernant l'intérêt de traduire la trivialité des "machin" en terme plus savant sous-objets de bidule. Bin je ne peux vraiment pas te répondre, ça fait juste deux semaines que j'ai regardé le lemme de Yoneda. Donc très mal placé pour répondre à la question, surtout que je ne suis pas du tout pro des maths et je ne le serais jamais et donc c'est plus par curiosité et par plaisir que je m'amuse avec ces diagrammes et les histoires de foncteur !

Problème : bin, on se laisse vite emporter a faire des constructions à plusieurs étages et finalement c'est délicat de vérifier que ça commute bien comme on l'espère. Donc d'un côté c'est fun mais d'un autre un peu dangereux (avis perso de débutant) ! Mais comme j'ai dis, je fais des maths comme d'autre personne joue à la pétanque i.e juste pour m'amuser !

christophe c · May 2019

De retour sur un pc, c'est plus facile

max a écrit:

Mais j'ai l'impression que tu as décidé que tu ne serais jamais convaincu

Ah non, là tu te trompes, je n'ai vraiment pas de position issue de désirs, j'adore me tromper et avoir des surprises, surtout à mon âge! Je suis une personne avide des chemins qui mènent au paradis, donc des contradictions trouvées dans les curcuits.

Mais quand je ne connais pas bien une spécialité, je fais le choix PUREMENT CONVENTIONNEL de dire "je ne suis pas convaincu" plutôt que le choix de dire "je suis convaincu" (à quoi rimerait de dire je suis convaincu face à un truc qu'on n'a pas capté?)

Dans ce que tu dis il y a des exemples que je ne connais pas, par contre, il y a des arnaques bien connues (pas bien connues en tant qu'arnaque) qui peuvent couter très cher en temps à qui s'y laisserait prendre, donc je tiens à préciser certains exemples, que je connais partiellement, que tu signales.

1/ Préjugé1: utiliser des topos (même seulement de Gronthendieck, donc "sémantiquement plein") serait faire de la théorie des ensembles intuitionnistes.

C'est une profonde foutaise!!! Il n'y a pas d'autres mots.

2/ Préjugé2: Il y aurait des "modèles intuitionnistes" de la théorie des ensembles où toutes les applications de $\R\to \R$ seraient continues (et même, tu ne l'as pas dit, localement affines).

C'est une profonde foutaise!, corollaire :-D de la foutaise1.

Entendons-nous bien, j'ai dû croiser le livre (et je l'ai dévoré en diagonale), qui sauf erreur, s'appelle "géométrie synthétique" quand j'avais à peine 30ans. J'y ai cru. Surmoi, ce n'était pas grave car j'étais déjà un peu structuré et j'avais conscience du caractère "slogan" du truc. Mais je souhaite attirer l'attention sur le caractère DEPLORABLE en termes de formation que peut constituer ce genre d'arnaque sur des étudiants qui n'auraient pas auparavant "une solidité logique".

Je ne critique en rien la qualité et les difficultés surmontées de ce travail, je ne critique pas non plus en interne (par exemple, un mail envoyé au CNRS à des gens avertis) l'envoi d'un slogan, mais je trouve très dangereux de "validier un mensonge même bon enfant" quand on parle sérieusement, surtout si on s'adresse à des gens peu structurés.

Je rappelle au lecteur c'est qu'est (sans technique) un topos. Soit $U$ l'univers mathématique. Oublions le signe $\in$. Ne regardons que les triplets $(A,B,f)$ où $f est une application de $A$ dans $B$. Ca forme une catégorie évidente, qui de plus a des propriétés truc et machin qui en font ce qu'on appelle un topos. La seule connaissance de cette catégorie (ie objets, flèches et opération rond) donne déjà énormément d'information sur l'univers. Réciproquement les propriétés "truc et machins" ont décidé d'être abrégées en "être un topos".

Il se trouve qu'il y a un truc (facile à définir) qui a une structure d'algèbre de Heyting dans les topos. Cela donne l'illusion qu'on y fait de la logique intuitionniste. Et là, attention, on risque de vite tomber dans la politique. Car la vérité est bien sûr "non". On 'y fait pas de la logique intuitionniste au sens propre, on y fait un truc qui peut partiellement s'appeler, à condition de se mettre de très grosses oeillères, des raisonnements intuitionnistes.

Cela permet à des gens de s'exprimer par abus de langage avec les termes "consistance relative", etc, et de faire croire que les topos sont des univers ensemblistes intuitionnistes.

C'est faux. Pour une raison tout bête, c'est qu'il n'existe tout simplement pas d'univers authentique qui soit non classique. En effet,l'axiome d'extensionalité collapse tout et force la logique classique*** (voir mes nombreux posts à ce sujet)

Maintenant attention, oui, ce sont des choses intéressantes et oui comme tu le rappelles max, ça semble très utile dans la spécialité (je dis là car ça semble être une bi-spécialité) topologie+géométrie algébrique (qui n'ont de pologique et de géométrique que le nom, mais c'est une autre affaire)

Ensuite, oui, max, tu sembles être sincère quand tu dis que ça unifie (j'y ai toujours cru, sur la base de témoignages car je n'y connais rien) plein de chose qui sans ça sont difficiles. Mais là encore, si tu prends le truc au total, en quoi est-il simplifié.

S'il faut ingurgiter un langage une théorie de 50 à 100 pages pour arriver in fine à prouver 2-3 trucs en 5 lignes, comment comptabilises-tu le poids total. Pour moi c'est 100 pages + 3 lignes, ce n'est pas 3 lignes tout court. En outre, la théorie en soi est assez basique, et j'ai grandement l'impression que les gens qui s'y investissent apprennent tout bêtement des réflexes conditionnés de l'ordre d'un "langue en 2D" (lecture rapide de diagrammes et de quantificateur sous-entendus).

Ca me pose problème (pas seulement par ma dyscalculie et mes lenteurs): en effet, je crois qu'il faut prendre une vraie décision institutionnelle un jour si on veut que les enfants apprennent une langue qui s'écrit en 2D. Pour l'heure on voit des gens dont 90% apparaissent comme snobs (1) (voire souvent imposteurs innocents!!! Ne sachant pas résoudre le moindre petit exo d'analyse) et seulement 10% semblent s'être initiés (2) à cette langue, et ces 10% se parlent entre eux, ou daignent de temps à autre nourrir un fan du groupe (1) sans le recaler car estiment que "c'est bon pour la cause".

Je n'aime pas trop ça: pour moi, en maths on prouve et le sceptique est roi. Les échanges ne doivent pas se faire entre initiés. Surtout quand il s'agit de solution!!!!!!!

Jeveux bien d'autres exemples (j'espère ne pas avoir été trop critique), mais en as-tu qui sortent de cette spécialité. Par exemple a-t-on un problème résolu par Grothendieck et accessible par la plupart des gens pros qui n'y connaissent rien ni en cat, ni en toppo alg, ni en geo alg?

*** il y a 2 sortes de logique intuitionniste.

1/ Une (la "fausse" ou celle des premiers balbutiements maladroits) qui est dogmatiquement définie en privant la partie droite des séquents du droit à avoir plusieurs items. Celle-ci n'est "sérieuse" et crédible en tant que telle que dans le propositionnelle. Dès qu'on monte, elle n'est plus autre chose qu'un vague arbitraire.

2/ La "vraie" (c'est une affaire de convention) qui émerge de recherches profondes l'ayant située dans une hiérarchie des axiomes issue de ce qui est du moins vers le plus garantissant absolument. Je les rappelle:

déplacement de ressources
suppression de ressources
clonages de ressources
remontée dans le temps (pérennité + clonage des ressources)

La logique intuitionniste véritable est celle qui admet les 3 premiers pouvoirs, la logique classique est celle qui admet les 4. Les deux premières ressources PLUSSSS l'extensionalité donne les 4 ressources. Il n'y a pas de théorie des ensembles "véritable" (ie de maths véritables) qui serait "intuitionniste sans être classique". Pour y parvenir, il faut tricher, c'est à dire demander à un des deux joueurs de se tirer volontairement des balles dans le pied, ce qui est idiot même si artificiellement obtensible (par exemple avec les topos, mais probablement de plein de manière artificiellement montables par encore découverte)

christophe c · May 2019

@modulo merci pour ton témoignage

@max, erratum: je corrigé ce que j'ai dit sur un point. Oui on peut peut être faire des maths non classique de hauts ordres MAIS CA NE PEUT SE FAIRE SUE SANS EXTENSIONALITE. Je n'ai jamais voulu faire de l'extensionnalite une obligation dans mon post précédent.

Mais attention: desextensionaliser les maths => les deplatoniser. Ce ne serait pas rien.

christophe c · May 2019

Je l'ai souvent dit (en faisant t hurler Gérard :-D ) j'invite à la prudence les gens qui font t semblant de ne pas être platoniciens.

Maxtimax · May 2019

Il va falloir préciser ce que tu entends par ce que tu dis sur les topoi, puisqu'il y a des théorèmes (pas des avis ou je ne sais quoi) qui montrent qu'ils jouent effectivement le rôle de sémantique pour la logique intuitionniste : cet énoncé n'en est pas un, mais il cache un vrai énoncé qui dit quelque chose qui, lorsqu'on le traduit en langage non formel dit ça. Cette traduction n'est évidemment pas fidèle, mais dire que c'est faux mérite plus ample explication :-D (au besoin je pourrai te trouver les théorèmes précis et tu me diras ce qui ne va pas dans ma traduction informelle)

Ensuite, tu dis 50 à 100 pages mais c'est une grosse exagération : dans les 50 à 100 pages il y en a au moins les 3/4 qui sont des exemples, là pour donner l'intuition. Si je voulais faire une intro aux catégories suffisante pour prouver que les adjoints commutent aux (co)limites de la même manière que tu fais tes intros aux ordinaux (i.e. rapide, sans passer de temps sur exemples/intuition/psychologie ou phrases pédagogiques), il me faudrait sans doute moins de 5 pages. Et quand 5 pages permettent d'unifier une telle variété de phénomènes, je le prends comme une bonne chose.

Finalement, tu demandes un exemple hors des mondes topo/géo algébrique. C'est une demande compliquée (les cat ont été découvertes littéralement pour la topologie algébrique, et développées dans ce domaine puis par Grothendieck donc en géo alg). Néanmoins je vais essayer. Tu n'es pas satisfait, j'imagine, par l'exemple du produit tensoriel ?
Je le répète quand même à tout hasard : des théorèmes généraux de théories des catégories montrent 1) son existence et unicité à (unique) isomorphisme près, 2) sa distributivité sur $\oplus$, 3) le fait qu'il préserve les surjections.

En théorie des représentations, les mêmes théorèmes généraux démontrent l'existence (et unicité blabla) de l'induction (et de la co-induction) ainsi que la réciprocité de Frobenius, tour ça dans des cadres en fait plus généraux.
(Mais ce sont des trucs que tu ne connais pas, je crois)

Oh et aussi, petite pub pour Yoneda : le théorème de Cayley en théorie des groupes en est un cas partiulier (bon là c'est clairement plus simple de montrer Cayley, j'avoue)

Les autres exemples auxquels je pense sont en topo/géo algébrique, mais c'est principalement dû à ma formation :-D

christophe c · May 2019

Oui je préciserai d'un PC.

Mais pour les exemples que je comprends je ne vois vraiment pas. Comme tu sais peut être je rappelle souvent ce que j'estime être là bonne definition du produit tensoriel et c'est trivial. Jamais vu que les catégories feraient mieux mais je veux bien voir (moi ça fait une ligne et on a tout y compris preuve). De plus on a de même avec toutes les Stoneries (Stones Cech etc) et il n'y a rien à unifier puisque ça m'est déjà. Si les cat "récupèrent" les produits pour dire "qui dit produit dit catégories" j'appelle juste ca de la politique. Politique ne veut pas dire "mal".

Je parlerai plutôt d'un problème ouvert longtemps resté bien accessible en tant qu' énoncé et résolu ENDUITE par un apport cat. Je ne doute pas une seconde que les cat résolvent bien des problemes de cat. De mon téléphone

christophe c · May 2019

Anecdote amusante: tu m'as bien avec l'expression "théorème de Cayley". Je ne sais pas pourquoi je prejugeais que c'était "tout sous groupe d'un groupe libre est libre :-D

Je me demandais en quoi une approche catégorique en simplifiait la preuve.

Las j'ai fini par googler. Merci pour cette bonne blague. Ça m'apprendra à être inculte. À noter que l'évidence (il n'y a rien à prouver c'est un axiome) en question est UN AXIOME platonicien ensembliste pur et dur avant tout. C'est donc l'archétype d'un mauvais exemple. Car on a typiquement besoin de Ap.

Maxtimax · May 2019

Bah non c'est pas unifié, puisque tu as d'un côté Cech et de l'autre le produit tensoriel :-D
Je veux bien voir une preuve plus rapide que "Par définition, $-\otimes A$ est un adjoint à gauche donc préserve les colimites, en particulier $\oplus$“.

À nouveau c'est compliqué de répondre, c'est comme si tu me demandais un problème ouvert que $\in$ a résolu...

Oui Cayley c'était une blague (enfin pour qui n'aime pas les interprétations)

L'autre théorème que tu mentionnes s'appelle Nielsen-Schreier, et il y a très peu d'espoir qu'une approche catégorique le simplifie puisqu'il est faux dans d'autres catégories qui ressemblent beaucoup aux groupes

christophe c · May 2019

Merci pour les infos. Bon, j'ai rallumé mon pc, parce que j'éclate les yeux avec mes lunettes de presbyte à 10E. Mais je dois aller chez le coiffeur (enfin je veux).

Pour le produit tensoriel, je te mets au défi de déplier les abréviations. Evidemment avec ce que tu écris, ça donne l'illusion que c'est court, mais tu as 4 mots savants dedans. Idem je peux dire que la formule de Stokes trivialise Brouwer à ce train-là, mais vue l'empilade de définitions qu'il y a derrière :-D

Cependant je crois que j'ai une piste sur l'illusion qui fait que les catégoristes se croient unificateurs à ce point (et attention, je ne nie en rien leur côté unificatrice, je l'ai répété bien des fois, mais je parlerais plutôt d'ambition unificatrice).

Avant de préciser détailler un peu ma piste, je tiens à "prouver" que je ne suis pas anti-catégories. Lorsque j'ai inventé le prouveur-sceptique calculatoire pour mes élèves (ie c'est un jeu où on a en permanence un couple $(x,y)$, le prouveur propose $z$, le sceptique choisit entre $(x,z)$ et $(y,z)$ et on continue, le prouveur ne gagnant que si une étape $(u,v)$ tel que $u=v$ est évident), j'ai remarqué que les non-matheux mettaient énormément de temps à s'apercevoir que maths = psychanalyse (en le sens que par exemple le bon coup à jouer face à $(147-53, 94)$ est $140+7- 50 - 3$, et qu'il bascule dans le camp matheux le jour où il réalisent qu'il est bon de jouer ce qu'on pense au lieu de $99-5$ comme ils le faisent avant). Je n'ai donc rien contre les gens qui déplient les évidences plates pour essayer de les "verbaliser". Je suis le premier à le faire en ayant remarqué l'erreur du modus ponens, que j'ai remplacé par $\frac{A+(A\to

}{(A\to A)\to B}$. C'est en effet une démarche de reconnaissance que maths = psychanalyse intérieure de nos certitudes, donc "a priori" une démarche intelligente.

Mais je reste pour l'instant un observateur, peu convaincu que le taf a vraiment bien avancé. D'autant que cat est submergé de cicatrices historiques et de gens (exemple Benabou) qui ont énormément souffert d'ostracisation, et donc exagère bcp trop maintenant que réhabilités.

La pise est qu'un topos est "essentiellement" l'étude des flèches entre les cardinaux (vus comme ordinaux particuliers). Or un truc m'a toujours marqué: les catégoristes incompétents (ceux qui le sont parmi les) ont de la salive plein la bouche quand ils tombent dans les délires petit vs pas petit.car probablement ce faisant, ils s'imaginent flirter avec les grandes tailles que sont les collections non collectivisantes. Je viens de réaliser que peut-être une partie de ce domaine ambitionne d'automatiser ça. Cette idée me vient car les définitions que je donne sont souvent de la forme "produit de tous les machins" alors que des esprits amateurs pourraient répondre "attention, il n'y a pas d'ensembles de tous les machins", ignorant que ce problème n'existe évidemment pas en TDE professionnelle. Or j'ai tendance à considérer que "les gens comprendront tacitement" que ce n'est pas un problème (pas plus que les contradictions ne le sont de toute façon, donc je ne distingue pas les amateurs des pros, ce n'est pas juste que je demande aux amateurs d'être des pros).

Une piste possible (et noble) serait peut-être que les cat cherchent à "verbaliser" et automatiser les sorties de l'univers qui n'en sont pas. Dans ce cas, on comprendrait peut-être mieux quel type de travail ils cherchent à s'infliger et pourquoi ce qu'ils font peut apparaitre "gérer du vide" à d'autres spécialités.

Cependant, je rappelle que le "gros" (selon moi) problème ouvert est l'élémination pertinente de "singleton", mais absolument pas celle "du produit de tous les espaces compacts de l'univers" qui elle ne pose pas de souci. Je m'explique.

On peut définir tout à partir de $\subseteq $ et $x\mapsto \{x\}$ (que j'appelle singleton), puisque $(x\in y) = singleton(x)\subseteq y$.

En un certain sens $\subseteq $ est bien "associatif" (ça se traduit par sa transitivité vu que c'est une adjectif et non une fonction).

C'est le pendant de ce que j'ai dit avant à savoir que $Constante(f(g)) = f\circ Constante(g)$

Certes $\circ$ est bien associative, mais $x\mapsto Constante(x)$ est bcp trop mystérieuse encore me semble-t-il. Cette piste me semble bien plus prometteuse que juste envoyer chez le coiffeur le produit de tous les espaces vectoriels de l'univers, avant de l'emmener en soirée mondaine où des allergiques aux "non collectivisante" seraient les chefs de soirée.

Pour info culturelle, je re-rappelle que Yoneda est un cas particulier du "théorème" :-D qui dit qu'un ultrafiltre stable par intersections quelconques est principal et que le jus découvert par la recherche ensembliste est de prendre des ultrafiltres qui sont bien stables par intersections quelconques, mais pas principaux (mais ils ne sont pas dans l'univers :-D ) . On ne saurait rêver conflit plus carré.

christophe c · May 2019

Bon cela dit, là je suis en train de dévier vers "recherche et philosophie" et c'est le fil de Pablo (initialement je suis intervenu car choqué de voir un néophyte s'exprimer en chinois et recevoir une réponse en "chinois2D". Et ce pour des raisons démocratiques AVANT tout et non de "recherche" (qui est une autre affaire).

Foys · May 2019

christophe c a écrit:

Je l'ai souvent dit (en faisant t hurler Gérard grinning smiley ) j'invite à la prudence les gens qui font t semblant de ne pas être platoniciens.

Ca c'est un peu malhonnête ("vous pensez comme moi sans vous en rendre compte").
De toute façon le "platonisme" est une notion subjective (chaque mathématicien est convaincu que les objets qu'il pense réels sont réels mais la liste des objets vraiment réels varie d'une personne à l'autre. Rappelons que Lebesgue a nié l'existence de l'ensemble des parties d'un ensemble quelconque).

Maxtimax · May 2019

Christophe : bah oui mais au même titre qu'il y a des abbréviations pour dire "$R$-module“, “application bilinéaire“ etc. Parmi toutes ces abbréviations, les catégoriques prennent le moins de place, et de loin.

Quant aux TDEistes professionnel.le.s je m'abstiendrai de faire un commentaire parce que l'expérience que j'en n'ai ne coïncide pas avec la tienne, mais j'en ai sûrement moins fréquenté que toi.

Je ne comprends pas ce que tu racontes après mais ça doit être moi.
Il ne faut pas non plus oublier qu'en plus d'être un langage aujourd'hui indispensable en topo et géo alg. , il y a un grand rôle de "distinguer ce qui est en rapport avec le problème de ce qui ne l'est pas". Typiquement, le truc du produit tensoriel c'est dire ”cette information n'a rien à voir avec ma situation spécifique, c'est “formel“ donc je peux la mettre de côté et me concentrer sur ce qui m'importe“

christophe c · May 2019

@foys: oui mais ce disant :-D Tu dis que chacun EST platonicien :-D ce qui est plus brutal que moi. Tu dis juste que la fonction n'est pas constante. Moi je ne dis qu'une chose. On découvre, on n'invente pas.

@max: bon en tout cas avec toi les catégories semblent avoir fait une belle prise. Tes derniers mots sont assez politiques comme tu dois le voir toi même lors d'une relecture. J'essaierai de technicien et être plus précis d'un PC vu que Pablo vient d'annoncer son recul / ces thèmes.

Maxtimax · May 2019

Christophe : cette année j'ai fair que de la topo. alg en gros donc pas trop le choix ;-) (je ne vois.pas ce qu'il.y a de politique)

Edit : c'est pas vrai de vrai, j'ai aussi fait de la géo alg.et de l'algèbre commutative et des représentations. Mais à chaque fois je parlais en.cats

christophe c · May 2019

Ce n'est pas un reproche, je vante souvent ce que j'estime d'excellents restaurants de poisson, même auprès de gens allergiques au poisson.

Les habitudes et la familiarité avec une pratique donnent souvent envie de la défendre.

C'est pourquoi, je fais comme je peux pour choisir des mots, à la fois un peu sceptiques, mais aussi pas trop incromprenant de l'état des interlocuteurs qui poiurraient mal prendre qu'on ne comprenne pas leur passion.

Bien avant même d'évoquer les catégories sur le forum, je répétais et répétais que les maths feraient un grand bond le jour où elles produiraient des preuves "non inventives" des théorèmes de topologie algébriques les plus externalisables (disons Brouwer pour faire simple). Je sais et je comprends que les catégories y aient élu domicile en attendant qu'on trouve ces preuves.

La géo -alg je ne connais pas du tout et quand je vois le long fil de Claude sur une équation dioophantienne de degré 3 qu'il affronte depuis des semaines, je n'ai SURTOUT pas envie de connaitre. La recherche professionnelle (et là je le vois sur le forum) conduit à une immersion parfois assez incroyable, avec un grand manque de pauses.

Pour apporter un témoignage humain, sache que j'ai taffé à ma sortie d'HP sur le pdf de 400 pages de A.Prouté et l'ai lu presque entièrement, je ne suis pas non plus un "débarquant". C'est à lissue de cette lecture que je me suis convaincu qu'on faisait fausse route dans le sens que mon intuition me dit (mais mon intuition peut me tromper) que c'est une voie sans issue.

La raison principale, je l'ai souvent dite: l'obsession du typage a une histoire psychanalytique douloureuse qui est la recherche de consistance (typer une preuve dans le système avec implication et intersection c'est l'assurance qu'elle normalise fortement ET RECIPROQUEMENT), on a donc une caractérisation complète de ce qui normalise.

Grace à l'extensionalité, toutes les théories mathématiques naturelles normalisent fortement de toute façon (même les contradictoires, qui prouveront alors non(ext)).

Seules les théories CONTRADICTOIRES représentent correctement la vie (elles seules donnent des OS qui sont en permanence allumés, ce qui est le rôle d'un OS, un OS éteint ne sert pas à grand chose :-D ). L'obsession du consistant et le typage "contrôlé" qui plus est (celui avec intersection ne l'est pas) me paraissent sans issue, même s'ils donneront peut-être encore quelques bons résultats dans les années qui viennent, je suis persuadé que sous peu , un gars (ou une fille!!) publiera quelque part que c'est vain.

Bon, en attendant, les gens s'éclatent, c'est le principal.

Je redis ce que j'ai dit que tu disais ne pas avoir compris.

Dans $P(E)$ tout ultrafiltre stable par toute intersection est principal. Même s'il est EXTERIEUR à l'univers.

Pour obtenir des résultats, il a fallu s'occuper dultrafiltres stables par intersections quelconque HORS de l'univers et SURTOUT PAS SUR l'algèbre de Boole $P(E)$.

C'est dire à quel point il a fallu faire de l'anti Yoneda. C'était ça (je n'ai pas relu) mes dernières phrases. Concernant les objets universels, je te redis (en fait, j'ai vu de mon téléphone chez le coiffeur que tu avais répondu quelque part "Stones Cech d'un côté et produit tensoriel de l'autre, c'est dispersé alors que les cat blabla") que ça n'a rien de dispersé, je te le dis en termes (simples) de catégories: "si tu peux former tous les produits que tu veux et prendre le plus petit machin contenant dans un cadre C, alors, étant donné S, tu prends le produits des X quand (f,X) varie les tels que $f$ va de $S$ dans $X$ et est "correct" (morphique) et $X$ dans C. Et une fois que tu as ça, $j:X \to P$, tu prends le plus petit T de C contenant l'image directe par $j$ de $S$.

Tu obtiens ainsi tous les trucs du genre produit tensoriel, stonifié divers et variés, etc. Faut juste pouvoir faire le produit et prendre le plus petit surmachin de.

Bien sûr qu'on peut se "fatiguer" à le faire catégoriquement, mais c'est trompeur car ça laisse le préjugé que ce que je viens de dire n'est pas formel (un peu de la même façon que j'ai rencontré bien des gens me disant que les articles du monde ne le sont pas, et ce préjugé là, qui est faux, tout est formel, simplement le recensement est à gros grains quand c'est en langue naturelle, "je le combats". Répéter ça en disant "on fait des catégories" me parait dangereux, de même que répéter une intuition de CE1 en disant "on fait des suites arithmétiques on est en première ça rigole plus", me parait malsain).

Cela dit, c'est un détail. Et je suis entièrement d'accord que la production de questions est une qualité du paradigme catégorique, auquel je ne nie pas le statut de langage encourageant pour ceux qui le maitrisent.

christophe c · May 2019

Remarque: le "plus petit machin" est juste une colimite, mais peu importe, il y a des situations où on a des plus petits machins mais pas de colimite.

christophe c · May 2019

ou une limite, je ne sais jamais de toute façon :-D

Maxtimax · May 2019

Mais ton argument là c'est un argument de catégories ! Pile poil ! Que tu veuilles appeler ça autrement, très bien, fais toi plaisir, je ne suis pas linguiste :-D mais le fait est que tu viens de reproduire exactement l'une des preuves du théorème du foncteur adjoint (au vocabulaire, hypothèses et généralité près, mais peu importe)
Tu veux appeler ça "formel", je veux appeler ça "catégories" : très bien, il faudra juste traduire quand on se parle ;-)

(Tu dis "préjugé de dire que ce n'est pas formel" : relis mes messages, je te cite le passage intéressant : ' "distinguer ce qui est en rapport avec le problème de ce qui ne l'est pas". Typiquement, le truc du produit tensoriel c'est dire ”cette information n'a rien à voir avec ma situation spécifique, c'est “formel“ donc je peux la mettre de côté et me concentrer sur ce qui m'importe“' - on dit la même chose, sauf que tu appelles ça 'pas des catégories', et moi j'appelle ça des catégories !)

christophe c · May 2019

De toute façon, on s'est compris (enfin je te dois des détails techniques sur l'impossibilité d'avoir de "vrais univers intuitionnistes").

Mon intervention voulait surtout alarmer contre le chinois 2D qui se met en place dans UNE PARTIE de la communauté, créant un ésotérisme en conflit avec le devoir de prouver. N'importe qui, qui ne parle pas le chinois2D (toi tu le parles) peut constater que quand modulo a donné sa traduction de ce que Pablo demandait, on a bien eu affaire à une traduction exactement au même titre que quelqu'un qui viendrait de me traduire un paragraphe allemand de wikipedia.

De plus (toujours les gens qui ne parlent pas le chinois2D), ils s'étonneront de la trivialité demandée (en admettant qu'ils ne connaissent pas Pablo). C'est juste un sentiment que je laisse à chacun le soin d'évaluer. Ce n'est pas inoffensif dans la sociologie des maths.

Pour le reste, j'ai confiance en l'aspect cuit à assez petit feu (malgré ta jeunesse) de ce que tu racontes, je ne t'ai pas souvent vu t'enflammer sur des sujets que tu ne connais pas ou connais nouvellement, donc je te lis (et te relirai dans les mêmes passages) en tentant d'apprendre des vraies infos de ce que tu as partagé.

christophe c · May 2019

@max, il y a quand même eu quelques mâle te dis techniques que je n'ai pas vu en première lecture.

Bon je maintiens bien sûr que ta phrase politique est trop vague mais ça tu le sais. Par contre, je crois qu'on ne s'est pas vraiment compris sur L'EXISTENCE.

Tu sembles dire que percevoir les.evidences "abstract non sense" n'a pas besoin d'être plus qualifié de formel que de categoriste et que c'edt un faux débat de linguiste.

Mais ça why not. Je ne voulais pas imposer un mot. Ce n'était pas mon but. Je ne suis pas "outré" quand quelqu'un dit "c'est categoricien" des qu'il y a des flèches.

Mon propos concernait AUTANT VOIR PLUS les existences que les propriétés des trucs supposés exister. En général c'est trivial UNE FOIS EXISTANT donc pour moi le débat n'était pas la.

Je t'accorde et ne l'ai jamais contesté que le langage des flèches quantifiées apporté une machine à produire des questions intéressantes sans aucune réserve. Mais ça ne les resout pas. On l'a d'ailleurs vu puisque tu n'as pas réussi à fournir (et comme tu es des plus forts du forum) à proposer de problèmes résolus par cat et qui posait des.soucis avant.

Je suis sur mon téléphone mais vais ajouter un truc que Max a dit et qui s'est peu vu car savant en termes populaires.

Il est rare (en logique c'est considéré comme suspect et donc pauvre) qu'un truc du premier ordre donne quelque chose qui s'exprime au deuxième ordre sans afficher de très grosses pertes sehes et brutales de substance. Exemple si vous trouvez une propriété ordre1 telle que tout anneau qui la possède est noetherien et bien vos anneaux seront TRIVIALEMENT noetheriens.

Or je ne suis pas expert mais psychanalytiquement je pense avoir trouvé ce qui fait inconsciemment triper les categoriens quand ils prononcent "adjonction adjonction adjonction". C'est que c'est justement une propriété DU PREMIER ORDRE qui force la "continuité" (qui est du deuxième ordre**).

Comme je ne suis pas expert je ne peux pas savoir l'étendue de la perte sèche payée comme prix. Mais disons que je reste un peu sur la réserve en attendant d'en savoir plus.

** d'un PC je donnerai la démo: si f,g sont adjointes elles sont "continues".

Comme autre exemple vous avez (croissance + surjectivité ) dans IR , mais il y a tout de même un "il existe" qu'on peut enlever en introduisant un nom de fonction semi inverse. Bin c'est la même chose. Pour ceux qui n'y connaissent rien cat, c'est un peu comme si un labo d'université d'analyse avait décidé de se focaliser sur les croissantes surjectives et en faisaient de la pub dans tous les médias. Ça a sa valeur, mais il serait intéressant de mesurer le prix payé.

Algèbre de Heyting et topoï

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 26