Enrich(notebook,#17978): Lean-15d references Serre100, Langlands, Geo-02 + Sheydvasser

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15d-Lean-Grothendieck-Visuel-Python.ipynb

@@ -20,15 +20,20 @@
     "\n",
     "**Une visite guidee visuelle des abstractions grothendieckiennes.**\n",
     "\n",
-    "Le depot porte deja trois carnets sur ce corpus :\n",
+    "Le depot porte deja six carnets sur ce corpus, plus une greffe croisee :\n",
     "\n",
     "| Carnet | Ce qu'il fait |\n",
     "|---|---|\n",
     "| `Lean-15-Grothendieck-Tribute` | le catalogue : les modules du lake, affiches par extraits |\n",
     "| `Lean-15b-Lean-Grothendieck` | l'atelier : exercices sur cribles, topologies, faisceaux |\n",
     "| `Lean-15c-Lean-Grothendieck-Companion` | le companion formel natif (kernel `lean4-wsl`) |\n",
+    "| `Serre100/01..15` | la descente arithmetique : corps finis, fonctions L, cohomologie, table de caracteres, reciprocite quadratique (15 carnets, lake `serre100_lean`) |\n",
+    "| `Langlands/01..02` | l'horizon : formes modulaires `SL(2,Z)/Hecke`, moonshine monstrueuse et invariant `j` (2 carnets) |\n",
+    "| `Geometry/02-From-Equation-To-Proof` | la greffe de la preuve : sur deux cellules-pivots, les encadres *Pour aller plus loin -- Surviving proofs* commentent l'echec et le contre-exemple a la lumiere de Sheydvasser (PR #17912) |\n",
     "\n",
-    "Aucun des trois ne **montre** ce dont il parle. Le premier affiche du code Lean, le deuxieme pose des questions, le troisieme compile des enonces. Or les objets de Grothendieck -- cribles, sites, faisceaux -- sont des objets **geometriques**, et l'intuition qui les rend maniables se transmet mal par une liste de theoremes.\n",
+    "Aucun des six ne **montre** ce dont il parle au sens ou ce carnet l'entend. Les trois premiers affichent du code Lean, posent des questions ou compilent des enonces. Les carnets Serre100 partent de l'arithmetique des corps finis pour remonter aux memes structures. Les carnets Langlands prennent la thematique de plus loin encore : la correspondance elle-meme. Geo-02 deplace l'intuition sur deux cellules d'un carnet de geometrie. Or les objets de Grothendieck -- cribles, sites, faisceaux -- sont des objets **geometriques**, et l'intuition qui les rend maniables se transmet mal par une liste de theoremes.\n",
+    "\n",
+    "Les figures qui suivent s'inspirent directement de ces cinq sources : la **condition de recollement** (section 4) prend son exemple arithmetique dans `Serre100/03-cohomologie-cech-espaces-finis` ; le **lemme de Yoneda** (section 5) admet un equivalent sur les **categories finies** dans `Serre100/04-lemme-yoneda-categories-finies` ; la **methode de l'echec et du contre-exemple** qui sous-tend les sections 1 a 6 est documentee in situ dans `Geometry-02` par les articles 1 et 2 de *Surviving proofs* (Sheydvasser, 05 et 12 septembre 2026), greffes Art 1 et Art 2 deposees par #17912.\n",
     "\n",
     "Ce carnet prend le probleme par l'autre bout : **une figure par abstraction**, dessinee en Python, sans dependance au lake ni a un kernel Lean. Il ne remplace pas les trois autres, il les rend lisibles.\n",
     "\n",
@@ -799,7 +804,9 @@
     "\n",
     "**Le point a retenir.** La condition de faisceau n'est pas une commodite technique : c'est ce qui distingue un simple prefaisceau (une donnee locale quelconque) d'un faisceau (une donnee locale qui merite d'etre appelee globale). Un prefaisceau peut porter des sections incompatibles ; un faisceau, non.\n",
     "\n",
-    "C'est aussi la raison pour laquelle `Sheaf.lean` de Mathlib definit un faisceau comme un prefaisceau muni d'une **preuve** de cette condition, et non comme un objet supplementaire."
+    "C'est aussi la raison pour laquelle `Sheaf.lean` de Mathlib definit un faisceau comme un prefaisceau muni d'une **preuve** de cette condition, et non comme un objet supplementaire.\n",
+    "\n",
+    "**Pour aller plus loin -- Serre100.** La meme condition de recollement, portee sur des **espaces finis** plutot que sur des ouverts topologiques, prend une forme explicite ou les intersections $U_i \\cap U_j$ sont des produits cartesiens. C'est le sujet de `Serre100/03-cohomologie-cech-espaces-finis` : on y voit la condition de cocycle (compatibilite sur les intersections doubles) commander l'integrale du produit cup, et la nullite de la cohomologie $\\check{H}^1$ etre exactement la condition de recollement de la figure 4. La figure Python que l'on dessine ici, c'est, informellement, le cas continu de ce que le Cech discrete code en algebre."
    ]
   },
   {
@@ -977,7 +984,9 @@
     "\n",
     "**Le point qui bloque souvent a la premiere lecture** : $\\alpha_A(\\mathrm{id}_A)$ reside dans $F(A)$, donc au-dessus de l'objet de depart $A$ lui-meme, pas au-dessus d'un objet quelconque. L'element identite de $\\operatorname{Hom}(A, A)$ est le seul qui existe sans hypothese ; c'est ce qui en fait la source canonique de la correspondance.\n",
     "\n",
-    "**Yoneda en une phrase.** Un objet $A$ n'est pas connu par une description interne, mais par l'ensemble de ses relations avec tous les autres. Le lemme rend cette phrase exacte : le foncteur $\\operatorname{Hom}(A, -)$ contient toute l'information sur $A$. C'est ce principe que la theorie des topos exploite -- dont le site de la section suivante fournit le premier exemple."
+    "**Yoneda en une phrase.** Un objet $A$ n'est pas connu par une description interne, mais par l'ensemble de ses relations avec tous les autres. Le lemme rend cette phrase exacte : le foncteur $\\operatorname{Hom}(A, -)$ contient toute l'information sur $A$. C'est ce principe que la theorie des topos exploite -- dont le site de la section suivante fournit le premier exemple.\n",
+    "\n",
+    "**Pour aller plus loin -- Serre100.** Le lemme de Yoneda admet un cas particulier **sur les categories finies** qui se laisse enumerer a la main : si $\\mathcal{C}$ est une categorie finie et $F$ un foncteur, les transformations naturelles $\\operatorname{Hom}(A,-) \\Rightarrow F$ sont determinees par la seule evaluation en $A$, et leur nombre est exactement $|F(A)|$. C'est le contenu de `Serre100/04-lemme-yoneda-categories-finies` : une preuve constructive qui donne, en passant, un algorithme pour enumerer ces transformations. Le dessin de la figure 5 capture la meme idee -- la bijection entre une famille indexee par $\\operatorname{Ob}(\\mathcal{C})$ et un element de $F(A)$ -- mais sans la discretude qui rend l'enumeration faisable a la main."
    ]
   },
   {