
 
 Auteur : Kevin Buzzard Auteur : Kevin Buzzard Table Of Links Table de gauche abstrait 
 
 Reconnaissance & Introduction Reconnaissance & Introduction 2. Universal properties 2 - Propriétés universelles 3. Products in practice Les produits en pratique 4. Universal properties in algebraic geometry Propriétés universelles en géométrie algébrique 5. The problem with Grothendieck’s use of equality. Le problème avec l’usage de l’égalité de Grothendieck. 6. More on “canonical” maps Plus sur les cartes « canoniques » 7. Canonical isomorphisms in more advanced mathematics Isomorphismes canoniques en mathématiques plus avancées 8. Summary And References 8 Résumé et références Abstract abstrait Nous discutons de la façon dont le concept d'égalité est utilisé par les mathématiciens (y compris Grothendieck), et quel effet cela a quand on essaie de formaliser les mathématiques. Overview Beaucoup d'objets et de constructions mathématiques sont uniquement caractérisés par une sorte de propriété définissante. Par exemple, les nombres réels sont le champ d'ordre archimédien complet unique, et de nombreuses constructions en algèbre (localisations, produits de tensor. . . ) et en topologie (produit d'espaces topologiques, achèvement d'un espace métrique ou uniforme. . . ) sont caractérisées uniquement par une propriété universelle. Pour être plus précis, je voudrais discuter des propriétés qui définissent un objet mathématique jusqu'à l'isomorphisme unique. Il n'y a qu'un seul tel groupe, jusqu'à l'isomorphisme, cependant ce groupe a des automorphismes (par exemple la carte envoyant un élément à son carré), ce qui signifie qu'il est unique mais seulement jusqu'à l'isomorphisme non unique, et par conséquent la propriété d'être un groupe de l'ordre 5 n'est pas le type de propriété dont parle ce document. Vous pouvez (et devriez probablement) développer la théorie des objets caractérisés par P en utilisant seulement l'hypothèse P, et vous n'avez pas besoin de vous soucier de toute construction particulière de l'objet (au-delà de savoir qu'il existe une construction qui satisfait P, et donc que votre théorie n'est pas vide). Assertion 1. Tous les deux objets mathématiques satisfaisant P peuvent en pratique être présumés égaux, car toute affirmation mathématiquement significative satisfaite par l'un est également satisfaite par l'autre. Assertion 2. Plus généralement, si vous avez deux objets qui sont canoniquement isomorphes, alors ces objets peuvent en pratique être présumés égaux. Assertion 3. Considérons un exemple. Bien qu'il existe plusieurs constructions différentes des nombres réels des rationaux (séquences de Cauchy, coupes de Dedekind, finition de l'espace uniforme de Bourbaki. . . . ), toute l'analyse de base enseignée dans un premier cours de premier cycle est développée en utilisant uniquement les axiomes d'Archimède et de complétude satisfaits par les nombres réels. Un mathématicien ne rêverait pas de dire quelle définition des nombres réels ils utilisaient - ce serait absurde. En effet, Newton, Euler et Gauss utilisaient heureusement "les" nombres réels bien avant que Cauchy, Dedekind et Bourbaki ne viennent avec leurs différents modèles: chacune de leurs définitions du champ ordonné R est uniquement isom Je dirai plus sur les localisations plus tard, mais il y a aussi plusieurs constructions différentes de la localisation R[1/S] d'un anneau commutatif à un sous-ensemble multiplicatif (un quotient de R×S, un quotient d'un anneau polynomial multivariable. . . ) et un mathématicien ne dirait jamais exactement quelle construction ils utilisent lorsqu'ils écrivent R[1/S] ; nous savons que cela n'a pas d'importance. Dans ce document, je soutiens que la première affirmation ci-dessus est fausse, la seconde est dangereuse, et la troisième est sans sens. Les affirmations 2 et 3 semblent être utilisées dans de nombreux endroits dans la littérature de la géométrie algébrique - en effet, nous allons discuter de l'utilisation du symbole de Grothendieck dans une certaine profondeur plus tard. Cependant, en tant que mathématicien travaillant, je suis également conscient qu'il y a quelque chose de plus profond ici, que je trouve difficile de mettre mon doigt sur. Le concept selon lequel deux objets sont canoniquement isomorphes et peuvent donc être identifiés est extrêmement important dans la pratique ; c’est un principe d’organisation utile, il réduit la charge cognitive, et il n’introduit pas en pratique des erreurs dans les arguments, au moins si l’auteur sait ce qu’ils font. De même, faire des définitions et prouver des théorèmes sur les objets en utilisant une construction explicite plutôt que la propriété universelle est un outil pratique qui est utilisé à travers les mathématiques (par exemple, choisir une base d’un espace vectoriel pour faire une définition et observer que la définition est indépendante du choix). Disons que l’on essaie de formaliser certaines mathématiques sur un ordinateur (c’est-à-dire de traduire les mathématiques de la littérature papier dans le langage d’un échantillon de théorème interactif – un programme informatique qui connaît les axiomes des mathématiques et les règles de la logique). Lorsqu’on est forcé d’écrire ce que l’on veut réellement dire et qu’on ne peut pas se cacher derrière des mots mal définis comme « canonique », ou des affirmations selon lesquelles les choses inégales sont égales, on trouve parfois qu’on doit faire du travail supplémentaire, ou même réfléchir à la manière dont certaines idées devraient être présentées. En effet, parfois, la façon la plus indolore de faire ce travail consiste à avoir à créer de nouvelles idées mathématiques qui ne sont pas présentes dans les arguments papier. Avec l'avènement de la formalisation des mathématiques autour de la géométrie algébrique et arithmétique en utilisant des échantillons de théorèmes informatiques, par exemple le travail sortant de la communauté des échantillons Lean ([BCM20], [Liv23], [dFF23], [AX23], [Zha23], . . . ) et les travaux connexes dans Isabelle ([BPL21]) et Agda cube ([ZM23]), ces choses commenceront à avoir de l'importance. 
 
 Ce document est disponible sous la licence CC BY 4.0 DEED. Ce papier est sous licence CC BY 4.0 DEED. Disponible dans les archives Disponible dans les archives

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

MediaBias.TECH

We publish deeply researched (and often vastly underread) academic papers about our collective omnipresent media bias.

MediaBias's

Cet audio est produit dans la langue originale de l'histoire !

Grothendieck, L'égalité et la difficulté de formaliser les arguments mathématiques

About Author

COMMENTAIRES

ÉTIQUETTES

CET ARTICLE A ÉTÉ PARU DANS

Related Stories

Libérer la puissance de l’IA. Une revue systématique des techniques de pointe : résumé et introduction

Télégramme : le pont de Crypto Island vers le continent

Naviguer sur les eaux : développer des applications RAG de qualité production avec des lacs de données

HackerNoon Decoded: The Top 10 Countries Where HackerNoon Is the Most Active

Libérer la puissance de l’IA. Une revue systématique des techniques de pointe : résumé et introduction

Télégramme : le pont de Crypto Island vers le continent

Naviguer sur les eaux : développer des applications RAG de qualité production avec des lacs de données

HackerNoon Decoded: The Top 10 Countries Where HackerNoon Is the Most Active

Light-Mode

Classic

Newspaper

Minty

Dark-Mode

Neon Noir

Minty

HN StartUps