Formalization in Lean of faithfully flat descent of projectivity

Cet article présente la formalisation en Lean du résultat fondamental de descente fidèlement plate de la projectivité, qui corrige une lacune subtile dans l'œuvre classique de Raynaud et Gruson en démontrant qu'un module $P$ est projectif sur $R$ si et seulement si $S\otimes_R P$ l'est sur $S$ pour tout morphisme fidèlement plat $R \to S$.

L'essentiel

🧱 Le Grand Puzzle : Quand l'architecture d'un bâtiment reste solide après un déménagement

Imaginez que vous êtes un architecte qui travaille sur des bâtiments (ce sont des anneaux en mathématiques) et leurs structures internes (ce sont des modules).

Le problème central de ce papier est le suivant : Comment savoir si une structure est parfaitement solide (ce qu'on appelle "projective") sans avoir à tout construire d'abord ?

En mathématiques, vérifier la solidité d'une structure complexe est souvent très difficile. Mais il existe une astuce : si vous pouvez construire une copie de votre bâtiment dans un autre univers (un univers plus grand, plus facile à explorer) et que cette copie est solide, alors votre bâtiment original l'est aussi. C'est ce qu'on appelle la descente fidèlement plate.

L'auteur, Liran Shaul, a pris cette idée, qui est un pilier des mathématiques du XXe siècle, et l'a codée dans un langage informatique appelé Lean. Pourquoi ? Parce que les humains font des erreurs, mais un ordinateur, lui, ne se trompe jamais. Il a vérifié chaque brique de la preuve pour s'assurer qu'il n'y avait aucune faille.

Voici les étapes de son aventure, expliquées avec des images :

1. Le Défi : Un trou dans la théorie

Il y a 50 ans, des mathématiciens géniaux (Raynaud et Gruson) avaient prouvé que si votre copie dans l'univers "S" est solide, alors votre original dans l'univers "R" l'est aussi. Mais plus tard, on a découvert un petit trou dans leur raisonnement, comme un mur mal construit dans un château. Personne n'avait vraiment vérifié la réparation proposée par un autre mathématicien (Perry) jusqu'à ce que Liran Shaul prenne le relais.

2. L'Outillage : Construire des échafaudages (Le "Devissage")

Pour réparer le mur, il faut pouvoir décomposer le bâtiment en pièces plus petites.

• L'analogie : Imaginez que vous avez un immeuble géant et infini. C'est trop dur à analyser d'un coup. L'idée de Kaplansky (un autre mathématicien) est de dire : "Si cet immeuble est fait de briques, alors n'importe quelle partie de cet immeuble peut aussi être décomposée en briques."
• En Lean : L'auteur a écrit du code pour prouver qu'on peut toujours découper un module infini en morceaux "dénombrables" (des tas de briques qu'on peut compter, même si c'est long). C'est comme avoir une règle magique qui transforme un labyrinthe infini en une série de couloirs gérables.

3. Le Test de Solidité : Le critère "Mittag-Leffler"

Comment savoir si un module est solide ? Il faut qu'il soit :

1. Plat (il ne se déforme pas quand on le plie).
2. Projectif (il est solide).
3. Mittag-Leffler (C'est le mot de passe secret !).

L'analogie du "Mittag-Leffler" :
Imaginez que vous envoyez un message à travers un système de relais (une chaîne de personnes).

• Si le message se perd ou se déforme à chaque étape, le système est mauvais.
• Si le système est "Mittag-Leffler", cela signifie qu'après un certain nombre d'étapes, le message se stabilise. Peu importe combien de relais vous ajoutez après, le message final ne change plus. C'est une garantie de stabilité.
• L'auteur a codé cette notion de "stabilisation" pour s'assurer que les mathématiques fonctionnent comme prévu.

4. Le Pont Magique : Les "Pushouts"

Pour comparer les deux mondes (R et S), il faut construire un pont. En mathématiques, ce pont s'appelle un pushout.

• L'analogie : C'est comme prendre deux pièces de puzzle (B et C) qui partagent un bord commun (A) et les coller ensemble pour former une nouvelle pièce (D).
• L'auteur a prouvé que si vous faites ce collage dans le monde "R" et que vous l'exportez dans le monde "S", le résultat est exactement le même. C'est crucial pour s'assurer que les propriétés ne se perdent pas lors du transfert.

5. La Preuve Finale : Le grand saut

Une fois tous ces outils construits (les échafaudages, le test de stabilité, le pont), l'auteur assemble le tout :

1. Il prend un module infini.
2. Il le découpe en petits morceaux (grâce à Kaplansky).
3. Il vérifie que chaque petit morceau est solide dans le monde "S" (l'hypothèse de départ).
4. Grâce à la "descente fidèlement plate", il prouve que si les morceaux sont solides dans "S", ils le sont aussi dans "R".
5. Il recolle les morceaux : si tous les morceaux sont solides, l'ensemble l'est aussi.

Pourquoi est-ce important ?

Ce papier ne sert pas juste à résoudre une énigme mathématique obscure.

• Fiabilité : En codant tout cela dans Lean, l'auteur a éliminé tout doute. C'est une preuve incontestable.
• Applications : Cela aide à comprendre la "dimension" des anneaux commutatifs, ce qui est fondamental pour la cryptographie, la physique théorique et l'informatique quantique.
• L'avenir : C'est un exemple de comment l'intelligence artificielle (l'auteur a utilisé des modèles de langage pour aider à écrire le code) et les mathématiques rigoureuses peuvent collaborer pour construire des connaissances inébranlables.

En résumé : Liran Shaul a pris une théorie mathématique complexe, un peu comme un vieux plan d'architecte avec une erreur, et a utilisé un ordinateur ultra-précis pour le corriger, le vérifier brique par brique, et prouver que la structure tient parfaitement debout, même dans l'infini.

Résumé technique

Voici un résumé technique détaillé de l'article « Formalization in Lean of Faithfully Flat Descent of Projectivity » de Liran Shaul, rédigé en français.

1. Problématique et Contexte

L'article traite de la formalisation dans le langage de preuve Lean 4 (avec la bibliothèque Mathlib) d'un résultat fondamental de l'algèbre commutative : la descente fidèlement plate de la projectivité.

Ce résultat, souvent attribué à Raynaud et Gruson (dans leur article fondateur [7]), stipule que pour un morphisme fidèlement plat $R \to S$ d'anneaux commutatifs (non nécessairement noethériens) et un $R$-module $P$ quelconque, $P$ est projectif sur $R$ si et seulement si $S \otimes_R P$ est projectif sur $S$.

Le problème spécifique :
L'article met en lumière une faille subtile dans la preuve originale de Raynaud et Gruson, identifiée plus tard par Gruson lui-même. Une preuve complète a été proposée par Perry (dans [6]) et intégrée dans le Stacks Project, mais elle n'avait jamais fait l'objet d'une révision par les pairs formelle. L'objectif de Shaul est de combler ce vide en formalisant et en vérifiant mécaniquement cette preuve, ainsi que toutes ses prérequis, dans Lean.

2. Méthodologie et Développement Technique

La formalisation a nécessité le développement de plus de 10 000 lignes de code à partir de zéro, car plusieurs concepts théoriques n'étaient pas disponibles dans Mathlib. L'approche méthodologique repose sur une décomposition structurée du problème en plusieurs modules interdépendants :

A. Développement de la Théorie des Modules

• Dévissage de Kaplansky : L'auteur formalise le théorème de Kaplansky permettant de réduire l'étude des modules projectifs à celle des modules engendrés dénombrablement. Cela implique la définition d'une structure de filtration transfinie (KaplanskyDevissage) sur les ordinaux, où chaque quotient successif est un module engendré dénombrablement.
• Théorème de Lazard : Formalisation du théorème établissant qu'un module est plat si et seulement s'il est isomorphe à une limite directe de modules libres de type fini. Cela a nécessité la construction de systèmes directs et de limites directes.
• Modules Mittag-Leffler : Définition et étude approfondie des modules Mittag-Leffler, une notion clé introduite par Raynaud et Gruson pour caractériser la projectivité.

B. Outils Catégoriels et Algébriques

• Pushouts de Modules : Implémentation concrète des pushouts dans la catégorie des modules (via des quotients de sommes directes) et preuve de leur compatibilité avec le changement de base (tensorisation).
• Applications Universellement Injectives : Définition et propriétés des applications $f: M \to N$ telles que $f \otimes \text{id}_Q$ est injective pour tout module $Q$. L'auteur prouve que cette propriété se descend le long de morphismes fidèlement plats.
• Systèmes Inverses et Condition Mittag-Leffler : Définition de la condition de Mittag-Leffler pour les systèmes inverses et preuve que la limite inverse d'un système Mittag-Leffler sur un ensemble d'indices dénombrable est non vide.

C. Stratégie de Preuve

La preuve formelle suit une logique rigoureuse :

1. Réduction au cas des modules engendrés dénombrablement via le dévissage de Kaplansky.
2. Caractérisation de la projectivité pour les modules dénombrables comme l'intersection de trois propriétés : platitude, propriété Mittag-Leffler, et décomposition en somme directe de modules dénombrables.
3. Utilisation de la descente fidèlement plate pour transférer les propriétés (Mittag-Leffler et génération dénombrable) de $S \otimes_R P$ vers $P$.

3. Résultats Clés et Théorèmes Formalisés

L'article présente plusieurs résultats majeurs formalisés, dont les énoncés exacts sont vérifiés par le compilateur Lean :

1. Théorème I (Descente de la projectivité) :
   Soit $R \to S$ un morphisme fidèlement plat. Un $R$-module $P$ est projectif si et seulement si $S \otimes_R P$ est projectif.

   • Preuve : Utilise une induction transfinie pour construire une filtration de Kaplansky, réduisant le problème au cas dénombrable, puis applique les lemmes de descente.

2. Théorème II (Caractérisation de la projectivité) :
   Un module $P$ est projectif si et seulement si :

   • $P$ est plat.
   • $P$ est Mittag-Leffler.
   • $P$ est une somme directe de modules engendrés dénombrablement.
   • Note : Ce résultat généralise le théorème de Kaplansky sur les modules projectifs et le théorème de Lazard.

3. Lemmes de Descence :

   • La propriété Mittag-Leffler se descend le long d'un morphisme fidèlement plat.
   • La génération dénombrable se descend le long d'un morphisme fidèlement plat.

4. Équivalence des conditions Mittag-Leffler :
   Preuve formelle de l'équivalence entre la définition catégorielle des modules Mittag-Leffler et leurs caractérisations via les systèmes directs (limites directes) et les systèmes inverses (limites inverses).

4. Contributions et Innovations

• Correction d'une faille historique : La formalisation valide la correction de Perry de la preuve de Raynaud-Gruson, éliminant toute ambiguïté mathématique sur ce résultat classique.
• Extension de Mathlib : L'article introduit des concepts avancés absents de la bibliothèque standard, notamment :
  • La théorie des systèmes inverses Mittag-Leffler.
  • La notion de domination entre applications linéaires.
  • Des structures de dévissage transfini utilisant les ordinaux.
• Utilisation de l'IA : L'auteur mentionne l'utilisation de modèles de langage (Claude Opus 4.5 et 4.6) pour générer une partie du code Lean, illustrant l'émergence de l'IA comme outil d'assistance dans la preuve formelle complexe.

5. Signification et Impact

Ce travail est significatif à plusieurs niveaux :

• Pour l'Algèbre Commutative : Il fournit une base vérifiée mécaniquement pour l'étude de la dimension finie des anneaux noethériens, un domaine où la descente fidèlement plate est un outil central.
• Pour la Preuve Formelle : Il démontre la capacité de Lean 4 à gérer des preuves mathématiques profondes impliquant des constructions transfinies, des limites directes/inverses et des catégories de modules non noethériennes.
• Pour la Communauté : Tous les codes sont publics et destinés à être intégrés dans Mathlib, enrichissant ainsi l'écosystème des mathématiques formelles pour les futurs chercheurs.

En résumé, Liran Shaul a réussi à transformer un résultat théorique subtil, dont la preuve originale comportait des lacunes, en une vérité mathématique rigoureusement vérifiée par ordinateur, tout en développant l'infrastructure nécessaire pour le faire.