Formalization in Lean of faithfully flat descent of projectivity

Dit artikel presenteert een formalisatie in Lean van het fundamentele resultaat in de commutatieve algebra dat een $R$-module projectief is dan en slechts dan als zijn uitbreiding via een getrouw platte ringhomomorfisme projectief is, waarmee een subtiel hiaat in het klassieke werk van Raynaud en Gruson wordt opgelost.

De kern

Stel je voor dat wiskunde een enorme, ingewikkelde stad is. In deze stad zijn er gebouwen (de ringen) en er zijn mensen die erin wonen (de modules). Soms willen wiskundigen weten of een bepaald gebouw "stabiel" is (projectief). Dat is een heel belangrijk kenmerk, want stabiele gebouwen zijn makkelijker te bouwen en te repareren.

Deze paper vertelt het verhaal van een wiskundige (Liran Shaul) die een oude, beroemde maar gebrekkige brug tussen twee steden heeft gerepareerd en vervolgens in een computerprogramma (Lean) heeft nagebouwd om te bewijzen dat hij echt werkt.

Hier is het verhaal in gewone taal:

1. Het Grote Probleem: De Gebrekkige Brug

In de jaren '70 schreven twee grote wiskundigen (Raynaud en Gruson) een heel belangrijk artikel. Ze bewezen dat als je een gebouw in de ene stad (R) hebt, en je het "verplaatst" naar een andere, grotere stad (S) via een speciale, onbreekbare brug (een faithfully flat kaart), je kunt zien of het gebouw stabiel is door alleen naar de kopie in de nieuwe stad te kijken.

• De regel: Als de kopie in de nieuwe stad (S) stabiel is, dan was het origineel in de oude stad (R) ook al stabiel.
• Het probleem: De originele brug had een klein, onzichtbaar gat. Het bewijs leek perfect, maar er zat een foutje in. Later ontdekten anderen dit, maar niemand had het officieel en onweerlegbaar opgelost.

2. De Oplossing: De Computer als "Super-Check"

Liran Shaul heeft besloten dit gat te dichten. Maar hij deed het niet alleen met pen en papier. Hij gebruikte Lean, een computerprogramma dat als een super-strict controleur fungeert. Lean laat geen enkele fout toe; als je een stap niet perfect kunt uitleggen, stopt het programma.

Hij heeft de hele brug, inclusief alle fundamenten, opnieuw gebouwd in de computer. Het resultaat? De brug is nu 100% veilig. Het bewijs is nu "geformaliseerd", wat betekent dat een computer het heeft nagelopen en bevestigd: "Ja, dit klopt echt."

3. De Gereedschapskist: Hoe bouw je zo'n brug?

Om deze brug te bouwen, moest Shaul eerst heel veel nieuw gereedschap maken, omdat het bestaande gereedschap (in de computerbibliotheek Mathlib) ontbrak. Hij gebruikte een paar slimme metaforen:

• De "Kaplansky-ontleding" (Het Legpuzzel):
  Stel je voor dat je een enorm, onoverzichtelijk gebouw moet controleren. Dat is te lastig. Shaul gebruikte een truc van de wiskundige Kaplansky: hij brak het enorme gebouw op in kleine, beheersbare stukjes (stukjes die "telfbaar" zijn, zoals een rij bakstenen). Als je kunt bewijzen dat elk klein stukje stabiel is, dan is het hele gebouw stabiel. Dit noemen ze een devissage (ontleding).

• De "Mittag-Leffler" (De Stabiele Stroom):
  Dit is een technisch concept, maar stel je voor dat je een rivier hebt waar water doorheen stroomt. Soms stopt de stroom of wordt hij chaotisch. Een "Mittag-Leffler-module" is als een rivier die altijd een stabiele, voorspelbare stroom heeft, zelfs als je hem van dichtbij bekijkt. Shaul bewees dat als een gebouw stabiel is, het ook deze "stabiele stroom" heeft.

• De "Pushout" (Het Samenvoegen):
  Stel je voor dat je twee wegen wilt samenvoegen tot één grote weg. In wiskunde heet dit een pushout. Shaul bouwde een computermodel dat precies laat zien hoe je twee wegen veilig kunt samenvoegen zonder dat er gaten ontstaan. Dit was cruciaal om te bewijzen dat de eigenschappen van de ene stad overgaan naar de andere.

• De "Universaal Injectieve" (De Onbreekbare Telefoonlijn):
  Dit is een manier om te zeggen dat informatie perfect overgedragen wordt, zonder dat er iets verloren gaat, zelfs als je de boodschap door een heel complex systeem stuurt. Shaul bewees dat als deze "telefoonlijn" in de nieuwe stad werkt, hij ook in de oude stad werkt.

4. Het Eindresultaat: Waarom is dit belangrijk?

Dit werk is niet alleen een technische prestatie voor computers. Het is een fundamentele bouwsteen voor de wiskunde.

• Betrouwbaarheid: Omdat een computer het heeft nagelopen, weten we nu met 100% zekerheid dat de theorie klopt. Er zijn geen twijfels meer over dat oude gat in het bewijs.
• Toekomst: Deze bewijzen zijn nu beschikbaar voor andere wiskundigen en computers. Ze kunnen deze "brug" gebruiken om nog complexere problemen op te lossen, zoals het bestuderen van de "finitistische dimensie" (een maatstaf voor hoe complex een wiskundig systeem kan worden).

Kort samengevat:
Liran Shaul heeft een beroemde, maar gebrekkige wiskundige theorie over "stabiele gebouwen" volledig opnieuw opgetrokken in een computer. Hij heeft daarvoor nieuwe gereedschappen (zoals puzzelstukjes en stabiele rivieren) uitgevonden en bewezen dat de theorie waterdicht is. Het is alsof hij een oude, beroemde brug heeft laten keuren door de strengste inspecteur ter wereld en nu zegt: "Kijk, hij is veilig, jullie kunnen eroverheen lopen!"

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "Formalization in Lean of Faithfully Flat Descent of Projectivity" van Liran Shaul, geschreven in het Nederlands.

Titel: Formalisatie in Lean van de Getrouwe Vlakke Afdaling van Projectiviteit

Auteur: Liran Shaul
Context: Commutatieve algebra, Formele verificatie (Lean 4/Mathlib).

---

1. Het Probleem

Het paper richt zich op de formele verificatie van een fundamenteel resultaat in de commutatieve algebra, bekend als Theorema I (oorspronkelijk uit het invloedrijke werk van Raynaud en Gruson [7]):

Laat $R \to S$ een getrouw vlakke (faithfully flat) afbeelding zijn van commutatieve ringen (niet noodzakelijk Noethers) en laat $P$ een willekeurige $R$-module zijn. Dan is $P$ projectief over $R$ dan en slechts dan als $S \otimes_R P$ projectief is over $S$.

Achtergrond en Motivatie:

• Dit resultaat is cruciaal voor het bewijs van de stelling dat de "finitistische dimensie" van een commutatieve Noetherse ring gelijk is aan haar Krull-dimensie.
• De originele bewijsvoering in [7] bevatte een subtiel gat, dat later werd opgemerkt door Gruson [3].
• Een volledig bewijs werd later gepubliceerd in [6] en opgenomen in het Stacks Project [1], maar dit was nooit formeel geverifieerd door een peer-review proces of een bewijshulpmiddel.
• Het doel van dit paper is om dit resultaat, samen met alle noodzakelijke voorveronderstellingen, volledig te formaliseren in Lean 4 met behulp van de Mathlib-bibliotheek.

---

2. Methodologie

De auteur heeft een systematische ontwikkeling van nieuwe wiskundige concepten en structuren in Lean 4 doorgevoerd, aangezien deze niet eerder beschikbaar waren. De totale code omvat meer dan 10.000 regels.

Belangrijkste methodologische pijlers:

1. Kaplansky Devissage: Het reduceren van het probleem naar het geval van modules die gegenereerd worden door een aftelbare verzameling. Dit vereiste de formalisatie van transfinite filtraties (geordend door ordinalen).
2. Mittag-Leffler Voorwaarde: Een uitgebreide behandeling van de Mittag-Leffler-voorwaarde voor inverse systemen en modules, inclusief equivalenties tussen verschillende definities.
3. Pushouts en Universale Injectiviteit: De constructie van pushouts in de categorie van modules en het formaliseren van "universally injective" kaarten, essentieel voor het begrijpen van dominantie tussen lineaire afbeeldingen.
4. Transfinite Inductie: Het gebruik van ordinaalgetallen om een filtratie van een willekeurige module te construeren, waarbij elke opeenvolgende quotiënt aftelbaar gegenereerd is.
5. Gebruik van LLM's: De auteur erkent het gebruik van grote taalmodellen (Claude Opus 4.5 en 4.6) bij het genereren van delen van de Lean-code.

---

3. Belangrijkste Bijdragen en Geformaliseerde Resultaten

Het paper presenteert de formalisatie van twee centrale stellingen en de brug die ze verbindt:

A. Theorema II: Karakterisering van Projectieve Modules

De auteur formaliseert een stelling (gebaseerd op [6, Theorem 7.4]) die projectiviteit karakteriseert via drie voorwaarden:
Een $R$-module $P$ is projectief dan en slechts dan als:

1. $P$ is vlak (flat) over $R$.
2. $P$ is een Mittag-Leffler-module over $R$.
3. $P$ is een directe som van aftelbaar gegenereerde $R$-modules.

• Kaplansky's Stelling: Het paper bewijst ook dat elke projectieve module een directe som is van aftelbaar gegenereerde projectieve modules (een klassiek resultaat van Kaplansky), wat essentieel is voor punt 3.
• Lazard's Stelling: De formalisatie omvat het bewijs dat elke vlakke module een directe limiet is van eindig gegenereerde vrije modules.

B. Theorema I: Getrouwe Vlakke Afdaling (Faithfully Flat Descent)

Dit is het hoofddoel van het paper. Het bewijs verloopt in twee fasen:

1. Het Aftelbare Geval: Als $S \otimes_R P$ projectief is en $P$ is aftelbaar gegenereerd, dan is $P$ projectief. Dit wordt bewezen door de projectiviteitscriterium (lift-eigenschap) toe te passen op een inverse limiet van Hom-sets, gebruikmakend van de surjectiviteit van inverse limieten voor Mittag-Leffler-systemen (Theorema 5.2).
2. Het Algemene Geval: Voor willekeurige modules wordt een Kaplansky-devissage (filtratie) geconstrueerd via transfinite recursie. Hierbij wordt aangetoond dat elke stap in de filtratie een aftelbaar gegenereerde projectieve quotiënt heeft. Omdat de eigenschap "projectief" behouden blijft onder directe sommen, volgt de projectiviteit van $P$.

C. Technische Lemmata en Concepten

De auteur heeft diverse sub-resultaten geformaliseerd die op zichzelf waardevol zijn voor de wiskundige bibliotheek:

• Pushout Isomorfisme: Bewijs dat de pushout commuteert met tensorproducten (basisschakeling).
• Dominantie: Formalisatie van het concept waarbij een lineaire afbeelding $g$ een afbeelding $f$ "domineert" (ker($f \otimes id$) $\subseteq$ ker($g \otimes id$)), en de equivalentie met het factoren door een afbeelding.
• Mittag-Leffler Inverse Systemen: Bewijs dat een Mittag-Leffler inverse systeem over een aftelbare gerichte indexset een niet-lege inverse limiet heeft.
• Afdaling van Eigenschappen: Bewijs dat de eigenschappen "Mittag-Leffler" en "aftelbaar gegenereerd" worden "teruggekaatst" (reflected) door getrouw vlakke afbeeldingen.

---

4. Resultaten en Implementatie

• Code: Alle code is beschikbaar in het repository [8] (lib/Kap.lean, lib/Lazard.lean, lib/Pushout.lean, lib/UnivInj.lean, lib/mlSystem.lean, lib/Domination.lean, lib/mlModule.lean, basechange.lean).
• Compilatie: Alle resultaten zijn succesvol gecompileerd met Lean 4 en Mathlib.
• Status: De auteur heeft de intentie om deze formalisaties in te dienen voor opname in de officiële Mathlib-bibliotheek.

---

5. Betekenis en Impact

• Verificatie van Klassieke Wiskunde: Dit werk sluit een gat in de historische literatuur door een bewijs dat decennia lang als correct werd beschouwd, maar nooit formeel was geverifieerd, nu volledig te verifiëren. Het bevestigt de correctheid van de "fix" die Perry en anderen hebben aangebracht op het originele werk van Raynaud en Gruson.
• Uitbreiding van Mathlib: Het paper introduceert complexe concepten (zoals transfinite devissage, Mittag-Leffler modules in de context van niet-Noetherse ringen, en pushouts) die nu beschikbaar zijn voor toekomstig onderzoek in de formele wiskunde.
• Methodologische Voorbeeld: Het demonstreert hoe moderne formele hulpmiddelen (Lean) kunnen worden gebruikt om diepe, technische problemen in de commutatieve algebra op te lossen die te complex zijn voor handmatige verificatie van elk detail.
• Toepassing: Het resultaat is een sleutelcomponent voor het bestuderen van de finitistische dimensie van commutatieve Noetherse ringen, een centraal onderwerp in de homologische algebra.

Kortom, dit paper vertegenwoordigt een mijlpaal in de formalisatie van commutatieve algebra, waarbij een diep theoretisch resultaat niet alleen wordt geverifieerd, maar ook de basis legt voor verdere formalisaties in dit domein.