restore(lean,#17066): lean15b — restauration « Lecture des 18 vérifications » (mot pour mot, +13/-0)

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15b-Lean-Grothendieck.ipynb

@@ -2429,6 +2429,19 @@
     "    print(f'  {i:>2d}. {name}')"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "c34d70af",
+   "metadata": {
+    "papermill": {},
+    "tags": []
+   },
+   "source": [
+    "### Lecture des 18 vérifications : l'index est vivant, pas déclaré\n",
+    "\n",
+    "La sortie énumère les `#check` que `MathlibMap.lean` fait passer au noyau — les noms effectivement présents dans le Mathlib vendu au moment du build. Lisez la structure de la liste : les premières entrées (`yoneda`, `coyoneda`) attestent le socle de théorie des catégories ; viennent ensuite la hiérarchie cribles puis topologies de Grothendieck (`trivial`, `discrete`, `dense` — les trois topologies extrémales du cours) ; puis les faisceaux (`IsSheaf`, `IsSeparated`, `TopCat.Sheaf`) ; enfin le monde des schémas (`Scheme`, `Spec`, `Γ` le foncteur des sections globales, et les deux foncteurs d'oubli vers `TopCat` et `LocallyRingedSpace`). Ce qui fait la valeur de cet index : chaque entrée a été **vérifiée par compilation**, pas copiée d'une documentation — si une future version de Mathlib renomme `Scheme.Γ`, le `#check` correspondant passera au rouge et signalera la divergence immédiatement. Les absents (ce que Mathlib n'a pas encore) restent documentés dans le module lui-même, section « ce que Mathlib a et n'a pas encore »."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "lean13b-section8-exercises",