Question d'un ignare

umrk · December 2020

Question d’un ignare (et que donc il vous est loisible de balayer d’un revers de la main).

Je suis avec intérêt et admiration vos discussions, même si elles me passent bien évidemment au-dessus de la tête (et notamment votre capacité à évoluer dans une infinité d’infinis ...).

Mais avant ceci, je pensais que la TDE était quelque chose de démodé, supplanté par les catégories, puis les Topos, et que c‘était une des raisons (pas la seule), de l’« épuisement » du projet Bourbaki (par ailleurs tout à fait admirable (la critique est facile ...)).

Laurent Lafforgue a fait le 6 Novembre dernier (c’est donc récent) une conférence :

https://aroundtoposes.com/laurent-lafforgue-on-the-creative-power-of-categories/

Où, (dans son style assez peu diplomatique), il rend compte du peu d’intérêt de la communauté scientifique vis à vis des Topos, pendant longtemps (c’est en train de changer).

Il montre que les catégories ont un lien avec la logique :

Evidemment, pour moi qui est un grand admirateur de Patrick Dehornoy, il m’est difficile d’imaginer qu’il a passé la plus grande partie de sa vie à explorer une voie sans issue, aussi je serais intéressé par vos commentaires …..

En particulier, je vous entends dire que toutes les mathématiques peuvent être construites au-dessus de ZF (ou ZFC, ou …), et je comprends que cet objectif est une puissante motivation, mais n’existe-t-il pas une autre voie, au travers des catégories (comme l’a suggéré Lawvere) ?

Maxtimax · December 2020

Démodé, peut-être, ça dépend ce que tu entends par là. Certainement qu'il y a moins de postes en TDE de nos jours qu'à une certaine époque, mais c'est le cas d'à peu près tous les domaines des maths pures...

Supplanté par les catégories et les topos, certainement pas. En fait, il y a un truc qui est très important à retenir c'est que pour la plupart des maths, les fondations précises n'importent pas ou du moins très peu. Ceci étant dit, si une personne a un doute sur ce qu'elle a "le droit" de faire etc., le dernier recours sera dans la plupart des cas ZF(C), et certainement pas les alternatives catégoriques (sauf rare exception). D'ailleurs, il est encore compliqué de nos jours de donner un sens à des fondations catégoriques, surtout puisque dans les formulations usuelles, les catégories sont fondées sur les ensembles.

Même s'il y avait d'autres fondations, cela ne signifierait pas que la TDE est une "voie sans issue" : une grosse partie de la TDE de nos jours n'est absolument pas fondationnelle (voire la plupart ? mais je ne m'y connais pas assez pour affirmer ça), donc même si la TDE n'était pas la théorie "du fondement", elle ne serait pas une "voie sans issue".

Pour ton dernier paragraphe, concernant Lawvere; oui, certainement on peut créer d'autres choses qui fonctionnent. La théorie ETCS de Lawvere est légèrement plus faible que ZFC mais suffisante en pratique.
Mais les topoi tels que Lafforgue les envisage n'ont pas cette vocation, si je ne m'abuse. En tout cas le programme de Caramello, qui a l'air d'être sa motivation principale, n'a pas cette vocation fondationnelle, c'est un programme orienté vers des applications (en maths pures, mais des applications tout de même). Donc c'est une question tout à fait différente.

umrk · December 2020

Merci de ta réponse. Et, c'est vrai, ni Olivia Caramello (ni d'ailleurs L Lafforgue, autant que je sache) ne présentent les Topos comme une alternative à la TDE pour ce qui est de fonder les mathématiques.

Foys · December 2020

La théorie des topos demande une très bonne aisance en théorie des catégories et ce langage déroute pas mal de mathématiciens (s'exprimer par flèches est très différent de s'exprimer en termes de "l'objet $x$ tel que" et "ceci appartient à cela").

Martial · December 2020

Au risque de me répéter, je suis d'accord avec Max. Je n'y connais rien en catégories, encore moins en topos, mais je donne mon avis concernant la TDE : quand j'ai démarré mon projet d'écriture en 2010 je voulais intituler le bouquin "La théorie des ensembles pour les nuls". L'idée était de partir de rien, disons, d'un bon niveau de Terminale S (ça va faire marrer Christophe, que je salue au passage s'il a du réseau sur sa plage bretonne, lol) et d'aller le plus loin possible.

Première anicroche : un mien ami, grand informaticien devant l'Eternel, a lu le chap 0 et n'y a pas tout compris. Il m'a écrit un mail, dans lequel il disait, entre autres : "si tu ne changes pas le titre, je vote Sarkozy aux prochaines élections, et je ne t'adresse plus la parole du restant de ma vie."
Du coup, j'ai changé le titre.

Deuxième anicroche : je me suis assez vite rendu compte que si un fraichement émoulu du bac S voulait lire mon livre, il me faudrait lui expliquer l'algèbre linéaire, la topologie, des rudiments d'analyse, lui donner des exemples d'ordres partiels pour qu'il comprenne l'énoncé du lemme de Zorn, etc. Bref, impossible.
Du coup, j'ai revu mes ambitions à la baisse et j'ai écrit dans la préface qu'un niveau L3 était souhaitable pour aborder la lecture.

Troisième anicroche : je voulais me démarquer des autres ouvrages du domaine en insistant sur l'aspect fondationnel de la TDE Là, j'y suis plus ou moins arrivé, mais seulement au début. Au chap 7 on a fini de construire $\mathbb{N}, \mathbb{Z}, \mathbb{Q}, \mathbb{R}, \mathbb{C}, \mathbb{H}, \mathbb{O}, \mathbb{S}$, etc, et après il n'y a plus grand chose de fondationnel. Tout au plus au chap 13, quand j'introduis la notion de rang, je montre que $V_{\omega + \omega}$, ou même un $V_{\omega + N}$ avec $N$ assez grand suffisent amplement pour faire toutes les maths hors TDE... et après, plus rien de fondationnel.

Alors, comme dit Max : fondationnel, oui, mais dès qu'on rentre dans la théorie avancée on ne parle plus que boutique, et il faut se mettre les mains dans le cambouis...

Martial · December 2020

@umrk : je peux te rassurer, Patrick n'a pas passé une partie de sa vie à explorer une voie sans issue. Sans parler de ses travaux de recherche (dont les vingt dernières années sont clairement hors TDE), il a contribué à ce que le néophyte "pas vraiment balèze en anglais" puisse appréhender l'essentiel des bases de cette théorie.

christophe c · December 2020

De mon téléphone. Je n'ai pas lu, juste survolé. Mais en résumé, ça n'a rien à voir et il y a pas de concurrence. Les maths se font même sans en avoir conscience en TDE. La TDE qui a à la fois l'apport platonicien (qui permet de parler sans main qui tremble, sans connaissance et sans expertise), ne type pas et descend de manière peu étudiée dans les logiques faibles.

Des outils DE RECHERCHE permettent d'avancer dans des directions unifiantes pour des théories faibles (à peu de risque d'inconsistance). En particulier quand ça "type bien" (par exemple quand E inter P(E) est vide.

Ça a rien à voir avec LA RECHERCHE en TDE qui s'occupe de l'autre bout beaucoup plus en amont : bataille sur les axiomes forts et intuitifs

christophe c · December 2020

J'ai été interrompu. Oui je disais donc que catégories, typages codes correcteurs d'erreurs etc bref l'installation de balises diverses ou de traduction diverses vont plus être attaqués par les outils récents comme le catégorisme.

La TDE version recherche est plus dans "la recherche de l'inconnu, le scan de "la nature de Dieu", par exemple via les GC qui "touchent" 0=1.

C'est très complémentaire et différent. Par exemple l'axiome du choix a une place en amont completement unique dont la nature est pas encore très bien comprise. La TDE n'y est pour rien, car elle est sans "décodage". On dit les choses comme elles sont, il n'y a pas de modélisation. D'où l'extraction des "essentiels". Par contre le prix à payer est que "c'est donné".

umrk · December 2020

christophe, le seul être humain capable de rédiger une thèse de Maths sur un téléphone portable ! (c'est admiratif, bien sûr !)

Martial · December 2020

@umrk : "christophe, le seul être humain capable de rédiger une thèse de Maths sur un téléphone portable ! "

Et encore, ce que tu ne sais pas c'est qu'au moment où il la rédige sur son téléphone elle est déjà complètement écrite dans sa tête...

axexe · December 2020

Pour ceux qui veulent faire un peu de logique catégorique, un polycopié d'Alain Prouté remarquable (comme tous ses poly).
Parler de ces choses c'est bien... Si on les maitrise...

Il veut dire quoi Lafforgue au juste, concrêtement?

La théorie des ensembles comme fondation, chacun son avis.
La théorie des ensembles comme discipline, il y a assez de problèmes ouverts pour occuper des chercheurs pendant encore pas mal de temps.

Ça fait 10 ans que j'entends parler des topos comme un remêde miracle. En 10 ans, je n'ai rien vu.

Martial · December 2020

@axexe : "La théorie des ensembles comme fondation, chacun son avis."
Tu connais le mien.

"La théorie des ensembles comme discipline, il y a assez de problèmes ouverts pour occuper des chercheurs pendant encore pas mal de temps."
Ouais, genre encore un millions d'années, au grand minimum !

axexe · December 2020

Lol, un cardinal mesurable d'année.

Moi au sujet des fondations, je n'ai pas trop d'avis encore tranché, vu que je n'ai rien vu d'autres (si les topos, mais c'est une blague ce truc).

Edit: je laisse mon message, mais enlève de ma tête que les topos sont une blague.

christophe c · December 2020

Le côté fondationnel de la TDE est pas un choix mais une évidence. Cela provient du fait que l'on a remplacé par \in l'espace entre les mots.

(Médor mange) = (Médor \in mangeant)

De mon téléphone.

Maxtimax · December 2020

axexe : tu as un avis sur HoTT ?

axexe · December 2020

Commentaire à démonter s'il le faut, je n'ai rien prouvé moi même et cela date de 5 ans...

Je n'ai pas d'avis sur HoTT Max (je pense que c'est proche de ton domaine ou pas... mais si il y a quelqu'un pour donner son avis, ce n'est pas moi) par méconnaissance totale du sujet.
J'ai modifié mon avis sur les topos car ce n'est pas le mien mais j'ai laissé le message.

J'avais suivis un seul groupe de travail sur Paris en 2015 et c'est vraiment des souvenirs qui datent (j'attendais le groupe de travail sur les groupes) et le sud du sud du 13ème arrondissements n'est pas propice à la balade quand il pleut.

Il y a un premier problème selon (d'autres) lol c'est que l'on "confond" théorie des types et théorie des catégories.
Les 2 peuvent être considérées comme des théories de fonctions. Mais la théorie des catégories est plus dans la composition de fonctions, alors que la théorie des types va "capturer" une fonction.
Les deux types de théories peuvent être mises en relation par des procédés astucieux mais je n'ai(j'ai dû faire la faute 30 fois...@AD) pas envie de raconter trop de conneries lol. Les choses ont-elles changées depuis ?

Tout comme ZF+DC est plus forte que Z.
La théorie des types est plus forte de HoTT.
La théorie des topos est plus forte que la théorie des catégories.

Après je ne sais pas si quelqu'un aura un jour les outils pour comparer la force logique de HoTT, la théorie des catégories et ZF+DC ("reverse mathématique").
Perso, c'est ce qui m’intéresse.

Dans quel système (ZF, HoTT) on trouve la force minimal pour prouver un théorème T.

Maxtimax · December 2020

La cohérence de ZF implique la cohérence de HoTT d'après des résultats relativement récents de Shulman (2018, voire 2019)

Inversement, HoTT "contient ZF" essentiellement comme son fragment discret (les types $X$ tels que $x=_X y$ est vide ou contractile) , je crois que certaines variantes permettent essentiellement de retrouver ZF donc il ne doit pas y avoit de grosse différence en consistency strength. En reverse mathematics, pas sûr, je pense qu'il faudrait déjà donner un sens à la question !

(Oui, HoTT c'est relativement lié à ce qui m'intéresse, on peut y faire de l'homotopie synthétique si je comprends boen. Mais je ne me suis pas plongé dans les détails, je ne crois pas par exemple qu'on ait déjà de notion satisfaisante de catégorie ou d'$\infty$-catégorie, et c'est ça qu'il me faudrait)

Martial · December 2020

@axexe : je n'y connais rien mais au cas où ça puisse t'intéresser.
Benoît Monin va faire de janvier à mars un cours intitulé "Calculabilité : Outils classiques", dans le cadre du M2 LMFI, 2h/semaine (c'est crédité de 4 ECTS, c'est pour ça).
Il va parler de généralités au début, puis, selon les desiderata des étudiants, s'orienter, soit vers les mathématiques à rebours, soit vers j'sais plus quoi. (Je ne retiens que ce qui m'intéresse, et encore avec bien des difficultés).

Ceci dit je ne sais pas :
1) Si ça t'intéresse.
2) Quelle option vont choisir les étudiants.
3) Si tu habites en RP (je crois que non).
4) Si tu as la disponibilité nécessaire (je crois que non).
5) Si le cours va avoir lieu en présentiel ou par zoom (auquel cas tu pourrais demander à suivre le cours en auditeur libre à condition que tes horaires collent).

Concernant le point 5 je pense qu'à l'heure actuelle personne à Paris 7 n'en sait rien, et même Macron doit être dans le flou artistique le plus total.

Enfin, je t'aurai transmis l'info...

axexe · December 2020

Merci Max pour les infos.

Merci Martial.

J'aimerais bien suivre quelques cours du semestre 2:
Grands cardinaux
Bitcoin
Types.

Je me suis farci le poly de Prouté, autant que cela serve à quelque chose lol.

Au niveau du cours que tu me proposes en tapant le nom de l'enseignant, je tombe sur un livre avec un chapitre entier sur les mathématiques à rebours. Je suis content, en Français c'est rare... (Pour Ramsey c'est bien).

Là on est dans le plaisir.

Niveau thèse à finir:
il y a un parcours logique à l'ENS de Lyon l'an prochain qui colle parfaitement avec la tournure que je veux donner au dernier chapitre de ma thèse, c'est quand même fou. Si un logicien de Lyon (normalement c'est bon) peut m'encadrer bénévolement 6-12 mois histoire que je la présente.

Alesha · December 2020

Maxtimax a écrit:

Oui, HoTT c'est relativement lié à ce qui m'intéresse, on peut y faire de l'homotopie synthétique si je comprends boen.

Les types de HoTT proprement dit correspondent à des $\infty$-groupoïdes (tous les chemins sont inversibles). Je pense que ce qui t'intéresse et ce que tu as en tête, c'est plutôt des $(\infty, 1)$-categories. Récemment, en effet, des variantes de HoTT (essentiellement des extensions, mais des points cruciaux comme le statut de l'axiome d'univalence ou l'existence d'univers sont encore assez obscurs, au moins pour moi) ont pour but d'être une théorie des types correspondant à des $(\infty, 1)$-categories mais je crois que c'est encore au stade de la recherche.

Maxtimax · December 2020

Alesha: oui tout à fait, mais une $(\infty,1)$-catégorie c'est moralement une catégorie "enrichie faiblement en $\infty$-groupoïdes". En HoTT, le "faiblement" est automatiquement pris en compte, et donc il n'est pas impensable de définir de tels machins en HoTT même.
Riehl et Shulman y travaillent notamment, et c'est le cas de beaucoup de gens.
A vrai dire, un point qui n'est pas clair pour moi est pourquoi la définition naïve de "catégorie" qu'on pourrait donner en HoTT ne convient pas (pour modéliser des $(\infty,1)$-catégories), mais j'ai peur qu'il faille se plonger dans les détails pour avoir une réponse.

Alesha · December 2020

L'article de Riehl et Shulman, ce n'est pas du HoTT proprement dit. Regarde les contextes des jugements : tu as des cubes et des topes, ce que tu n'as pas dans HoTT; Riehl et Shulman, c'est une "extension" de HoTT (mais a priori sans l'axiome d'univalence et sans univers, si j'ai bien compris, en tout cas dans cet article).

Maxtimax · December 2020

Alesha: oui tu as raison !
Tu aurais une explication rapidos (même si incomplète) de pourquoi le truc naïf ne marche pas ?

Alesha · December 2020

Maxtimax a écrit:

A vrai dire, un point qui n'est pas clair pour moi est pourquoi la définition naïve de "catégorie" qu'on pourrait donner en HoTT ne convient pas (pour modéliser des $(\infty,1)$-catégories)

Dans HoTT, étant donné un type A et deux éléments a et a' de type A, tu peux former un type des chemins de a vers a', mais tous ces chemins sont inversibles. Dans Riehl et Shulman, tu as une construction (via des "extensions de types") qui permet de considérer le type hom_A(a, a') (et tu as une fonction canonique des chemins au sens de HoTT de a vers a' vers hom_A(a, a')) dans le but d'avoir une correspondance entre les types (au moins ceux qui sont Segal) et les $(\infty,1)$-catégories. Je crois que ce tu dis est que l'on pourrait définir un type des $(\infty,1)$-catégories dans HoTT (je ne suis pas sûr d'avoir bien compris), mais c'est différent d'avoir une correspondance entre types et $(\infty,1)$-catégories.

Maxtimax · December 2020

Alesha: oui je veux définir un tel type, pas une correspondance. Pire, je ne veux pas de correspondance ! Je suis bien content avec des types comme $\infty$-groupoïdes, et après je voudrais définir dedans les $\infty$-catégories, pour lesquelles il y a une définition naïve "évidente", et je ne suis pas sûr de ce qui ne marche pas. Il est possible que même si tout est bien fait, requérir uniquement l'associativité ne permette pas automatiquement (par de la "magie HoTT") de récupérer les cohérences supérieures ?

christophe c · December 2020

De mon téléphone pour les passants.

Opinion personnelle : même si ça ne change rien ke suis personnellement hostile au choix politique de JoTT d'avoir popularisé ses outils en présentant les ensembles comme des cas particuliers d'objet. Le niveau de la France est celui de la Roumanie en maths école, et berner les gens ne me paraît pas efficace même si je comprends les volontés d'accès aux crédits.

Il fait savoir qu'à peu près tout objet est un cas particulier de tout autre objet dès que des conditions très simples sont réunies. Les slogans de vente trompeurs ont comme inconvénients de faire oublier, voire de cacher ça et de faire partir les gens sur de mauvaises bases des le départ.

La différence OPERATOIREMENT essentielle entre le catégorisme qui étudie un fragment de science très consistant et l'ensemblsme qui spécule à la frontière de l'inconsistance (ie limites de Dieu) est que dans un cas fondamentalement on ne souhaite pas identifier A avec 1=>A. Alors que dans l'autre si.

Cette identification (qu'on pourrait qualifier de positionnement-en-platonisme) ne sert pas tant à étudier les théories faibles qu'à éviter la verbosite de qui risque de tout noter dans les théories fortes et speculantes.

Il est à noter que des les catégories CCC, sans être vraiment faite, elle est néanmoins partiellement importée. Les topos ne sont qu'une cerise sur gâteau du CCC-isme.

On a des intervenants célèbres sur le forum (je parle de fdp par exemple) qui, bien que certes ne connaissant pas ça, se rangeraient (au conditionnel) à l'option de traiter A,B d'une part et A=>B d'autre part comme d'une nature différente.

Martial · December 2020

@axexe : peux-tu me dire en 2 mots quel est le sujet de ta thèse ?
(Bon, s'il y a 150 mots je prends aussi).

axexe · December 2020

@Martial
Je n'avais pas vu ton message.
Je vais essayer de faire un petit résumé lisible pour un non spécialiste des 2 domaines. (L'intro de ma thèse quoi :-D)
Par MP par contre.

Martial · December 2020

@axexe : merci d'avance, c'est sympa.

A propos de spécialistes, il y a un seul énoncé dont je suis convaincu :

$$\forall D, domaine(D) \Rightarrow \neg(\text{ je suis spécialiste de } D),$$
lol.

axexe · December 2020

Mdr (Pas envie d'écrire je suite morte de rire)

Martial · December 2020

@axexe : "morte de rire".
C'est une faute de frappe ou ça reflète la vérité ?
(T'es pas obligé de répondre , lol).

axexe · December 2020

Suspense...
Mattar l'entretien bien aussi ;-).
Faute de frappe.

Martial · December 2020

@axexe : Mattar ?

axexe · December 2020

Début du HS

La majorité des personnes sur le forum, on se connait pas leur sexe...
Et c'est tant mieux lol.
C'est Christophe qui entrenenait le suspense sur le genre de Mattar (le boss de ce forum).
Et pour compliquer le tout, la personne dont je respecte le plus la thèse est transgenre...

Fin du HS.

Par contre tu penses changer la mise en page Latex de ton livre? Car j'ai l'impression qu'elle est différente de la standart.
Si c'est un choix, c'est ton livre, je n'ai pas à juger.

Martial · December 2020

@axexe : qu'est-ce qui va pas dans ma mise en page latex ?

Tu as le temps pour répondre, l'éditeur c'est pas pour demain, lol.

Poirot · December 2020

@Martial : c'est vrai qu'il y a un truc déplaisant au niveau de ta mise en page $\LaTeX$. J'imagine que tu n'as pas envie de tout recompiler maintenant, mais il faudra y penser un jour si tu veux attirer plus de lecteurs ! Je ne saurai pas décrire précisément le problème, mais il me semble que les caractères sont plus fins que dans la plupart des documents TeX auxquels on est habitué, et la police n'a pas l'air d'être la police standard (on dirait un peu du Word).

nicolas.patrois · December 2020

Personnellement, je veux bien avoir l’ignaritude d’umrk. :-D

Martial · December 2020

@Poirot et Tous : voici mon préambule. Peut-être un spécialiste pourra-t-il me dire ce qui ne va pas.
Pour l'instant je gère les chaps un par un, et c'est seulement à l'étape finale que je fusionnerai tout ça, donc ça ne serait pas un problème de tout recompiler... sauf évidemment si ça me nique complètement ma mise en page :

\documentclass[12pt]{article}

\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage[utf8]{inputenc}
\usepackage[french]{babel}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{graphicx}
\usepackage{epsfig}
\usepackage{float}
\usepackage{dsfont}
\usepackage{babel}
\usepackage{tikz,tikzsymbols,pgf}
\usepackage{bbold}
%\usepackage{bbold-type1}
\usepackage{mathrsfs}

\usetikzlibrary{positioning, arrows.meta}

\newtheorem{theorem}{Th\'eor\`eme}
\newtheorem{acknowledgement}[theorem]{Acknowledgement}
\newtheorem{algorithm}[theorem]{Algorithme}
\newtheorem{axiom}[theorem]{Axiome}
\newtheorem{case}[theorem]{Cas}
\newtheorem{claim}[theorem]{Objectif}
\newtheorem{conclusion}[theorem]{Conclusion}
\newtheorem{condition}[theorem]{Condition}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{corollary}[theorem]{Corollaire}
\newtheorem{criterion}[theorem]{Crit\`ere}
\newtheorem{definition}[theorem]{D\'efinition}
\newtheorem{example}[theorem]{Exemple}
\newtheorem{exercise}[theorem]{Exercice}
\newtheorem{lemma}[theorem]{Lemme}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{problem}[theorem]{Probl\'eme}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{remark}[theorem]{Remarque}
\newtheorem{solution}[theorem]{Solution}
\newtheorem{summary}[theorem]{Résumé}
\newenvironment{proof}[1][Preuve]{\textbf{#1.} }{\ \rule{0.5em}{0.5em}}

\usepackage[a4paper]{geometry}
\geometry{verbose,tmargin=3cm,bmargin=3cm,lmargin=3.5cm,rmargin=3cm,headheight=1cm,headsep=1cm}

Poirot · December 2020

Je ne sais pas si le "problème" se situe dans le préambule, c'est peut-être plutôt dans les paramètres de ton compilateur TeX, qu'est-ce que tu utilises comme logiciel ?

Martial · December 2020

J'utilise MiKTeX avec TeXStudio sous windows... oui, je sais, pas très pro.

Question d'un ignare

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 29