diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb index 5f0a48424f..411d489709 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb @@ -39,32 +39,7 @@ "tags": [] }, "source": [ - "## Introduction : pourquoi Grothendieck dans une serie Lean ?\n", - "\n", - "Alexandre Grothendieck (1928-2014) a refonde la geometrie algébrique entre 1958 et 1970 autour de l'IHES (Bures-sur-Yvette), en collaboration avec Jean Dieudonne et un nombre considerable d'eleves. Son langage -- catégories, foncteurs, foncteurs derives, sites, faisceaux, schemas, topos -- a transforme l'ensemble des mathematiques. Les milliers de pages des **EGA** (Éléments de Geometrie Algébrique) et **SGA** (Seminaire de Geometrie Algébrique du Bois-Marie) sont la trace ecrite de ce programme.\n", - "\n", - "**Cet hommage ne pretend pas formaliser EGA ou SGA.** Le but est plus modeste, mais réel : **montrer comment une partie du langage grothendieckien est déjà accessible dans Mathlib 4**. Si vous suivez la serie Lean (Lean-2 a Lean-6, Lean-10 LeanDojo), vous avez vu les fondations : types dependants, propositions, tactiques, Mathlib. On va voir maintenant que ces fondations donnent acces a Grothendieck.\n", - "\n", - "### Ce que vous saurez a la fin\n", - "\n", - "1. Reconnaitre les structures categoriques de Mathlib qui implementent les idees de Grothendieck (cribles, sites, topologies de Grothendieck, faisceaux).\n", - "2. Localiser dans Mathlib les définitions de schema (`AlgebraicGeometry.Scheme`), de spectre (`Spec`), du site de Zariski et des propriétés locales de morphismes (etale, lisse, separe).\n", - "3. Distinguer ce qui est **déjà la** (exploitable pedagogiquement), ce qui est **partiel** (utile avec precautions), et ce qui est **hors-scope Mathlib 4 actuel** (cohomologie etale ℓ-adique, motifs, six opérations, GRR).\n", - "4. Lire les enonces des théorèmes grothendieckiens dans la syntaxe Lean 4 / Mathlib.\n", - "\n", - "### Prerequis\n", - "\n", - "- Familiarite avec Lean 4 et Mathlib (cf Lean-1 a Lean-6).\n", - "- Notions de base de théorie des catégories (objet, morphisme, foncteur, transformation naturelle). Aucune connaissance prealable de geometrie algébrique n'est requise pour comprendre les enonces.\n", - "- Sympathie pour le projet de **comprendre une chose en la plongeant dans le contexte le plus général qui la rend naturelle** (la phrase est de Grothendieck).\n", - "\n", - "### Duree estimée : 60 minutes\n", - "\n", - "**Note technique sur l'exécution**\n", - "\n", - "Ce notebook utilise un kernel **Python 3**. Les sources Lean sont lues directement depuis le projet `grothendieck_lean/` qui accompagne ce notebook (même repertoire). Ce projet Lake contient des modules sous `Grothendieck/` formalisant des tours pedagogiques de Mathlib (catégories, cribles, schemas, Zariski, calibration, mais aussi faisceaux, faisceautisation, cohomologie par Ext, Mayer-Vietoris et Cech). Le build (`lake build Grothendieck`) est lance en WSL via subprocess, avec vérification de l'absence de sorry. Ce pattern est emprunte aux notebooks Lean-13/16 (Kochen-Specker/Conway).\n", - "\n", - "Pour les exercices interactifs, `run_lean(snippet)` ecrit un snippet temporaire et l'exécute dans l'environnement Lake du projet, ce qui donné acces a tout Mathlib." + "## Introduction : pourquoi Grothendieck dans une serie Lean ?\n\nAlexandre Grothendieck (1928-2014) a refonde la geometrie algébrique entre 1958 et 1970 autour de l'IHES (Bures-sur-Yvette), en collaboration avec Jean Dieudonne et un nombre considerable d'eleves. Son langage -- catégories, foncteurs, foncteurs derives, sites, faisceaux, schemas, topos -- a transforme l'ensemble des mathematiques. Les milliers de pages des **EGA** (Éléments de Geometrie Algébrique) et **SGA** (Seminaire de Geometrie Algébrique du Bois-Marie) sont la trace ecrite de ce programme.\n\n**Cet hommage ne pretend pas formaliser EGA ou SGA.** Le but est plus modeste, mais réel : **montrer comment une partie du langage grothendieckien est déjà accessible dans Mathlib 4**. Si vous suivez la serie Lean (Lean-2 a Lean-6, Lean-10 LeanDojo), vous avez vu les fondations : types dependants, propositions, tactiques, Mathlib. On va voir maintenant que ces fondations donnent acces a Grothendieck.\n\n### Ce que vous saurez a la fin\n\n1. Reconnaitre les structures categoriques de Mathlib qui implementent les idees de Grothendieck (cribles, sites, topologies de Grothendieck, faisceaux).\n2. Localiser dans Mathlib les définitions de schema (`AlgebraicGeometry.Scheme`), de spectre (`Spec`), du site de Zariski et des propriétés locales de morphismes (etale, lisse, separe).\n3. Distinguer ce qui est **déjà la** (exploitable pedagogiquement), ce qui est **partiel** (utile avec precautions), et ce qui est **hors-scope Mathlib 4 actuel** (cohomologie etale ℓ-adique, motifs, six opérations, GRR).\n4. Lire les enonces des théorèmes grothendieckiens dans la syntaxe Lean 4 / Mathlib.\n\n### Prerequis\n\n- Familiarite avec Lean 4 et Mathlib (cf Lean-1 a Lean-6).\n- Notions de base de théorie des catégories (objet, morphisme, foncteur, transformation naturelle). Aucune connaissance prealable de geometrie algébrique n'est requise pour comprendre les enonces.\n- Sympathie pour le projet de **comprendre une chose en la plongeant dans le contexte le plus général qui la rend naturelle** (la phrase est de Grothendieck).\n\n### Duree estimée : 60 minutes\n\n**Note technique sur l'exécution**\n\nCe notebook utilise un kernel **Python 3**. Les sources Lean sont lues directement depuis le projet `grothendieck_lean/` qui accompagne ce notebook (même repertoire). Ce projet Lake contient des modules sous `Grothendieck/` formalisant des tours pedagogiques de Mathlib (catégories, cribles, schemas, Zariski, calibration, mais aussi faisceaux, faisceautisation, cohomologie par Ext, Mayer-Vietoris et Cech). Le build (`lake build Grothendieck`) est lance en WSL via subprocess, avec vérification de l'absence de sorry. Ce pattern est emprunte aux notebooks Lean-13/16 (Kochen-Specker/Conway).\n\nPour les exercices interactifs, `run_lean(snippet)` ecrit un snippet temporaire et l'exécute dans l'environnement Lake du projet, ce qui donne acces a tout Mathlib." ] }, { @@ -1397,19 +1372,7 @@ "tags": [] }, "source": [ - "### Interpretation : propriétés locales\n", - "\n", - "Les trois predicats Lean affichent une signature uniforme : `{X Y : Scheme} -> (X ⟶ Y) -> Prop`. C'est-a-dire : etant donné un morphisme `f : X ⟶ Y`, dire `Etale f`, `Smooth f`, `IsSeparated f` est une proposition.\n", - "\n", - "| Propriété | Intuition |\n", - "|-----------|-----------|\n", - "| `Etale` | morphisme \"plat + non ramifie\" : analogue d'un revetement de surface de Riemann |\n", - "| `Smooth` | morphisme \"plat + lisse au sens algébrique\" : analogue d'une submersion lisse en geometrie differentielle |\n", - "| `IsSeparated` | analogue de \"separe\" topologique : la diagonale est fermee |\n", - "\n", - "Mathlib regroupe ces propriétés sous le concept de **propriété locale** (locale sur la cible, sur la source, etc.) dans `Mathlib.AlgebraicGeometry.Morphisms.Basic`. C'est l'API qui sera utilisee pour construire le **site etale** -- la brique manquante pour parler de cohomologie etale (cf section suivante).\n", - "\n", - "**Note Mathlib actuelle** : les anciens noms `IsEtale`, `IsSmooth` ont ete renommes en `Etale`, `Smooth` (depreciations visibles dans les warnings)." + "### Interpretation : propriétés locales\n\nLes trois predicats Lean affichent une signature uniforme : `{X Y : Scheme} -> (X ⟶ Y) -> Prop`. C'est-a-dire : etant donne un morphisme `f : X ⟶ Y`, dire `Etale f`, `Smooth f`, `IsSeparated f` est une proposition.\n\n| Propriété | Intuition |\n|-----------|-----------|\n| `Etale` | morphisme \"plat + non ramifie\" : analogue d'un revetement de surface de Riemann |\n| `Smooth` | morphisme \"plat + lisse au sens algébrique\" : analogue d'une submersion lisse en geometrie differentielle |\n| `IsSeparated` | analogue de \"separe\" topologique : la diagonale est fermee |\n\nMathlib regroupe ces propriétés sous le concept de **propriété locale** (locale sur la cible, sur la source, etc.) dans `Mathlib.AlgebraicGeometry.Morphisms.Basic`. C'est l'API qui sera utilisee pour construire le **site etale** -- la brique manquante pour parler de cohomologie etale (cf section suivante).\n\n**Note Mathlib actuelle** : les anciens noms `IsEtale`, `IsSmooth` ont ete renommes en `Etale`, `Smooth` (depreciations visibles dans les warnings)." ] }, { @@ -1752,67 +1715,7 @@ "tags": [] }, "source": [ - "## 9. Pour aller plus loin\n", - "\n", - "### References historiques\n", - "\n", - "1. **A. Grothendieck**, *Éléments de geometrie algébrique* (avec J. Dieudonne), Publications mathematiques de l'IHES, 1960-1967 (EGA I-IV).\n", - "2. **A. Grothendieck et al.**, *Seminaire de geometrie algébrique du Bois-Marie*, plusieurs volumes, 1960-1969 (SGA 1-7).\n", - "3. **A. Grothendieck**, *Recoltes et Semailles*, manuscrit autobiographique, 1985-1986 (publie posthume, edition Gallimard 2022).\n", - "4. **A. Grothendieck**, *Tohoku paper* : \"Sur quelques points d'algebre homologique\", Tohoku Math. J. 9 (1957), 119-221.\n", - "5. **The Stacks Project**, https://stacks.math.columbia.edu/ : reference moderne, encyclopedique, mise a jour collaborative.\n", - "6. **R. Hartshorne**, *Algebraic Geometry*, Springer GTM 52, 1977.\n", - "7. **R. Vakil**, *The Rising Sea: Foundations of Algebraic Geometry*, draft en ligne, https://math.stanford.edu/~vakil/216blog/.\n", - "\n", - "### Travaux Lean recents\n", - "\n", - "- **Joel Riou** et al., travaux 2024-2025 sur les catégories dérivées, le foncteur dérive total, les localisations de catégories : cf `Mathlib.CategoryTheory.Localization.*` et `Mathlib.CategoryTheory.Triangulated.*`.\n", - "- **Kevin Buzzard**, **Adam Topaz**, **Patrick Massot** et la communaute Mathlib, ports continus d'EGA / Stacks Project.\n", - "- **Liquid Tensor Experiment** (Scholze + Commelin et al.) : exemple recent de formalisation lourde en geometrie algébrique formelle.\n", - "\n", - "### Liens vers d'autres notebooks de la serie\n", - "\n", - "- [Lean-6 Mathlib Essentials](Lean-6-Mathlib-Essentials.ipynb) : tour des principales structures Mathlib\n", - "- [Lean-10 LeanDojo](Lean-10-LeanDojo.ipynb) : agents de preuve sur Mathlib\n", - "- [Lean-12 Sensitivity](Lean-12-Sensitivity-Theorem.ipynb) : un théorème combinatoire avec preuve compacte Lean (Huang 2019)\n", - "- [Lean-16b Conway Tribute](Lean-16b-Conway-Game-of-Life-Lean.ipynb) : hommage Conway, Game of Life\n", - "- [Lean-13 Kochen-Specker](Lean-13-Kochen-Specker.ipynb) : théorème KS, même pattern (Python kernel + subprocess WSL Lean)\n", - "- [conway_lean/](conway_lean/) : modules Lean Conway (Doomsday, Life, Kochen-Specker)\n", - "- [grothendieck_lean/](grothendieck_lean/) : modules Lean accompagne ce notebook (Catégories, Sites, Schemes, Zariski, MathlibMap, Calibration + modules avances)\n", - "\n", - "**Note de scope (PR / Epic)**\n", - "\n", - "Le sous-projet `MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/` (workspace Lake avec `lakefile.lean`) accompagne cet hommage. Le projet a evolue depuis sa creation :\n", - "\n", - "- **Modules** sous `Grothendieck/` (catégories, cribles, schemas, Zariski, calibration, mais aussi treillis de cribles, générateurs de coverage, propriétés canoniques, topologie dense, faisceautisation, exactitude a gauche, sous-canonicite, points d'un site, hom-faisceaux, faisceau constant, familles conservatives, cohomologie des faisceaux par Ext, carrés de Mayer-Vietoris, suite exacte longue de Mayer-Vietoris, cohomologie de Cech ; + fondamentaux catégoriels : Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma).\n", - "- **Aucun sorry** comme terme de preuve.\n", - "- Les modules originaux couverts pedagogiquement dans ce notebook : `CategoryAndSites`, `SchemesTour`, `ZariskiSite`, `MathlibMap`, `Calibration`, `SieveLattice`. Les modules supplémentaires (SheafBasics, SieveOps, CoverageGen, CanonicalProps, SieveGenerate, DenseTopology, Sheafification, LeftExact, Subcanonical, SitePoints, SheafHom, ConstantSheaf, Conservative, SheafCohomology/Basic, MayerVietorisSquare, SheafCohomology/MayerVietoris, SheafCohomology/Cech + Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma) approfondissent la théorie des faisceaux, des sites et de la cohomologie, ainsi que les fondamentaux catégoriels.\n", - "\n", - "Lie a l'Epic #1646 (Grothendieck Lean side-track).\n", - "\n", - "### Le geste au-dela du langage\n", - "\n", - "Cet hommage montre qu'une partie du langage de Grothendieck vit déjà dans Mathlib : catégories, cribles, topologies, faisceaux, schemas, site de Zariski. Mais le langage n'est pas le seul heritage. Le geste qui porte ce langage -- *trouver la representation ou le problème cesse d'etre dur* -- traverse le depot tout entier, bien au-dela de Lean.\n", - "\n", - "Un même concept, dans CoursIA, se decline d'abord en **simulation** (calcul, experimentation, visualisation) puis, quand c'est possible, en **preuve formelle** (vérification mecanique, certification). Les mêmes théorèmes de choix social (Arrow, Sen) vivent en Python pedagogique *et* en Lean certifie. Le même Sudoku se resout par recherche, par contraintes, ou par SAT. Ce geste -- changer de representation jusqu'a ce que la difficulte se dissolve -- est précisément celui que Grothendieck decrit dans *Recoltes et Semailles* : non pas forcer la noix, mais laisser la mer monter.\n", - "\n", - "La cle de lecture [La mer qui monte](../../../docs/grothendieckian-lens.md) deploye ce fil conducteur a travers l'ensemble du depot, montrant que le geste grothendieckien n'est pas reserve aux mathematiques formelles. Il est la méthode même de l'IA digne de confiance : re-representer la sortie incertaine d'un modèle dans un cadre verifiable.\n", - "\n", - "Quant a la formalisation du *langage* de Grothendieck dans Mathlib -- les schemas, les faisceaux, le site etale -- elle poursuit sa route dans l'Epic [#1646](https://github.com/jsboige/CoursIA/issues/1646). Ce notebook est un hommage ; le travail continue.\n", - "\n", - "### Exercices supplémentaires (bonus)\n", - "\n", - "Pour aller plus loin que les 3 exercices de la section 8 :\n", - "\n", - "1. **`#check` exploratoire**. Trouver dans Mathlib les définitions de `CategoryTheory.Limits.HasLimits`, `CategoryTheory.Adjunction`, et lire leur signature. Indication : utiliser le pattern `run_lean` de ce notebook (`ALL_CHECKS` consolide pour gagner du temps).\n", - "2. **Cribles et raffinements**. Dans `Mathlib.CategoryTheory.Sites.Sieves`, identifier le lemme qui dit \"raffiner un crible par un crible donné un crible\" (composition de cribles).\n", - "3. **Yoneda explicite**. Lire `CategoryTheory.yonedaLemma` dans Mathlib (le lemme de Yoneda formel). Quelle est sa conclusion ?\n", - "4. **Faisceaux et recollement**. Dans `Mathlib.Topology.Sheaves.Sheaf`, identifier la condition de recollement qu'un `Presheaf` doit satisfaire pour etre un `Sheaf`. Que dit-elle intuitivement ?\n", - "5. **Pretopologie / topologie**. Dans `BigZariski.lean`, lire la preuve de `zariskiTopology_eq`. Combien de lignes ? Quelle tactique principale ?\n", - "\n", - "***\n", - "\n", - "**Navigation** : [<< Lean-14 Finiteness-Derivatives](Lean-14-Finiteness-Derivatives.ipynb) | [Lean-16b Conway Tribute >>](Lean-16b-Conway-Game-of-Life-Lean.ipynb) | [Index](README.md)" + "## 9. Pour aller plus loin\n\n### References historiques\n\n1. **A. Grothendieck**, *Éléments de geometrie algébrique* (avec J. Dieudonne), Publications mathematiques de l'IHES, 1960-1967 (EGA I-IV).\n2. **A. Grothendieck et al.**, *Seminaire de geometrie algébrique du Bois-Marie*, plusieurs volumes, 1960-1969 (SGA 1-7).\n3. **A. Grothendieck**, *Recoltes et Semailles*, manuscrit autobiographique, 1985-1986 (publie posthume, edition Gallimard 2022).\n4. **A. Grothendieck**, *Tohoku paper* : \"Sur quelques points d'algebre homologique\", Tohoku Math. J. 9 (1957), 119-221.\n5. **The Stacks Project**, https://stacks.math.columbia.edu/ : reference moderne, encyclopedique, mise a jour collaborative.\n6. **R. Hartshorne**, *Algebraic Geometry*, Springer GTM 52, 1977.\n7. **R. Vakil**, *The Rising Sea: Foundations of Algebraic Geometry*, draft en ligne, https://math.stanford.edu/~vakil/216blog/.\n\n### Travaux Lean recents\n\n- **Joel Riou** et al., travaux 2024-2025 sur les catégories dérivées, le foncteur dérive total, les localisations de catégories : cf `Mathlib.CategoryTheory.Localization.*` et `Mathlib.CategoryTheory.Triangulated.*`.\n- **Kevin Buzzard**, **Adam Topaz**, **Patrick Massot** et la communaute Mathlib, ports continus d'EGA / Stacks Project.\n- **Liquid Tensor Experiment** (Scholze + Commelin et al.) : exemple recent de formalisation lourde en geometrie algébrique formelle.\n\n### Liens vers d'autres notebooks de la serie\n\n- [Lean-6 Mathlib Essentials](Lean-6-Mathlib-Essentials.ipynb) : tour des principales structures Mathlib\n- [Lean-10 LeanDojo](Lean-10-LeanDojo.ipynb) : agents de preuve sur Mathlib\n- [Lean-12 Sensitivity](Lean-12-Sensitivity-Theorem.ipynb) : un théorème combinatoire avec preuve compacte Lean (Huang 2019)\n- [Lean-16b Conway Tribute](Lean-16b-Conway-Game-of-Life-Lean.ipynb) : hommage Conway, Game of Life\n- [Lean-13 Kochen-Specker](Lean-13-Kochen-Specker.ipynb) : théorème KS, même pattern (Python kernel + subprocess WSL Lean)\n- [conway_lean/](conway_lean/) : modules Lean Conway (Doomsday, Life, Kochen-Specker)\n- [grothendieck_lean/](grothendieck_lean/) : modules Lean accompagne ce notebook (Catégories, Sites, Schemes, Zariski, MathlibMap, Calibration + modules avances)\n\n**Note de scope (PR / Epic)**\n\nLe sous-projet `MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/` (workspace Lake avec `lakefile.lean`) accompagne cet hommage. Le projet a evolue depuis sa creation :\n\n- **Modules** sous `Grothendieck/` (catégories, cribles, schemas, Zariski, calibration, mais aussi treillis de cribles, générateurs de coverage, propriétés canoniques, topologie dense, faisceautisation, exactitude a gauche, sous-canonicite, points d'un site, hom-faisceaux, faisceau constant, familles conservatives, cohomologie des faisceaux par Ext, carrés de Mayer-Vietoris, suite exacte longue de Mayer-Vietoris, cohomologie de Cech ; + fondamentaux catégoriels : Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma).\n- **Aucun sorry** comme terme de preuve.\n- Les modules originaux couverts pedagogiquement dans ce notebook : `CategoryAndSites`, `SchemesTour`, `ZariskiSite`, `MathlibMap`, `Calibration`, `SieveLattice`. Les modules supplémentaires (SheafBasics, SieveOps, CoverageGen, CanonicalProps, SieveGenerate, DenseTopology, Sheafification, LeftExact, Subcanonical, SitePoints, SheafHom, ConstantSheaf, Conservative, SheafCohomology/Basic, MayerVietorisSquare, SheafCohomology/MayerVietoris, SheafCohomology/Cech + Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma) approfondissent la théorie des faisceaux, des sites et de la cohomologie, ainsi que les fondamentaux catégoriels.\n\nLie a l'Epic #1646 (Grothendieck Lean side-track).\n\n### Le geste au-dela du langage\n\nCet hommage montre qu'une partie du langage de Grothendieck vit déjà dans Mathlib : catégories, cribles, topologies, faisceaux, schemas, site de Zariski. Mais le langage n'est pas le seul heritage. Le geste qui porte ce langage -- *trouver la representation ou le problème cesse d'etre dur* -- traverse le depot tout entier, bien au-dela de Lean.\n\nUn même concept, dans CoursIA, se decline d'abord en **simulation** (calcul, experimentation, visualisation) puis, quand c'est possible, en **preuve formelle** (vérification mecanique, certification). Les mêmes théorèmes de choix social (Arrow, Sen) vivent en Python pedagogique *et* en Lean certifie. Le même Sudoku se resout par recherche, par contraintes, ou par SAT. Ce geste -- changer de representation jusqu'a ce que la difficulte se dissolve -- est précisément celui que Grothendieck decrit dans *Recoltes et Semailles* : non pas forcer la noix, mais laisser la mer monter.\n\nLa cle de lecture [La mer qui monte](../../../docs/grothendieckian-lens.md) deploye ce fil conducteur a travers l'ensemble du depot, montrant que le geste grothendieckien n'est pas reserve aux mathematiques formelles. Il est la méthode même de l'IA digne de confiance : re-representer la sortie incertaine d'un modèle dans un cadre verifiable.\n\nQuant a la formalisation du *langage* de Grothendieck dans Mathlib -- les schemas, les faisceaux, le site etale -- elle poursuit sa route dans l'Epic [#1646](https://github.com/jsboige/CoursIA/issues/1646). Ce notebook est un hommage ; le travail continue.\n\n### Exercices supplémentaires (bonus)\n\nPour aller plus loin que les 3 exercices de la section 8 :\n\n1. **`#check` exploratoire**. Trouver dans Mathlib les définitions de `CategoryTheory.Limits.HasLimits`, `CategoryTheory.Adjunction`, et lire leur signature. Indication : utiliser le pattern `run_lean` de ce notebook (`ALL_CHECKS` consolide pour gagner du temps).\n2. **Cribles et raffinements**. Dans `Mathlib.CategoryTheory.Sites.Sieves`, identifier le lemme qui dit \"raffiner un crible par un crible donne un crible\" (composition de cribles).\n3. **Yoneda explicite**. Lire `CategoryTheory.yonedaLemma` dans Mathlib (le lemme de Yoneda formel). Quelle est sa conclusion ?\n4. **Faisceaux et recollement**. Dans `Mathlib.Topology.Sheaves.Sheaf`, identifier la condition de recollement qu'un `Presheaf` doit satisfaire pour etre un `Sheaf`. Que dit-elle intuitivement ?\n5. **Pretopologie / topologie**. Dans `BigZariski.lean`, lire la preuve de `zariskiTopology_eq`. Combien de lignes ? Quelle tactique principale ?\n\n***\n\n**Navigation** : [<< Lean-14 Finiteness-Derivatives](Lean-14-Finiteness-Derivatives.ipynb) | [Lean-16b Conway Tribute >>](Lean-16b-Conway-Game-of-Life-Lean.ipynb) | [Index](README.md)" ] } ],