Hommage à Grothendieck — Visite de Mathlib

Alexandre Grothendieck (1928-2014).

Grothendieck a déplacé l’objet d’étude : plutôt que disséquer chaque structure isolément, il a construit les catégories, les sites et les faisceaux qui les portent — et laissé les théorèmes tomber comme des corollaires. Ce workspace montre que ce langage vit déjà dans Mathlib 4 : c’est une visite guidée du paysage grothendieckien telle que la bibliothèque la formalise aujourd’hui.

L’esprit de la visite

Ce workspace est un hommage pédagogique — délibérément pas une tentative de formaliser EGA/SGA. Le but est d’offrir aux apprenants un point d’entrée curaté vers :

  • Catégories, cribles (sieves) et topologies de Grothendieck
  • Faisceaux (sheaves), prefaisceaux séparés, topologies sous-canoniques
  • Génération de recouvrements (coverage) et caractérisation des faisceaux
  • La topologie canonique et les sites sous-canoniques
  • Schémas (espaces annelés en anneaux locaux localement Spec R) et site de Zariski
  • Ce que Mathlib possède et ce qu’il n’a pas (encore)

Comment lire ce workspace

Trois parcours sont proposés selon ton but :

  1. Lecteur découvrant Grothendieck pour la première fois. Suis l’arc « poser le site → construire le faisceau → faire parler les points ». Les Parties 1 (catégories et sites), 6 (cribles), 8 (ordre sur les topologies) jettent les fondations ; 13 (faisceautisation) et 14 (exactitude à gauche) donnent le théorème clé ; 15 (points d’un site) et 19 (familles conservatrices) relient la théorie à ses modèles ; 20-23 (cohomologie) mesurent l’obstruction. Le tableau des Parties (ci-dessous) donne le contenu de chaque module en une ligne.

  2. Lecteur intéressé par les six opérations (image directe / réciproque / exceptionnelle). Le fil va de la Partie 33 (DirectImage, f^* ⊣ f_*) à la Partie 34 (ExceptionalDirect, f_! ⊣ f^*) puis la Partie 68 (ExceptionalTriple, f_! ⊣ f^* ⊣ f_* au complet). Trois adjonctions, ordonnées de la mieux connue à la moins connue.

  3. Lecteur intéressé par le pont Lawvere–Tierney ↔︎ Grothendieck. Parties 58 (classifieur Ω), 59 (opérateur de clôture j sur Ω), 60 (le dictionnaire : topologies de Grothendieck = topologies de Lawvere–Tierney, les deux notions se confondent). C’est le pont où la logique catégorique rejoint la géométrie relative.

Conventions de navigation. Les modules sont regroupés en dossiers Grothendieck/ et SheafCohomology/ ; chaque module Foo.lean a un sibling Foo_en.lean pour la version anglaise (convention i18n EPIC #4980). L’umbrella Grothendieck.lean est un index de lecture FR-only : il importe chaque module FR et jamais un _en — les siblings anglais restent construits par les globs du lakefile (#16154, invariant tenu par scripts/lean/tests/test_grothendieck_umbrella.py). Le tableau ci-dessous donne, pour chaque Partie, le module FR + le module _en + une ligne de contenu.

La trajectoire

Les modules leaf (0 sorry, 0 axiome ajouté) tracent un chemin cohérent, du site brut jusqu’à la cohomologie :

flowchart LR
    T1["<b>Sites & cribles</b><br/><i>Parties 1·6·8·11·12·16</i><br/>topologies de Grothendieck<br/>pullback_id · pullback_monotone"]
    T2["<b>Faisceaux & séparation</b><br/><i>7·9·10·17</i><br/>préfaisceau séparé<br/>transfert le long de J₁ ≤ J₂"]
    T3["<b>Faisceautisation</b><br/><i>13·14</i><br/>foncteur faisceau associé<br/>exactitude à gauche (LeftExact)"]
    T4["<b>Points & conservateurs</b><br/><i>15·19</i><br/>foncteurs fibres<br/>familles conservatrices"]
    T5["<b>Cohomologie</b><br/><i>20·21·22·23</i><br/>Ext · Mayer-Vietoris · Čech"]
    T1 --> T2 --> T3 --> T4 --> T5
    S["<b>Schémas & site de Zariski</b><br/><i>Parties 2·3</i><br/>foncteur Spec<br/>zariski_topology_eq"] -.->|"ancre géométrique"| T1
    MM["<b>Carte Mathlib</b><br/><i>Partie 4</i><br/>index #check"] -.->|"ancre bibliothèque"| T3

Poser le site (Parties 1, 6, 8, 11, 12, 16). Tout part de la donnée d’une catégorie munie d’une topologie de Grothendieck — triviale, discrète, dense, canonique. Les cribles y forment un treillis que le pullback parcourt (pullback_id, pullback_pullback, pullback_monotone…), et chaque topologie se compare, se génère et se ferre par clôture de recouvrement.

Construire le faisceau (Parties 7, 9, 10, 13, 14, 17, 18). Au-dessus du site vivent les préfaisceaux ; la condition de recollement — unicité puis existence — définit la séparation puis le faisceau, transférable le long de J₁ ≤ J₂. La faisceautisation (foncteur faisceau associé, exact à gauche) convertit tout préfaisceau en faisceau :

flowchart TD
    SITE["<b>Site</b><br/><i>catégorie + topologie de Grothendieck</i><br/>(Partie 1)"]
    PSH["<b>Préfaisceau</b><br/><i>objets Cᵒᵖ → Type*</i>"]
    SEP["<b>Préfaisceau séparé</b><br/>unicité du recollement"]
    SH["<b>Faisceau</b><br/>existence + unicité du recollement"]
    SHIF["<b>Faisceautisation</b><br/><i>foncteur faisceau associé</i><br/>Partie 13 — exactitude à gauche (Partie 14)"]
    COH["<b>Cohomologie des faisceaux</b><br/>Parties 20-23<br/>Ext · Mayer-Vietoris · Čech"]
    SITE --> PSH --> SEP --> SH
    SHIF -.->|"produit un faisceau<br/>depuis un préfaisceau"| SH
    SH --> COH
    TR["<b>Transfert de faisceau</b><br/>le long de J₁ ≤ J₂<br/>(Partie 7)"] -.-> SH

Faire parler les points, mesurer la cohomologie (Parties 15, 19, 20-23). Les points d’un site (foncteurs fibres) et leurs familles conservatrices relient la théorie à ses modèles ; la cohomologie des faisceaux — via Ext, Mayer-Vietoris et Čech — en est l’instrument de mesure.

Les ancrages. Côté géométrie, les schémas et le site de Zariski (Parties 2, 3) relient la visite à la géométrie algébrique d’origine, avec le théorème-pont zariski_topology_eq. Côté bibliothèque, la carte Mathlib (Partie 4, index #check) dit honnêtement ce qui existe et ce qui manque, et Calibration.lean (Partie 5) reprend la taxonomie d’étalonnage du harnais prouveur (Epic #1453, P1-P4) sans être consommée par lui : les cibles effectives du harnais vivent dans calibration_lean/ (classe HARNESS, frontière arbitrée #13212).

Les fondations catégorielles (Parties 24-32). Yoneda, adjonctions, monades, catégories comma, (co)limites, équivalences, extensions de Kan, catégories monoïdales : le socle sur lequel tout ce qui précède s’écrit.

Les deux veines récentes (Parties 33-44). Le fil des six opérations s’ouvre avec DirectImage.lean (Partie 33, index de l’adjonction f^* ⊣ f_*) puis ExceptionalDirect.lean (Partie 34, #10357) qui formalise f_! ⊣ f^* au niveau préfaisceau — l’image directe à support propre comme extension de Kan à gauche, chaînon manquant entre f^* et f_*. En parallèle, le programme couverture (Phase 5 de l’Epic #2159, vagues 2026-08-14..16 : #10879 → #11244) systématise la forme flèche et la forme bundlée de la couverture — de covers_comp_iff jusqu’à la forme flèche de la topologie dense (Partie 44), en passant par les lois du pseudofoncteur pullback et le treillis des topologies. Une troisième veine s’ouvre avec Classifier.lean (Partie 58, #2159) : le classifieur de sous-objets Ω — littéralement le préfaisceau des cribles de la Partie 6 — qui fait des préfaisceaux et des faisceaux d’ensembles sur un site essentiellement petit des topos élémentaires (Lawvere–Tierney). Elle se referme en deux temps : LawvereTierney.lean (Partie 59) pose l’opérateur de clôture j sur Ω (trois lois + naturalité), puis TopologyDictionary.lean (Partie 60) démontre le dictionnaire — topologies de Grothendieck et topologies de Lawvere–Tierney sont la même donnée, les deux transports étant inverses l’un de l’autre.

Structure du code

La formalisation couvre l’ensemble des modules leaf + 1 umbrella Grothendieck.lean (imports-only, index de lecture FR-only — #16154). Les trois sous-modules de SheafCohomology/ sont les Parties 20, 22 et 23 du tableau.

Partie Fichier _en Contenu Lignes
racine Grothendieck.lean (aucun — FR-only) Racine umbrella (imports-only + commentaire d’invariant FR-only) ; importe chaque leaf FR et jamais un sibling _en (invariant #16154 ; les siblings _en restent compilés par les globs du lakefile) ; ExceptionalDirect importé c.2026-08-15, fermeture #11286 291
1 Grothendieck/CategoryAndSites.lean CategoryAndSites_en.lean Cribles, topologies de Grothendieck (triviale/discrète/dense), trois axiomes 243
2 Grothendieck/SchemesTour.lean SchemesTour_en.lean Type des schémas, foncteur Spec, Γ, homeoOfIso, pleinement fidèle 196
3 Grothendieck/ZariskiSite.lean ZariskiSite_en.lean Prétopologie de Zariski, théorème-pont zariskiTopology_eq, sous-canonique 139
4 Grothendieck/MathlibMap.lean MathlibMap_en.lean Index #check des définitions Mathlib liées à Grothendieck 124
5 Grothendieck/Calibration.lean Calibration_en.lean 4 cibles de micro-preuve dans l’esprit du harnais prouveur (Epic #1453, non consommées par lui — cf calibration_lean/, frontière #13212) 95
6 Grothendieck/SieveLattice.lean SieveLattice_en.lean Identités de pullback de cribles (7) : pullback_id, pullback_pullback, pullback_bot, pullback_monotone, pullback_union (#7895), pullback_ofObjects, mem_iff_pullback_eq_top 253
7 Grothendieck/SheafBasics.lean SheafBasics_en.lean Bases faisceau/préfaisceau séparé, transfert de faisceau le long de J₁ ≤ J₂ 231
8 Grothendieck/SieveOps.lean SieveOps_en.lean Ordre sur les topologies, clôture de recouvrement, composition de cribles 208
9 Grothendieck/CoverageGen.lean CoverageGen_en.lean Coverage-vers-topologie, caractérisation des faisceaux, sup de coverages 233
10 Grothendieck/CanonicalProps.lean CanonicalProps_en.lean Topologie canonique, sous-canoïcité, faisceaux représentables 155
11 Grothendieck/SieveGenerate.lean SieveGenerate_en.lean Identités de génération de cribles 243
12 Grothendieck/DenseTopology.lean DenseTopology_en.lean La topologie dense 218
13 Grothendieck/Sheafification.lean Sheafification_en.lean Faisceautisation (le foncteur faisceau associé) 259
14 Grothendieck/LeftExact.lean LeftExact_en.lean Exactitude à gauche de la faisceautisation 219
15 Grothendieck/SitePoints.lean SitePoints_en.lean Points d’un site (foncteurs fibres) 411
16 Grothendieck/Subcanonical.lean Subcanonical_en.lean Topologies de Grothendieck sous-canoniques 232
17 Grothendieck/SheafHom.lean SheafHom_en.lean Hom interne des faisceaux 273
18 Grothendieck/ConstantSheaf.lean ConstantSheaf_en.lean Le foncteur faisceau constant (ponte vers CategoryTheory.Sites.ConstantSheaf de Mathlib) 252
19 Grothendieck/Conservative.lean Conservative_en.lean Familles conservatrices de points 501
20 Grothendieck/SheafCohomology/Basic.lean SheafCohomology/Basic_en.lean Cohomologie des faisceaux (basée sur Ext) 336
21 Grothendieck/MayerVietorisSquare.lean MayerVietorisSquare_en.lean Carrés de Mayer-Vietoris 338
22 Grothendieck/SheafCohomology/MayerVietoris.lean SheafCohomology/MayerVietoris_en.lean Suite exacte longue de Mayer-Vietoris 235
23 Grothendieck/SheafCohomology/Cech.lean SheafCohomology/Cech_en.lean Cohomologie de Čech 203
24 Grothendieck/YonedaLemma.lean YonedaLemma_en.lean Le lemme de Yoneda (plongement, équivalence, naturalité, pleinement fidèle, coyoneda) 286
25 Grothendieck/Adjunction.lean Adjunction_en.lean Adjonction de foncteurs, unité/co-unité, lemme de la tortue (turtle), adjoints à droite/gauche 335
26 Grothendieck/Monads.lean Monads_en.lean Monades en théorie des catégories, unité, multiplication, loi d’association 253
27 Grothendieck/Comma.lean Comma_en.lean Catégorie comma, projections, fonctorialité 239
28 Grothendieck/Limits.lean Limits_en.lean Limites et colimites 421
29 Grothendieck/Equivalences.lean Equivalences_en.lean Équivalences de catégories, foncteurs pleinement fidèles, essentiellement surjectifs 338
30 Grothendieck/Construction.lean Construction_en.lean Constructions catégorielles de base 256
31 Grothendieck/KanExtensions.lean KanExtensions_en.lean Extensions de Kan (limites/colimites généralisées) 481
32 Grothendieck/MonoidalCategories.lean MonoidalCategories_en.lean Catégories monoïdales, tenseur, unité, associateur 397
33 Grothendieck/DirectImage.lean DirectImage_en.lean Index #check (8) de l’adjonction f^* ⊣ f_* — image directe / réciproque des faisceaux de modules (#8882) 325
34 Grothendieck/ExceptionalDirect.lean ExceptionalDirect_en.lean Image directe exceptionnelle f_! au niveau préfaisceau et son adjonction f_! ⊣ f^* — extension de Kan à gauche de f^* le long de f (#10357, Phase 2 de #2159) 202
35 Grothendieck/CoversArrow.lean CoversArrow_en.lean Forme flèche de la couverture : covers_monotone, covers_union, covers_inf, équivalence covers_comp_iff (#10879, Phase 5 de #2159) 199
36 Grothendieck/Cover.lean Cover_en.lean Couverture bundlée J.Cover X : coe-injective, lois pullback/top/inf, bind_mem_iff, condition de base (#10912, Phase 5 de #2159) 284
37 Grothendieck/PullbackFunctor.lean PullbackFunctor_en.lean Lois de cohérence du pseudofoncteur pullback sur J.Cover : pullback_triple, pullbackComp_assoc, unités gauche/droite (#11023, Phase 5 de #2159) 149
38 Grothendieck/PullbackFunctorLaws.lean PullbackFunctorLaws_en.lean Lois de foncteur du pullback : pullback_functor_id, pullback_functor_comp(_assoc), covers_pullback_comp (#11035, Phase 5 de #2159) 141
39 Grothendieck/TopologyLattice.lean TopologyLattice_en.lean Lois de treillis des topologies de Grothendieck : inf/sup_covering, sSup_covering, le_covers (#11038, Phase 5 de #2159) 211
40 Grothendieck/CoversPullback.lean CoversPullback_en.lean Lois de la forme flèche sous pullback : covers_pullback_comp, covers_bind, covers_iso_covering/cancel, covers_mono (#11057, Phase 5 de #2159) 202
41 Grothendieck/CoversOrder.lean CoversOrder_en.lean Lois d’ordre de la forme flèche J.Covers : covers_top/bot_iff, covers_inter_iff, covers_of_covering, covers_generate_sieve (#11068, Phase 5 de #2159) 164
42 Grothendieck/PullbackCoversLaws.lean PullbackCoversLaws_en.lean Lois de la forme flèche sous pullback itéré : covers_pullback_assoc, covers_pullback_id, covers_pullback_generate (#11217, Phase 5 de #2159) 160
43 Grothendieck/CoversLattice.lean CoversLattice_en.lean Lois de treillis indexées de la forme flèche : sInf/sSup_covering, sInf/sSup_covers (#11231, Phase 5 de #2159) 106
44 Grothendieck/CoversTopologies.lean CoversTopologies_en.lean Forme flèche de la topologie dense : dense_covers_iff, dense_covers_precomp (stabilité par précomposition), dense_covers_id (#11244, Phase 5 de #2159) 115
45 Grothendieck/CoversPushforward.lean CoversPushforward_en.lean Image directe de la forme flèche le long d’un foncteur : covers_pushforward, covers_pushforward_comp, covers_pushforward_iso, covers_pushforward_of_covering (PR #11262 MERGED 2026-08-16 par po-2025, Partie 45 de #2159) 152
46 Grothendieck/CoversBind.lean CoversBind_en.lean Composition séquentielle de la forme flèche J.Covers : covers_bind, covers_bind_assoc, covers_bind_id_left/right, covers_bind_of_covering (PR #11285 MERGED 2026-08-16 par po-2025, Partie 46 de #2159) 138
52 Grothendieck/CoversCoverageArrow.lean CoversCoverageArrow_en.lean Forme flèche de la topologie engendrée par une couverture au sens Coverage (#11396, Phase 5 de #2159) 174
53 Grothendieck/CoversPrecoverageArrow.lean CoversPrecoverageArrow_en.lean Forme flèche de la topologie engendrée par une pré-couverture Precoverage.toGrothendieck : pont covers_iff_toGrothendieck avec l’extension inductive Saturate (#11402, Phase 5 de #2159) 187
54 Grothendieck/CoversPretopologyArrow.lean CoversPretopologyArrow_en.lean Forme flèche de la topologie engendrée par une prétopologie (Pretopology.toGrothendieck) : pont central covers_iff_toGrothendieck, covers_of_mem_toGrothendieck, covers_iff_pullback_toGrothendieck (Phase 5 de #2159) 189
55a Grothendieck/CoversCoherentArrow.lean CoversCoherentArrow_en.lean Forme flèche de la topologie cohérente (coherentTopology) : instantiation du patron covers_iff_toGrothendieck / stabilité pullback (Phase 5 de #2159) 183
55b Grothendieck/CoversRegularArrow.lean CoversRegularArrow_en.lean Forme flèche de la topologie régulière (regularTopology, catégorie Preregular) : même patron de ponts (Phase 5 de #2159) 175
55c Grothendieck/CoversExtensiveArrow.lean CoversExtensiveArrow_en.lean Forme flèche de la topologie extensive (extensiveTopology, catégorie FinitaryPreExtensive) : même patron de ponts (Phase 5 de #2159) 181
56 Grothendieck/CoversZariskiArrow.lean CoversZariskiArrow_en.lean Forme flèche de la topologie de Zariski (première topologie nommée concrète de la série) : covers_iff_zariski + caractérisation géométrique par recouvrements ouverts covers_iff_exists_cover (Phase 5 de #2159, autonome sur main) 233
57 Grothendieck/CoversAtomicArrow.lean CoversAtomicArrow_en.lean Forme flèche de la topologie atomique (GrothendieckTopology.atomic, condition d’Ore à droite) : pont ponctuel atomic_covering (analogue manquant de dense_covering), covers_iff_atomic (central), covers_atomic_of_mem, stabilité covers_atomic_precomp, retombées covers_atomic_id/covers_atomic_top (Phase 5 de #2159) 159
58 Grothendieck/Classifier.lean Classifier_en.lean Le classifieur de sous-objets : Ω = le préfaisceau des cribles (Functor.sieves), truth/χ, Presheaf.classifier, cribles J-clos (Sheaf.Ω), instances HasSubobjectClassifier préfaisceaux + faisceaux ; 4 théorèmes propres (truth_picks_top, chi_app_mem_iff, chi_app_downward_closed, chi_app_eq_top_of_app) (Partie 58 de #2159) 202
59 Grothendieck/LawvereTierney.lean LawvereTierney_en.lean La topologie de Lawvere–Tierney : l’opérateur de clôture sur Ω (LawvereTierney), 3 lois (extensivité, idempotence, préservation des meets) + naturalité au pullback ; topologies discrète (j S = S) et indiscrete (j S = ⊤), j_top/j_monotone/closure_isClosed, cribles clos de l’indiscrete (Partie 59 de #2159) 241
60 Grothendieck/TopologyDictionary.lean TopologyDictionary_en.lean Le dictionnaire Grothendieck ↔︎ Lawvere–Tierney : la clôture jClosure J S = {f \| S.pullback f ∈ J} (sens J → j, grothendieckToLawvereTierney), les cribles denses j S = ⊤ (sens j → J, lawvereTierneyToGrothendieck), pont central covering_iff_jClosure, et les deux round-trips inverses — la frontière déclarée ouverte par la Partie 59 (« exige un opérateur absent de Mathlib v4.32.1 ») est fermée en le construisant depuis les axiomes bruts (Partie 60 de #2159) 330
61 Grothendieck/SitesComparison.lean SitesComparison_en.lean Foncteurs continus et lemme de comparaison : le pont préfaisceau→faisceau (sheafPushforwardContinuous), fonctorialité (identité, composition — miroir faisceau de pullback_pullback), et l’adjonction induite sur les catégories de faisceaux adjunction_sheafPushforwardContinuous (SGA 4 III.1.6) — les adjonctions descendent aux faisceaux sans sheafification explicite (Partie 61 de #2159) 158
62 Grothendieck/PlusConstruction.lean PlusConstruction_en.lean La construction Plus : l’ingrédient constructif de la sheafification en deux passes (SGA 4 II.3) — fonctorialité (plusFunctor), flèche canonique toPlus (naturalité), identité clé (P ⟶ P⁺)⁺ = P⁺ ⟶ P⁺⁺, point fixe des faisceaux (isoToPlus), propriété universelle du relevé (plusLift/plusLift_unique/plus_hom_ext) (Partie 62 de #2159) 196
63 Grothendieck/SheafCondition.lean SheafCondition_en.lean La condition de faisceau produit-égaliseur : reformulation de Presheaf.IsSheaf J P comme diagramme égaliseur P(X) → ∏ᵢ P(U_i) ⇉ ∏ᵢⱼ P(U_i ×_X U_j) — forme cribles (sheaf_iff_equalizer_sieve), forme familles d’arrows sous HasPullbacks C (sheaf_iff_equalizer_arrows, Stacks 00VM), pont prétopologie (sheaf_pretopology_iff, Stacks 00VL, SGA 4 II.1) (Partie 63 de #2159) 129
64 Grothendieck/SheafConditionInvariance.lean SheafConditionInvariance_en.lean Invariance de la condition de faisceau : stabilité de Presheaf.IsSheaf sous changement de site équivalent (morphismes couverts, équivalence de catégories, refinements) — pont avec Partie 61 —
65 Grothendieck/SheafConditionCharacterization.lean SheafConditionCharacterization_en.lean Caractérisations de la condition de faisceau : reformulations équivalentes de Presheaf.IsSheaf sous des hypothèses structurelles (présence de produits fibrés, finitude) — pont direct avec Partie 63 —
66 Grothendieck/SheafTopologySpectrum.lean SheafTopologySpectrum_en.lean Spectre de topologies de Grothendieck : lattice des topologies sur un site fixé, comparaisons canoniques (discrète, triviale, canonique, sous-canonique, dense) —
67 Grothendieck/LocalSurjectivitySpectrum.lean LocalSurjectivitySpectrum_en.lean Spectre de la surjectivité locale : lattice des conditions de surjectivité locale (faithfully flat, fppf, étale) et leurs rapports —
68 Grothendieck/Spaces.lean Spaces_en.lean Espaces annelés : la structure RingedSpace revisitée pour le contexte topos-théorique (introduction pédagogique, pré-Partie 2) —
69 Grothendieck/CoversEtaleArrow.lean CoversEtaleArrow_en.lean Forme flèche de la topologie étale : instantiation du patron covers_iff_toGrothendieck sur GrothendieckTopology.etale (Phase 5 de #2159, voisinage de Parties 55a-c) —
70 Grothendieck/SpacesMathlib.lean SpacesMathlib_en.lean Espaces Mathlib : index #check des constructions Mathlib liées aux RingedSpace / SheafedSpace / PresheafedSpace — cartographie pédagogique —
71 Grothendieck/SpacesSubcanonical.lean SpacesSubcanonical_en.lean Espaces sous-canoniques : instantiation du critère sous-canonicalité (Partie 16) sur les espaces annelés —
72 Grothendieck/Stalks.lean Stalks_en.lean Tige du représentable : unique_stalk_yoneda, isEmpty_stalk_yoneda et nonempty_stalk_yoneda_iff montrent qu’elle est un singleton si x ∈ U, et vide sinon — premier maillon faisceaux ↔︎ espaces étalés (cf. PR #14903) 110
73 Grothendieck/StalkPoints.lean StalkPoints_en.lean Le foncteur fibre du point est la tige : opensPoint et l’isomorphisme naturel stalkFiberIso réalisent le TODO explicite de Mathlib Topology/Sheaves/Points.lean (SGA 4 IV 6.3 ; cf. PR #14919) 210
74 Grothendieck/StalkSeparated.lean StalkSeparated_en.lean Les tiges détectent l’égalité des sections (préfaisceau séparé) : eq_of_germ_eq_of_isSeparated — relâchement séparé du section_ext Mathlib (cf. PR #15416) 154
75 Grothendieck/StalkGluing.lean StalkGluing_en.lean Recollement des familles de germes : toute famille localement représentable provient d’une unique section globale ; reformulation comme surjectivité vers le sous-type GermFamily.IsLocallyRepresentable 161
76 Grothendieck/StalkCharacterization.lean StalkCharacterization_en.lean Caractérisation du faisceau par les tiges : l’équivalence IsSheaf F ↔︎ <séparation par les germes> ∧ <recollement des familles localement représentables> — le capstone des Parties 74-75, et le seul endroit du lake où la condition de faisceau est dérivée plutôt que consommée (via isSheaf_of_isSheafUniqueGluing_types) 152
77 Grothendieck/Skyscraper.lean Skyscraper_en.lean Le faisceau gratte-ciel : support et tiges — support (skyscraper p₀ A) = closure {p₀}. Mathlib énonce les deux isomorphismes de tige (skyscraperPresheafStalkOfSpecializes, ...OfNotSpecializes / ...IsTerminal) mais ne pose nulle part la notion de support ni le calcul du sien ; cette partie les assemble, nomme l’hypothèse nécessaire IsEmpty (IsTerminal A) (sans elle le support est vide), en déduit le corollaire pour p₀ fermé (= {p₀}) et la dichotomie des tiges point par point 175
78 Grothendieck/SerreMap.lean SerreMap_en.lean Le miroir Serre de la Partie 4 : index #check du versant Serre du pont Serre–Grothendieck dans Mathlib — classes de Serre (définition + clôture deux-sur-trois + instance groupes abéliens finis), localisation de Serre + Gabriel–Popescu, perfection au sens de Serre (PerfectRing, PerfectField.ofFinite instancié sur ZMod 7), construction de Serre (Matrix.ToLieAlgebra, exceptionnelles), dérivée de Serre, domaine fondamental (Cours d’arithmétique VII), DVR (Corps locaux) — et la liste honnête des absents (GAGA, dualité, FAC, R1+S2, Quillen–Suslin, Hochschild–Serre, Serre-noethérien). #16334 170
79 Grothendieck/Flasque.lean Flasque_en.lean Faisceaux flasques, du topologique au site — IsFlasqueSieves P : toute famille compatible sur tout crible (couvrant ou non) s’amalgame, la version site de la flasquité que Mathlib ne pose nulle part (Mathlib.Topology.Sheaves.Flasque couvre le seul topologique). Conséquences : nonempty_obj_of_isFlasqueSieves (le crible vide force des sections sur tout objet — subtilité invisible à la définition topologique), isSheaf_of_isFlasqueSieves_of_isSeparated (flasque + séparé ⇒ faisceau, chaînage explicite de IsSeparated.isSheaf : existence par flasquité, unicité par séparation), isFlasqueSieves_const_of_subsingleton (le préfaisceau constant n’est flasque que sur un sous-singulier non vide), deux ponts vers Mathlib (pushforward_isFlasque_bridge image directe Partie 33, isFlasque_skyscraper_bridge gratte-ciel Partie 77). God58 II.3, SGA 4 II, MM92 II.3 Ex. 9. 184
80 Grothendieck/FlasqueStability.lean FlasqueStability_en.lean Stabilité de la flasquité : isomorphismes, produits, frontière de l’acyclicité — isFlasqueSieves_of_iso (invariance par isomorphisme : famille transportée par e.inv, amalgamation revenue par e.hom, compatibilité par naturalité), isFlasqueSieves_pi (tout produit de préfaisceaux flasques est flasque, Godement II.3.2 : la famille se projette composante par composante via piObjIso, chaque composante s’amalgame, le vecteur des amalgamations amalgame — stabilité que Mathlib n’enregistre ni côté topologique ni côté sites), subsingleton_H_succ_of_flasque_of_injective (croisement Partie 20 × Partie 79 : flasque et injectif ⇒ H^{n+1} trivial, consommant l’instance Mathlib d’annulation ; le maillon manquant flasque ⇒ injectif (II.5.2, par Zorn) explicitement documenté comme frontière du lake). Ligne de lecture : les stabilités sans choix (iso, produit) s’arrêtent exactement là où Zorn devient nécessaire. God58 II.3-II.5, SGA 4 II. 230
81 Grothendieck/FlasqueRetract.lean FlasqueRetract_en.lean La flasquité descend aux rétractes — isFlasqueSieves_of_retract : si Q est rétracte de P (e : P ⟶ Q, s : Q ⟶ P, s ≫ e = 𝟙 Q) et P flasque, alors Q flasque — généralisation unilatérale de l’invariance par isomorphisme (God58 II.3.1, cas symétrique) : la famille se pousse par la section, s’amalgame dans P, revient par e ; naturalités + e ≫ s = 𝟙, aucun choix. Alias isFlasqueSieves_of_retract' (rôles échangés : e ≫ s = 𝟙 P, les deux sens d’une split pair), corollaire isFlasqueSieves_of_iso' (l’iso redéduit en une ligne au rétracte), pont abélien isFlasqueSieves_of_retract_addCommGrp (whiskering droit par forget : la stabilité passe aux préfaisceaux de groupes abéliens, cadre des rétractes utiles). Mathlib n’enregistre rien de tel, même topologique. Prolonge la frontière « sans choix » de la Partie 80 : tout rétracte se transporte canoniquement, seul le maillon Zorn flasque ⇒ injectif (God58 II.5.2) coûte un choix. God58 II.3.1, SGA 4 II, croisements P79/P80. 164
82 Grothendieck/FlasqueExact.lean FlasqueExact_en.lean Du crible à l’épi — exists_isAmalgamation_of_sieveTop (le crible maximal amalgamate toujours, sans hypothèse sur P : la flasquité de cribles est une condition sur les cribles propres), exists_lift_of_isFlasqueSieves_of_mono (flasque de cribles ⇒ prolongement le long de tout mono, site arbitraire — la lecture « sous-objet » du prolongement des sections), exists_isAmalgamation_of_isFlasque_generate_singleton (réciproque partielle : Presheaf.IsFlasque ⇒ amalgamation sur tout crible engendré par une flèche unique ; l’écart résiduel vers IsFlasqueSieves = exactement les cribles multi-générateurs), et epi_of_shortExact_of_isFlasqueSieves (Godement II.3 côté sites : la preuve Zorn de Mathlib epi_of_shortExact ne consomme la flasquité de X₁ qu’une seule fois, sur homOfLE inf_le_right — la reprise locale avec substitution de ce seul maillon par le prolongement mono montre que « epi sur toute flèche » cède à « amalgamation sur tout crible » : le théorème de la suite exacte courte vit déjà dans le monde des sites). Frontière documentée : la réciproque complète exigerait Zorn sur les familles multi-flèches. God58 II.3/II.5, SGA 4 II, MM92 II.3/III.4. 235
83 Grothendieck/FlasqueQuotient.lean FlasqueQuotient_en.lean Le pont se referme — isFlasque_of_isFlasqueSieves (pont retour : flasque de cribles ⇒ flasque au sens Mathlib pour toute flèche de Opens X — le site est mince, toute flèche y est mono, le relèvement mono de la Partie 82 s’applique à chaque restriction, sans hypothèse de faisceau), isFlasqueSieves_of_isFlasque_of_isSheaf (pont aller : faisceau + flasque Mathlib ⇒ flasque de cribles, sans Zorn — la frontière multi-générateurs de la Partie 82 disparaît sur Opens X : le supremum V₀ des membres du crible borne la famille dans le treillis des ouverts, la condition de faisceau y colle la famille (presieveOfCovering.mem_grothendieckTopology), la flasquité étend la section de V₀ à U), et isFlasqueSieves_of_shortExact_of_isFlasque₁₂ (Godement II.3.1 seconde moitié côté cribles : X₁ et X₂ flasques de cribles ⇒ X₃ flasque de cribles, miroir de TopCat.Sheaf.IsFlasque.of_shortExact_of_isFlasque₁₂ — l’épi de S.g vient de la Partie 82, les restrictions de X₂ du pont retour, la conclusion du pont aller). Sur Opens X, les deux flasquités coïncident pour les faisceaux. God58 II.3.1, SGA 4 II, MM92 II.3. 206
84 Grothendieck/Godement.lean Godement_en.lean Le faisceau de Godement C⁰ : sections discontinues — godementPresheaf (U ↦ ∏_{x ∈ U} Fₓ, le produit des tiges (P73), sans aucune condition de continuité), isFlasque_godementPresheaf (C⁰F flasque sans hypothèse sur F : extension par zéro hors de U, le zéro des tiges rend le prolongement toujours possible — consomme Presheaf.IsFlasque Mathlib), isSheaf_godementPresheaf (C⁰F est un faisceau : recollement pointwise via isSheaf_iff_isSheafUniqueGluing, le choix de l’indice par point est inoffensif car la compatibilité, pour des sections qui SONT des fonctions, est une égalité pointwise), injective_toGodement_of_isSheaf (l’unité germe F → C⁰F est injective si F est faisceau : germ_eq fournit un voisinage par point, ⨆ W = U, unicité du recollement — toutes les égalités de morphismes d’ouverts passent par Subsingleton). Construction absente de Mathlib (vérifié v4.33.0, 0 hit) ; ouvre la voie à la résolution canonique de Godement (itérer C⁰ sur les noyaux), fil prochain. God58 II.4.1, croisements P73/P79-P83. 218
85 Grothendieck/GodementFunctor.lean GodementFunctor_en.lean La fonctorialite de C⁰ : l’endofoncteur et son unite — le prerequis manquant pour iterer la construction sur les noyaux (resolution canonique de Godement). godementHomApp (l’action d’un morphisme φ : F ⟶ G sur les sections de Godement, point par point dans les tiges via Presheaf.stalkFunctor : une section est une fonction choisie librement, aucune compatibilite a verifier), godementFunctor (C⁰ est un endofoncteur de X.Presheaf AddCommGrpCat — identite et composition sont celles des tiges, map_id/map_comp gratuits, comme la flasquitude de la Partie 84 : tout vient de ce que C⁰ est un produit d’evaluations), toGodementNatTrans (l’unite F → C⁰F est naturelle — 𝟭 ⟶ C⁰, cas de Presheaf.stalkFunctor_map_germ_apply : le germe du morphisme est le morphisme des germes), ce qui permet d’ecrire le premier pas du complexe de Godement. La preservation des monomorphismes par C⁰ n’est pas etablie ici. God58 II.4.1, suite de P84. 138
86 Grothendieck/GodementMono.lean GodementMono_en.lean C⁰ préserve les monomorphismes — le prérequis nommé par la Partie 85 est fermé — injective_app_of_mono (un mono φ : F ⟶ G de préfaisceaux de groupes abéliens est injectif sur chaque ouvert : NatTrans.mono_iff_mono_app lit le mono d’une transformation naturelle composante par composante, et AddCommGrpCat.mono_iff_injective identifie mono et injection), godementHomApp_injective (l’injectivité descend aux tiges : deux sections de Godement dont les images coïncident en chaque point coïncident, l’application induite sur les tiges étant injective — Presheaf.stalkFunctor_map_injective_of_app_injective, valable pour tout préfaisceau), godementMapHom_mono (C⁰φ est un mono : l’injectivité section par section est le mono dans AddCommGrpCat), et l’instance godementFunctor_preservesMonomorphisms (C⁰ est un foncteur qui préserve les monomorphismes — Functor.map_mono s’applique désormais à C⁰). C’est le prérequis qui manquait pour itérer C⁰ sur les noyaux et former le complexe de Godement 0 → F → C⁰F → C⁰(K) → ⋯. God58 II.4.1, suite de P85. 99
87 Grothendieck/GodementResolution.lean GodementResolution_en.lean La suite des unités itérées F → C⁰F → C⁰²F est posée — et ce n’est pas la résolution canonique : godementUnitIter (le morphisme C⁰F ⟶ C⁰²F, l’unité toGodement réappliquée au préfaisceau C⁰F), le témoin godementUnit_comp_injective (sur les faisceaux, le composé μ ≫ μ(C⁰F) est injectif — composé de l’unité injective sur les faisceaux et de l’unité réappliquée injective sans hypothèse — donc cette suite de morphismes n’est pas un complexe : μ ≫ d⁰ = 0 est faux pour ce morphisme, ce n’est pas un énoncé différé), et godementUnit_injective_of_isSheaf (l’exactitude en F de 0 → F → C⁰F, mono sur les faisceaux — seul fait d’exactitude posé). La vraie différentielle de la résolution canonique (conoyau de l’unité, God58 II.4.1) et l’acyclicité H^n(C⁰F) = 0 pour n ≥ 1 sont la frontière nommée de la Partie 89. 110
88 Grothendieck/GodementAcyclicity.lean GodementAcyclicity_en.lean L’allongement de la suite des unités d’un maillon : le morphisme C⁰²F ⟶ C⁰³F (godementUnitIter_at_iterate = l’unité réappliquée au préfaisceau itéré C⁰F), l’égalité de définition rfl (godementUnitIter_at_iterate_def) et l’extension structurelle de la suite de deux à trois flèches (godementUnitChain_extends). Aucune propriété de complexe, de null-composition ni d’acyclicité H^n(C⁰F) = 0 n’est posée ni promise : la suite des unités n’est pas un complexe (godementUnit_comp_injective, P87), et ces questions exigent d’abord la vraie différentielle (conoyau de l’unité, God58 II.4.1) — frontière nommée de la Partie 89. ~110
89 Grothendieck/GodementCanonicalDiff.lean GodementCanonicalDiff_en.lean Le pas canonique de Godement : la frontière nommée est traitée — godementStep (pour tout f : A ⟶ B, la composée B ⟶ C⁰(coker f) : projection du conoyau puis unité du conoyau — le motif uniforme de la résolution canonique), comp_godementStep_zero (la null-composition du pas canonique est prouvée : f ≫ godementStep f = 0 par la condition universelle du conoyau — deux réécritures), godementCanonicalDZero (la différentielle de degré 0 d⁰ = godementStep μ : C⁰F ⟶ C⁰(coker μ)) et toGodement_comp_godementCanonicalDZero (μ ≫ d⁰ = 0 : le début de la résolution augmentée 0 → F → C⁰F → C⁰(coker μ) est un complexe — le contraire exact du témoin P87 pour l’itération, qui était injectif donc non nul). L’exactitude en C⁰F (ker d⁰ = im μ), l’itération du pas (d¹, d², …) et l’acyclicité H^n(C⁰F) = 0 restent la frontière nommée de la Partie 90. 109
90 Grothendieck/GodementExactness.lean GodementExactness_en.lean Le complexe au-delà du degré 0 et le mono catégorique de l’unité — godementCanonicalDOne (la différentielle de degré 1 d¹ = godementStep d⁰ : C¹F ⟶ C⁰(coker d⁰) — le motif itératif de P89 appliqué à d⁰), godementCanonicalDZero_comp_godementCanonicalDOne (d⁰ ≫ d¹ = 0 : la résolution canonique est un complexe au-delà du degré 0, instance directe de comp_godementStep_zero — chaque degré suivant est gratuit par le même argument) et mono_toGodement_of_isSheaf (l’unité F → C⁰F est un monomorphisme catégorique sur les faisceaux : la montée catégorique de l’injectivité section par section de P84 (godementUnit_injective_of_isSheaf) via NatTrans.mono_iff_mono_app + AddCommGrpCat.mono_iff_injective — l’exactitude de 0 → F → C⁰F en F, désormais énoncée dans le langage des complexes). Note de l’auteur : la réduction de l’exactitude en C⁰F au mono de l’unité du conoyau (exact_toGodement_godementCanonicalDZero_of_mono, draft r65) a été retirée de cette Partie — sa preuve exigeait la séparéité du conoyau pour F faisceau (recollement de [God58] II.4.1) et un sorry tactique devenu sorryAx transitif à l’import (classe forbidden §B). La frontière honnête est reportée à la Partie 91, qui procédera par construction directe du recollement et placera les instances IsIso/Mono au site d’usage. L’itération complète de la réduction aux degrés supérieurs et l’acyclicité H^n(C⁰F) = 0 pour n ≥ 1 ([God58] II.5) restent du périmètre P91. 124
35 (complément) Grothendieck/ExceptionalTriple.lean ExceptionalTriple_en.lean Triade d’images exceptionnelles : f_! ⊣ f^* ⊣ f_* au niveau préfaisceau — complément à la Partie 35, autour de l’image réciproque (pont avec Partie 34 ExceptionalDirect et Partie 33 DirectImage) —
hors-série Grothendieck/Fppf.lean Fppf_en.lean Topologie fppf : forme flèche de la topologie fidèlement plate de présentation finie — module sans numéro de Partie déclaré —

La colonne Lignes compte le fichier FR seul ; le sibling _en ajoute approximativement autant.

Build & état

  • Toolchain : leanprover/lean4:v4.33.0 (cf. lean-toolchain du lake ; migration v4.32.1 → v4.33.0 survenue post-#11294, attestée par git log -- lean-toolchain)

  • Build : lake build (WSL requis). La cible défaut (globs := #[Grothendieck.*]dulakefile.lean) compile **tous** les modules FR et_en(1 umbrella + les leaf FR, plus les modules_en; les comptes exacts sont mesurés pargit ls-tree -r HEAD). Dernier build vérifié sur la branche de cette PR :lake build GrothendieckSUCCESS local (cf. §Validation du body PR — preuve jointe). Le compte disque (leaf FR, leaf_en, umbrella) est mesuré par le checker anti-récidivescripts/lean/check_grothendieck_readme.py` (sortie JSON, exit code non-zéro sur dérive).

  • Preuves : 0 sorry, 0 axiome ajouté — tous les modules sont complets à la création. (Un grep sorry naïf matche des mentions en prose dans les docstrings bilingues, notamment deux dans ExceptionalDirect.lean ; la CI compte en mode real — après strip des commentaires — et vaut 0.)

  • Dépendances : Mathlib 4 (via lakefile.lean)

  • i18n (EPIC #4980, convention Option A ratifiée 2026-07-04) : couverture bilingue complète — les fichiers FR (1 umbrella Grothendieck.lean + les leaf canoniques mesurés par git ls-tree -r HEAD) et leurs siblings _en.lean, ratio 1:1 intégral (vérifié par scripts/lean/check_i18n_siblings.py). L’historique « gap PullbackFunctor.lean sans _en » est clos depuis c.2026-08-18 : PullbackFunctor_en.lean est sur disque, et les modules FR ont leur sibling _en. Namespaces _en anti-collision, contenu non-docstring byte-identique, vérifiable par CI. L’umbrella est un index FR-only : il importe chaque leaf FR et jamais un _en (invariant #16154, tenu par l’organe always-on scripts/ci/check_grothendieck_umbrella.py). README.en.md est le miroir EN du présent fichier. Hors-scope : .lake/packages/, libs vendored.

Note de cohérence : couverture 1:1 intégrale — les leaf FR canoniques et leurs siblings _en (le gap PullbackFunctor sans _en, nommé dans une version antérieure de cette note, est comblé sur disque). Le globs du lakefile auto-découvre tous les modules présents, FR comme _en. Vérification reproductible : python scripts/lean/check_grothendieck_readme.py — sortie non-zéro sur tout écart entre prose et disque.

Références

Le langage visité ici — topologies de Grothendieck, sites, faisceaux, schémas — naît de la géométrie algébrique de Grothendieck. Voici les points d’entrée canoniques ; ce workspace est une visite indexée sur Mathlib, pas une formalisation d’EGA/SGA.

  • Mac Lane, S.; Moerdijk, I. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer Universitext, 1992. — La référence standard pour topologies de Grothendieck, cribles, sites et faisceaux (Parties 1, 6-8, 10, 13-14).
  • Artin, M.; Grothendieck, A.; Verdier, J. L. (éd.) Théorie des topos et cohomologie étale des schémas (SGA 4). Springer Lecture Notes in Mathematics 269, 270, 305, 1972-1973. — L’origine des sites, topologies de Grothendieck et points d’un topos (Parties 1, 15, 19).
  • Grothendieck, A.; Dieudonné, J. Éléments de géométrie algébrique (EGA). Publications Mathématiques de l’IHÉS, 1960-1967. — L’origine des schémas et du site de Zariski (Parties 2-3).
  • Vakil, R. The Rising Sea: Foundations of Algebraic Geometry. — Notes pédagogiques largement utilisées, dans l’esprit grothendieckien.
  • The Stacks Project. stacks.math.columbia.edu — Référence pour schémas, faisceautisation et cohomologie des faisceaux (Parties 13, 20-23).
  • The Mathlib Community. Mathlib4, Category Theory and Sites. mathlib4 docs — La bibliothèque que cette visite indexe (Partie 4) ; voir de Moura & Ullrich, « The Lean 4 Theorem Prover » (2021).
  • nLab. ncatlab.org — Entrées Grothendieck topology, sieve, site, sheaf, sheafification.

Voir aussi

  • Epic #1646 (hommage à Grothendieck) — Issue #2159 (profondeur de formalisation : Phase 1 shippée, Phase 2 = #10357, Phase 5 = Parties 35-44, Parties 64-77 par la suite)
  • EPIC #4980 — convention i18n Lean (Option A sibling pair ; les paires _en dans ce lake, ratio 1:1)
  • Epic #1453 (calibration du harnais prouveur) — Issue #8960 (réconciliation des numérotations Partie)
  • #11286 — CLOSED 2026-08-16 (PR #11294 MERGED) : import umbrella de ExceptionalDirect réalisé ; l’orphelin de #10357 a vécu 6 semaines avant ce merge
  • Workspace hommage Conway (../conway_lean/) — série de notebooks Lean (../README.md)
  • README.en.md — miroir EN du présent fichier

Le périmètre, honnêtement

Chaque résultat est pleinement prouvé (0 sorry, 0 axiome ajouté), et l’index #check de la Partie 4 documente explicitement la frontière entre ce que Mathlib possède et ce qu’il n’a pas (encore) — la visite expose cette frontière au lieu de la maquiller. Le module compagnon Calibration.lean (Partie 5) relie la formalisation à l’effort de preuve plus large.

Cet hommage est un index curaté qui laisse les apprenants voir la bibliothèque à travers des yeux grothendieckiens ; l’Issue #2159 / l’Epic #1646 suivent la formalisation ultérieure — cette visite est le socle, pas le plafond. Pour prolonger : conway_lean/ et la série de notebooks Lean côté compagnons ; Mac Lane–Moerdijk et SGA 4 pour le cœur topos-théorique ; Vakil et le Stacks Project pour les schémas et la cohomologie.

Digestion (grille #13106)

Digestion de premier niveau du lake contre la grille obligatoire de #13106 (EPIC digestion et canonicalisation). Verdicts sur la base du README, des docstrings de modules et des issues de formalisation — marqués PRÉSENT/PARTIEL/ABSENT avec la preuve file:line vérifiée. Un digest plus fin (reconstruction du chemin de chaque Partie) reste à faire par des grains dédiés.

# Point de la grille Verdict Preuve / état
1 Énoncé exact + niveau de garantie PRÉSENT modules Grothendieck/*.lean ; garantie « 0 sorry, 0 axiome ajouté » (README.md §Build & état, lakefile.lean globs)
2 Provenance, littérature, priorité, attribution PARTIEL §Références (README.md: Mac Lane–Moerdijk, SGA 4, EGA, Vakil, Stacks, Mathlib, nLab) + docstrings citant SGA 4 I/II (§ CategoryAndSites.lean:1-20) ; l’attribution par Partie (quel auteur, quel snip) n’est pas systématique
3 Nouveauté réelle vs dépendances PARTIEL « vit déjà dans Mathlib 4 », frontière indexée par la Partie 4 (#check) ; pas d’énoncé explicite « ce que ce lake ajoute à Mathlib »
4 Carte deps / toolchain / axiomes PRÉSENT §Build & état (README.md) : toolchain v4.33.0 (cf. lean-toolchain ; migration v4.32.1 → v4.33.0 attestée par git log -- lean-toolchain), dépendance Mathlib (db584cd6 per lakefile.lean), 0 axiome ajouté ; i18n #4980
5 Trivial vs nouveau développé PARTIEL la trajectoire (sites→faisceaux→cohomologie) hiérarchise, mais le trivial/nouveau n’est pas déclaré partie-par-partie
6 Friction naturelle (obstacles, essais ratés, dette) ABSENT→comblé ci-dessous §Le périmètre, honnêtement + Classifier.lean:190 (« ElementaryTopos pas encore disponible »), #11286 (import umbrella ExceptionalDirect en attente), phases #2159/#10357
7 Chemin de découverte vs reconstruction ABSENT→comblé ci-dessous la trajectoire est pédagogique mais n’explicite pas le « pourquoi cet ordre / ce qu’on a écarté »
8 Limites, claims non établis, réserves PRÉSENT §Le périmètre, honnêtement : « socle, pas plafond », frontière Mathlib exposée
9 Raccord corpus + prérequis PRÉSENT navlinks Lean-15-Grothendieck-Tribute.ipynb / Lean-15b-Lean-Grothendieck.ipynb / Lean-15c-Lean-Grothendieck-Companion.ipynb (re-lient le lake) ; §Voir aussi

Point 6 — friction naturelle (comblement)

Quatre frictions réelles, documentées à la source :

  1. Contrainte d’anti-régression auto-imposée : chaque module complet à la création (0 sorry, 0 axiome ajouté) — le plafond du lake est borné par ce que Mathlib expose déjà, pas par un choix de sous-formalisation. C’est une friction de périmètre : quand un concept manque dans Mathlib, il est soit reconstruit localement, soit renvoyé en attente.
  2. Frontière Mathlib vivante : Classifier.lean:190 — ElementaryTopos « pas encore disponible dans cette révision » : la borne du lake est mobile avec Mathlib.
  3. Dette de raccord résolue : #11286 — import umbrella de ExceptionalDirect CLOSED 2026-08-16 (PR #11294) : un module orphelin depuis #10357, relié en 6 semaines. L’umbrella importe chaque leaf FR et jamais un _en (#16154), tandis que le globs du lakefile assure aussi la compilation des 83 siblings _en.
  4. Friction i18n historique résolue : l’absence d’un sibling _en pour PullbackFunctor (comblée depuis c.2026-08-18, cf §Build & état) — la paire bilingue est une contrainte de maintenance vérifiable par scripts/lean/check_i18n_siblings.py.

Point 7 — chemin de découverte (comblement)

Le chemin n’est pas une reconstruction — c’est une visite indexée, et ce fait est la découverte centrale : « le langage grothendieckien vit déjà dans Mathlib 4 ». L’ordre pédagogique (sites → cribles/topologies → faisceaux → faisceautisation → cohomologie, ancré par Spec/Zariski et par l’index #check) est un chemin de lecture, pas la trace d’un développement. Le point d’entrée pour un apprenant : README → compagnons (Lean-15*) → modules, avec Mac Lane–Moerdijk et SGA 4 comme lecture d’accompagnement. Ce qui a été écarté et pourquoi (le choix « hommage, pas formalisation d’EGA/SGA ») est explicite dans §L’esprit de la visite et §Le périmètre, honnêtement — mais la trace du développement réel (quels tentatives ont été abandonnées) n’est pas consignée par Partie ; c’est la limite de cette digestion, à compléter par un grain qui interroge les auteurs.

Retour au sommet