Add: Grothendieck Partie 81 - la flasquite descend aux retractes (#2159)

[jsboige]

Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: DEEP/lean #16980

Grothendieck Partie 81 — la flasquité descend aux rétractes

Suite du fil God58 II.3 (P79 IsFlasqueSieves → P80 stabilités iso/produits → P81 rétractes). See #2159 (Epic #1646, Phase 2).

Contenu

• isFlasqueSieves_of_retract (théorème principal) : si Q est un 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) : une seule composition égale à l'identité suffit. Preuve : la famille se pousse par la section s (compatibilité par naturalité), s'amalgame dans P, revient par e ; la conclusion est (s ≫ e).app z = z appliquée par congrFun (congrArg (fun φ => φ.app _) h).
• isFlasqueSieves_of_retract' : rôles échangés (e ≫ s = 𝟙 P : P rétracte de Q) — le même théorème renommé, les deux sens d'une split pair nommés pour la consommation aval.
• isFlasqueSieves_of_iso' : l'invariance par iso redéduite en une ligne du rétracte (e.inv_hom_id) — doublon délibéré du th1 de la Partie 80 (PR Add: Grothendieck Partie 80 - stabilite de la flasquie (iso, produits, frontiere acyclicite) #16980 en review) : ici il témoigne que le rétracte est la généralisation.
• isFlasqueSieves_of_retract_addCommGrp : pont abélien — le rétracte se transporte par forget (right whiskering : Functor.whiskerRight, égalité par ← Functor.whiskerRight_comp, h, Functor.whiskerRight_id'), donc la flasquité lue à travers forget descend aux rétractes de préfaisceaux AddCommGrpCat.

Lecture conceptuelle (prolonge P80) : ce qui se transporte sans choix, ce n'est pas seulement l'isomorphisme — c'est tout rétracte. La frontière « sans choix vs Zorn » de la P80 est confirmée : un rétracte ne coûte aucun choix, le maillon flasque ⇒ injectif (God58 II.5.2) en coûte un.

Validation (B — Lean)

1. Compte sorry : python scripts/lean/count_code_sorry.py --json → grothendieck_lean distinct_code_sorry: 0 avant et après (aucun sorry introduit ; l'instrument, pas grep).
2. lake build SUCCESS : build WSL complet du lake (copie ~/p81-build, packages Mathlib 4.33.0 symlinkés) — rc=0, 4634 jobs, deux passes (itération finale + confirmation incrémentale après le rename des sections du sibling). 4 itérations de preuve (inversions d'orientation ≫ corrigées, NatTrans.comp_app est le lemme morphismes → congrFun/congrArg, Functor.whiskerRight_id' pour matcher 𝟙 G).
3. B.3 proof-integrity : applicable et VERTE — correction 2026-09-20T15:37Z (reserve adjoint [ADJOINT -- COMMENT_WITH_CONCERNS] 15:13Z, DM adjoint-pr16980-b3-a90cd30c) : le body disait a tort << non applicable >>. Verifie firsthand : .github/workflows/lean-grothendieck.yml appelle lean-axiom.yml avec target-modules: "*", le check-run proof-integrity / Proof integrity (grothendieck_lean) conclut SUCCESS au head 4fe5a5c (parmi les runs: [('proof-integrity / Proof integrity (grothendieck_lean)', 'completed', 'success')]). Aucun native_decide/sorryAx/Classical.choice : preuves constructives par reecriture, comptage du point 1 a 0.
4. i18n (EPIC i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980) : python scripts/lean/check_i18n_siblings.py .../FlasqueRetract_en.lean → OK 1/1 pairs byte-identical, 0 drift, 0 orphan (leçon du cycle : les noms de section restent byte-identiques entre siblings — corrigé avant commit). Refactor prover : aucun.

Notes pour le merge

• Conflit texte attendu avec Add: Grothendieck Partie 80 - stabilite de la flasquie (iso, produits, frontiere acyclicite) #16980 (P80) : les deux PR insèrent au même endroit de Grothendieck.lean (entre import Grothendieck.Flasque et Fppf) et après la ligne 79 des READMEs. Résolution triviale — ordre final : Flasque, FlasqueRetract, FlasqueRetract_en, FlasqueStability, FlasqueStability_en, Fppf ; READMEs : ligne 80 (P80) puis ligne 81 (P81). Cette PR est basée sur origin/main (pas un stack) volontairement.
• Claim posé sur [Epic Grothendieck] Avancer la formalisation Lean (au-dela de la Phase 1) #2159 avant édition (check_lane_claim.py CLEAR, paths explicites).
• 5 fichiers : 2 nouveaux .lean (164 lignes chacun), agrégateur (+2 imports), README FR/EN (+1 ligne chacun).

🤖 Generated with Claude Code

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #16990 (Add: Grothendieck Partie 81 - la flasquite descend aux retractes (#2159)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- chore(lean,#16154): umbrella Grothendieck FR-only — -17 imports EN + organe anti-derive #16228 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md
• terminal -- lean(#16334): SerreMap/SerreMap_en - miroir Serre de MathlibMap (grain 9) #16374 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md, recouvrement de chemins 60% -- lean(#16334): SerreMap/SerreMap_en - miroir Serre de MathlibMap (grain 9) #16374 est deja sur main.
• terminal -- feat(lean,#2159): Partie 79 — faisceaux flasques : IsFlasqueSieves, du topologique au site #16623 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md, recouvrement de chemins 60% -- feat(lean,#2159): Partie 79 — faisceaux flasques : IsFlasqueSieves, du topologique au site #16623 est deja sur main. (issues communes : [Epic Grothendieck] Avancer la formalisation Lean (au-dela de la Phase 1) #2159) (issues communes : [Epic Grothendieck] Avancer la formalisation Lean (au-dela de la Phase 1) #2159)
• terminal -- Add: Grothendieck Partie 80 - stabilite de la flasquie (iso, produits, frontiere acyclicite) #16980 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md, recouvrement de chemins 60% -- Add: Grothendieck Partie 80 - stabilite de la flasquie (iso, produits, frontiere acyclicite) #16980 est deja sur main. (issues communes : [Epic Grothendieck] Avancer la formalisation Lean (au-dela de la Phase 1) #2159) (issues communes : [Epic Grothendieck] Avancer la formalisation Lean (au-dela de la Phase 1) #2159)

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[jsboige]

Réserve adjoint levée ([DM adjoint-16990-blocked-20260920], audit head 4fe5a5cfb) : « README counts lag new leaf » — traitée en code, commits 4872260e8 + 0288b2e82.

Diagnostic : P80 #16980 a été mergée à 17:42:51Z (e66e2c3f2), après le fork de cette branche — l'arbre final (P80+P81) porte 80 leaf FR + 80 _en, d'où le UNDERCOUNT signalé sur des comptes à 78.

Réparation :

1. 4872260e8 — merge origin/main : lignes de table 80 (FlasqueStability) et 81 (FlasqueRetract) conservées, imports umbrella des deux côtés (3 conflits résolus explicitement, rien d'auto-mergé à la légère) ;
2. 0288b2e82 — comptes corrigés par ancres exactes (12 patches, 6 par README) : 78/79 → 80 leaf, 81 sources FR, 80 paires _en ; numéros de Partie intacts.

Vérification post-fix (relancée sur 0288b2e82) : table FR 80/80 et table EN 80/80 vs git ls-tree HEAD — 0 module manquant, 0 orphelin, claims 80 modules leaf cohérents avec l'arbre. lake build du tree fusionné délégué à lean-matrix CI (chaque côté vert isolément ; le merge n'ajoute que lignes README + imports).

Note ordre de merge : main post-P80 porte encore les comptes stalles 78 — c'est cette PR qui les remplace par l'état cohérent 80 ; le drift n'est pas masqué, il est réparé ici.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16990
head: 0288b2e
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 2aff1eec7103ba929ea590c99aaa04315d3f097021855984adf22e7c6db1ca7b
diff-files: 5
diff-additions: 344
diff-deletions: 12
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]