feat(lean,#2159): Partie 73 -- point du site des ouverts, iso presheafFiber = stalk (TODO Mathlib)

[jsboige]

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: LIGHT/docs #14906

Summary

Partie 73 de l'Epic #2159 (Grothendieck hommage, Phase 2) : point du site des ouverts associé à un point x, et identification du foncteur fibre avec la tige — nouveau module Grothendieck/StalkPoints.lean (+ jumeau i18n StalkPoints_en.lean, convention #4980).

• Le point du site opensPoint T x : GrothendieckTopology.Point (opensTopology T) : transcription sur le site own du point canonique Opens.pointGrothendieckTopology de Mathlib (la fibre en U est l'ensemble au plus singleton des éléments de U égaux à x), avec jointly_surjective prouvé via notre propre mem_opensTopology_iff (Partie 70) — l'égalité des topologies garantit qu'il s'agit du même point.
• Résultat principal — stalkFiberIso : (opensPoint T x).presheafFiber.obj F ≅ stalk F x pour tout préfaisceau F sur Opens T. C'est le TODO explicite de Mathlib (Topology/Sheaves/Points.lean : « Redefine the stalks functors in Stalks.lean using GrothendieckTopology.Point.presheafFiber ») — l'iso n'existe pas dans Mathlib (vérifié : 0 occurrence de presheafFiber dans Topology/Sheaves/Stalks.lean), il est ici établi côté lake.
• Stratégie — double passage à la colimite : les germes forment un cône sur le diagramme des éléments de la fibre (germ_res), les toPresheafFiber forment un cône sur le diagramme des voisinages (toPresheafFiber_w) ; les deux descentes universelles (fiberToStalk, stalkToFiber) se répondent via colimit.ι_desc et les deux lemmes d'extension (stalk_hom_ext, presheafFiber_hom_ext) donnent les deux sections identité.
• Naturalité : stalkFiberIso_naturality — l'iso entrelace presheafFiber.map et stalkFunctor.map ; la tige EST le foncteur fibre du point, en tant que foncteurs et pas seulement objet par objet.
• Jonction : soude la théorie abstraite des points d'un site (Partie 15, SGA 4 IV 6.3) au calcul concret des tiges (Partie 72) — le premier maillon du dictionnaire points de l'espace ↔ fibres, au cœur de la théorie des topos (MM92 Chap. II §3).

Anti-régression (§B)

• sorry : count_code_sorry.py --json — 0 avant / 0 après (nouveaux fichiers uniquement, aucune preuve existante touchée ; grothendieck_lean : 143 fichiers, distinct_code_sorry: 0).
• lake build Grothendieck.StalkPoints Grothendieck.StalkPoints_en : SUCCESS — Build completed successfully (1417 jobs) (commit local prouvable, worktree feature/2159-p73-stalk-points).
• Proof integrity : job câblé sur ce lake (lean-grothendieck.yml → lean-axiom.yml), à lire au passage de la CI.
• i18n : check_i18n_siblings.py — paire FR/EN byte-identique hors docstrings/commentaires.

See #2159

[jsboige]

[Hermes] — #14919 review LIGHT (Partie 73, StalkPoints.lean)

1. ✅ Zéro sorry — les 2 seules occurrences dans le diff sont les commentaires d'en-tête « Aucun sorry introduit » ; aucune tactique sorry dans le corps (FR ni _en).
2. ✅ Jumeaux i18n symétriques — StalkPoints.lean / StalkPoints_en.lean suivent le même squelette déclaration-à-déclaration (opensPoint 77↔301, jointly_surjective 88↔312, stalkFiberIso_naturality 194↔417), convention #4980 respectée.
3. ✅ Scope borné aux 2 nouveaux fichiers, aucune preuve existante touchée. Security scan : 0 match.
4. ℹ️ Le build+axioms passe par le CI lean-grothendieck.yml (déclenché par grothendieck_lean/**.lean) — non rejoué localement sur cette machine de review ; verdict structurel seulement, le vert CI reste la preuve de compilation.

Point d'intérêt : stalkFiberIso répond au TODO explicite de Mathlib Topology/Sheaves/Points.lean — belle continuité de l'Epic #2159. (contrainte token : COMMENT only)