[jsboige]

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/guard #14065

Summary

Partie 66 de l'hommage Grothendieck (Epic #2159, Extension Phase 2) : le spectre de topologies d'un préfaisceau — Spec(P) = {J | P est un faisceau pour J}. Après la Partie 65 (caractérisation égaliseur pour une topologie FIXÉE) et la Partie 7 (isSheaf_of_le, descente le long de J₁ ≤ J₂), ce module fait porter la question sur la coordonnée topologie. Trois théorèmes, zéro sorry à la création :

Théorème	Énoncé	Preuve
isSheaf_const_unit	le préfaisceau constant singleton est un faisceau pour TOUTE topologie — son spectre est le treillis entier	Subsingleton général (instance Pi sur tous les objets, pas seulement le point d'amalgame)
isSheaf_inf	Spec(P) stable par infimum binaire : faisceau pour J₁ et J₂ ⇒ faisceau pour J₁ ⊓ J₂	Grothendieck.TopologyLattice.inf_covering (décomposition de l'appartenance à l'infimum)
isSheaf_iInf	version indexée : faisceau pour chaque J i ⇒ faisceau pour ⨅ i, J i	iInf_covering + Classical.arbitrary

Pourquoi Nonempty ι est nécessaire (documenté dans la docstring) : sur une famille vide, ⨅ i, J i est la topologie maximale (tout crible couvre), qui n'admet pas tous les préfaisceaux comme faisceaux.

Pourquoi pas un 4e théorème isSheaf_prod : Mathlib CategoryTheory/Sites/Limits.lean ferme déjà Presheaf.IsSheaf sous les limites — le réénoncer ici serait un corollaire d'instance, pas un théorème. Le choix s'est porté sur la coordonnée topologie (composant le propre TopologyLattice du lake), non couverte sous cette forme.

Livrables

• Grothendieck/SheafTopologySpectrum.lean (FR canonique) — nouveau module, 3 théorèmes
• Grothendieck/SheafTopologySpectrum_en.lean (sibling EN, modèle pair i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980) — namespace Grothendieck_en, docstrings EN, énoncés/preuves byte-identiques
• Grothendieck.lean — 2 imports d'agrégateur (lignes 62-63)

Validation

Relancée après le commit final 2c827bac7a :

• lake build Grothendieck.SheafTopologySpectrum Grothendieck.SheafTopologySpectrum_en : Build completed successfully (929 jobs) — les deux cibles vertes localement (Mathlib peuplé via lake exe cache get, exit 0). Premier passage rouge (3 erreurs mécaniques : application directe Functor.const Cᵒᵖ PUnit vs forme .obj du Mathlib vendored, h₂ non référencé, Classical.arbitrary sans type explicite) — corrigé symétriquement dans le module FR et le sibling EN, re-build vert.
• B.1 sorry count : python scripts/lean/count_code_sorry.py --json → grothendieck_lean : distinct_code_sorry = 0 (126 fichiers, naive_sorry = 114 = prose docstrings, vacuous: []). Avant/après : 0 → 0, création sans sorry.
• B.2/B.3 : build local SUCCESS ci-dessus ; proof-integrity CI : target-modules: "*" + fail-on-sorry: true (lean-grothendieck.yml) — couvre le module nouveau ET l'agrégateur (2 imports ajoutés, lignes 62-63). B.3 est applicable, câblé sur "*".
• i18n sibling checker : check_i18n_siblings.py <FR> <EN> → 1/1 pairs byte-identical (0 drift, 0 orphan, 0 unbuilt), re-vérifié APRÈS les edits de fix.
• Anti-collision noms : grep isSheaf_const_unit|isSheaf_inf|isSheaf_iInf hors fichiers du module → 0 hit dans le lake.
• Régression : aucun fichier existant modifié hormis les 2 lignes d'import de l'agrégateur ; pas de suppression de contenu (226 insertions, 0 délétion).

Voir aussi

See #2159 (Partie 66, l'Epic reste ouverte), See #1646.