From 4fe5a5cfb169ffc22d1b3f55f213d6d869c6f641 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sun, 20 Sep 2026 16:59:06 +0200 Subject: [PATCH 1/2] Add: Grothendieck Partie 81 - flasquity descends to retracts (#2159) isFlasqueSieves_of_retract: one-sided generalization of invariance under isomorphism (God58 II.3.1) - a retract of a flasque presheaf is flasque, no choice involved. Alias with roles exchanged, iso corollary re-derived in one line, abelian bridge via right whiskering by forget. FR module + EN sibling (byte-identical code), aggregator imports, READMEs. Co-Authored-By: Claude Sonnet 5 --- .../Lean/grothendieck_lean/Grothendieck.lean | 2 + .../Grothendieck/FlasqueRetract.lean | 164 ++++++++++++++++++ .../Grothendieck/FlasqueRetract_en.lean | 164 ++++++++++++++++++ .../Lean/grothendieck_lean/README.en.md | 1 + .../Lean/grothendieck_lean/README.md | 1 + 5 files changed, 332 insertions(+) create mode 100644 MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/FlasqueRetract.lean create mode 100644 MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/FlasqueRetract_en.lean diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean index d793bb13b4..1b9fae8cbf 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean @@ -40,6 +40,8 @@ import Grothendieck.ExceptionalDirect import Grothendieck.ExceptionalTriple import Grothendieck.Equivalences import Grothendieck.Flasque +import Grothendieck.FlasqueRetract +import Grothendieck.FlasqueRetract_en import Grothendieck.Fppf import Grothendieck.KanExtensions import Grothendieck.LawvereTierney diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/FlasqueRetract.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/FlasqueRetract.lean new file mode 100644 index 0000000000..43139edd5d --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/FlasqueRetract.lean @@ -0,0 +1,164 @@ +/- +Copyright (c) 2026 CoursIA. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Hommage Grothendieck — Partie 81 : la flasquité descend aux rétractes. + +Alexandre Grothendieck (1928-2014). + +Extension Phase 2 (#2159, Epic #1646). + +La Partie 79 a défini la flasquité au niveau des sites +(`Grothendieck.Flasque`, `IsFlasqueSieves`) : toute famille compatible sur +n'importe quel crible possède une amalgamation. La Partie 80 (branche +`feature/grothendieck-partie-80`) a étudié la stabilité par isomorphisme et +par produits. Cette partie généralise le premier maillon : la flasquité +descend le long d'une rétraction **unilatérale**. + + - `isFlasqueSieves_of_retract` : si `Q` est un rétracte de `P` — une + paire `e : P ⟶ Q`, `s : Q ⟶ P` avec `s ≫ e = 𝟙 Q` — et si `P` est + flasque, alors `Q` est flasque. L'invariance par isomorphisme + (Godement II.3.1) en est le cas symétrique (les deux compositions + égales à l'identité) ; ici une seule égalité suffit. La preuve pousse + la famille le long de la section `s`, amalgame dans `P`, et revient + par `e` : la compatibilité suit la naturalité de `s`, la conclusion + celle de `e` et l'égalité `e ≫ s = 𝟙`. + + - `isFlasqueSieves_of_retract'` : la même lecture avec les rôles + échangés — si `e ≫ s = 𝟙 P` et `Q` est flasque, alors `P` est + flasque. C'est le théorème précédent renommé (`P` est alors le + rétracte de `Q`) : les deux sens d'une split pair sont couverts par + un seul énoncé, enregistrés séparément pour la consommation aval. + + - `isFlasqueSieves_of_iso'` : l'invariance par isomorphisme comme + corollaire du rétracte (`e.inv ≫ e.hom = 𝟙`). Doublon délibéré du + théorème de la Partie 80 (branche en cours de review) : ici il + témoigne que le rétracte est bien la généralisation. + + - `isFlasqueSieves_of_retract_addCommGrp` : le pont vers le monde + abélien — pour des préfaisceaux de groupes abéliens, le rétracte se + transporte par `forget` (whiskering), donc la flasquité lue à travers + `forget` descend aussi aux rétractes de préfaisceaux abéliens. C'est + le cadre où vivent les rétractes utiles en pratique (faisceaux + scindés, images directes fendues). + +La lecture conceptuelle, dans le prolongement de la Partie 80 : ce qui se +transporte **sans choix**, ce n'est pas seulement l'isomorphisme — c'est +tout ce qui est rétracte. Une section `s` fournit le transport du retour ; +aucune donnée n'est choisie, tout est canoniquement déplacé. La frontière +établie en Partie 80 (le maillon `flasque => injectif` exige Zorn) est +confirmée : un rétracte ne coûte aucun choix, une extension maximale en +coûte un. + +Références : + - R. Godement, *Topologie algébrique et théorie des faisceaux* [God58], + Chap. II §3 (prop. 3.1 : l'invariance par isomorphisme, dont le + rétracte est la forme unilatérale). + - SGA 4, Exposé II (sites et cribles). + - Partie 79 (`Grothendieck.Flasque`) : `IsFlasqueSieves`. + - Partie 80 (`Grothendieck.FlasqueStability`, branche + `feature/grothendieck-partie-80`) : invariance par iso, produits, + frontière de l'acyclicité. + +Convention i18n (EPIC #4980 ratifiée 2026-07-04) : ce module est jumelé avec +sa version anglaise canonique dans le fichier sibling +`Grothendieck/FlasqueRetract_en.lean` — suffixe `_en` sur le namespace +(`Grothendieck.FlasqueRetract_en`), imports identiques, docstrings et +commentaires traduits. Les énoncés de théorèmes, tactiques Lean, noms de +lemmes et références Mathlib restent en anglais (Mathlib 4, tactic DSL +standard). Seules les docstrings `/-- ... -/` et commentaires `-- ...` +diffèrent entre les deux fichiers. Anti-§D byte-identity garanti : le +namespace body est préservé bit-à-bit (énoncés et preuves byte-identiques +entre `FlasqueRetract.lean` et `FlasqueRetract_en.lean`). + +Epic #1646, Phase 2 (#2159). Tous les `sorry`s éliminés à la création. +-/ + +import Mathlib.CategoryTheory.Sites.IsSheafFor +import Mathlib.CategoryTheory.Sites.SheafOfTypes +import Mathlib.CategoryTheory.Whiskering +import Grothendieck.Flasque + +namespace Grothendieck + +open CategoryTheory CategoryTheory.Limits Opposite + +universe u v + +section Retracte + +variable {C : Type u} [Category.{v} C] + +/-- **La flasquité descend aux rétractes** : si `Q` est un rétracte de `P` +(`e : P ⟶ Q`, `s : Q ⟶ P`, `s ≫ e = 𝟙 Q`) et `P` est flasque, `Q` est +flasque. La famille `Q` se pousse en famille `P` via la section `s`, la +compatibilité suit la naturalité, et l'amalgamation `t` revient par `e`. +L'invariance par isomorphisme (Godement II.3.1) en est le cas symétrique : +ici une seule composition égale à l'identité suffit. -/ +theorem isFlasqueSieves_of_retract {P Q : Cᵒᵖ ⥤ Type (max v u)} (e : P ⟶ Q) + (s : Q ⟶ P) (h : s ≫ e = 𝟙 Q) [IsFlasqueSieves P] : IsFlasqueSieves Q where + amalgamates := by + intro X S x hx + obtain ⟨t, ht⟩ := IsFlasqueSieves.amalgamates (P := P) S + (fun Y f hf => s.app (op Y) (x f hf)) + (fun Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ h' => by + show P.map g₁.op (s.app (op Y₁) (x f₁ hf₁)) + = P.map g₂.op (s.app (op Y₂) (x f₂ hf₂)) + rw [← NatTrans.naturality_apply (φ := s) g₁.op (x f₁ hf₁), + ← NatTrans.naturality_apply (φ := s) g₂.op (x f₂ hf₂), + hx g₁ g₂ hf₁ hf₂ h']) + refine ⟨e.app (op X) t, ?_⟩ + intro Y f hf + have nat : (Q.map f.op) (e.app (op X) t) + = e.app (op Y) ((P.map f.op) t) := + (NatTrans.naturality_apply (φ := e) f.op t).symm + have hid : ∀ {Y : C} (z : Q.obj (op Y)), + e.app (op Y) (s.app (op Y) z) = z := by + intro Y z + have hz := congrFun (congrArg (fun φ => φ.app (op Y)) h) z + simpa using hz + rw [nat, ht f hf, hid] + +/-- **La même lecture, rôles échangés** : si `e ≫ s = 𝟙 P` (c'est alors +`P` qui est rétracte de `Q`) et `Q` est flasque, `P` est flasque. Les deux +sens d'une split pair sont couverts par un seul théorème ; cet alias +nommé sert la consommation aval. -/ +theorem isFlasqueSieves_of_retract' {P Q : Cᵒᵖ ⥤ Type (max v u)} (e : P ⟶ Q) + (s : Q ⟶ P) (h : e ≫ s = 𝟙 P) [IsFlasqueSieves Q] : IsFlasqueSieves P := + isFlasqueSieves_of_retract s e h + +end Retracte + +section Corollaires + +variable {C : Type u} [Category.{v} C] + +/-- **Invariance par isomorphisme comme corollaire du rétracte** : le +théorème de la Partie 80 se redéduit ici en une ligne, témoignant que le +rétracte unilatéral est bien la généralisation. -/ +theorem isFlasqueSieves_of_iso' {P Q : Cᵒᵖ ⥤ Type (max v u)} (e : P ≅ Q) + [IsFlasqueSieves P] : IsFlasqueSieves Q := + isFlasqueSieves_of_retract e.hom e.inv e.inv_hom_id + +end Corollaires + +section Abelian + +variable {C : Type u} [Category.{v} C] + +/-- **Pont vers le monde abélien** : pour des préfaisceaux de groupes +abéliens, le rétracte se transporte par `forget` (whiskering droit +préserve la composition et l'identité), donc la flasquité lue à travers +`forget` descend aux rétractes de préfaisceaux abéliens — le cadre où +vivent les rétractes utiles en pratique. -/ +theorem isFlasqueSieves_of_retract_addCommGrp + {F G : Cᵒᵖ ⥤ AddCommGrpCat.{max v u}} (e : F ⟶ G) (s : G ⟶ F) + (h : s ≫ e = 𝟙 G) + [IsFlasqueSieves (F ⋙ forget AddCommGrpCat.{max v u})] : + IsFlasqueSieves (G ⋙ forget AddCommGrpCat.{max v u}) := + isFlasqueSieves_of_retract (Functor.whiskerRight e (forget AddCommGrpCat.{max v u})) + (Functor.whiskerRight s (forget AddCommGrpCat.{max v u})) (by rw [← Functor.whiskerRight_comp, h, Functor.whiskerRight_id']) + +end Abelian + +end Grothendieck diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/FlasqueRetract_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/FlasqueRetract_en.lean new file mode 100644 index 0000000000..2fdf7d4eca --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/FlasqueRetract_en.lean @@ -0,0 +1,164 @@ +/- +Copyright (c) 2026 CoursIA. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Grothendieck tribute — Part 81 (EN sibling of Grothendieck/FlasqueRetract.lean): +flasqueness descends to retracts. + +Alexandre Grothendieck (1928-2014). + +Phase 2 extension (#2159, Epic #1646). + +Part 79 defined flasqueness at the level of sites +(Grothendieck.Flasque, IsFlasqueSieves): any compatible family on any +sieve admits an amalgamation. Part 80 (branch +feature/grothendieck-partie-80) studied stability under isomorphisms +and products. This part generalizes the first link: flasqueness descends +along a one-sided retraction. + + - isFlasqueSieves_of_retract: if Q is a retract of P — a pair + e : P ⟶ Q, s : Q ⟶ P with s ≫ e = 𝟙 Q — and P is flasque, + then Q is flasque. Invariance under isomorphism (Godement II.3.1) + is the symmetric case (both compositions equal to the identity); + here a single equality suffices. The proof pushes the family along + the section s, amalgamates in P, and comes back through e: + compatibility follows from the naturality of s, the conclusion + from that of e and the identity e ≫ s = 𝟙. + + - isFlasqueSieves_of_retract': the same reading with the roles + exchanged — if e ≫ s = 𝟙 P and Q is flasque, then P is + flasque. This is the previous theorem renamed (P is then the + retract of Q): both directions of a split pair are covered by a + single statement, recorded separately for downstream consumption. + + - isFlasqueSieves_of_iso': invariance under isomorphism as a + corollary of the retract (e.inv ≫ e.hom = 𝟙). A deliberate + duplicate of the Part 80 theorem (branch under review): here it + witnesses that the retract is indeed the generalization. + + - isFlasqueSieves_of_retract_addCommGrp: the bridge to the abelian + world — for presheaves of abelian groups, the retract transports + through forget (whiskering), so flasqueness read through forget + also descends to retracts of abelian presheaves. This is the setting + where practically useful retracts live (split sheaves, split direct + images). + +The conceptual reading, extending Part 80: what transports without +choice is not just the isomorphism — it is everything that is a +retract. A section s provides the transport back; no datum is chosen, +everything is canonically moved. The boundary established in Part 80 +(the flasque => injective link requires Zorn) is confirmed: a retract +costs no choice, a maximal extension costs one. + +References: + - R. Godement, Topologie algebrique et theorie des faisceaux [God58], + Chap. II §3 (prop. 3.1: invariance under isomorphism, of which the + retract is the one-sided form). + - SGA 4, Expose II (sites and sieves). + - Part 79 (Grothendieck.Flasque): IsFlasqueSieves. + - Part 80 (Grothendieck.FlasqueStability, branch + feature/grothendieck-partie-80): invariance under iso, products, + boundary of acyclicity. + +i18n convention (EPIC #4980 ratified 2026-07-04): this module is the +English canonical twin of Grothendieck/FlasqueRetract.lean — _en +suffix on the namespace (Grothendieck.FlasqueRetract_en), identical +imports, translated docstrings and comments. Theorem statements, Lean +tactics, lemma names and Mathlib references remain in English (Mathlib 4, +standard tactic DSL). Only the /-- ... -/ docstrings and -- ... comments +differ between the two files. Anti-§D byte-identity guaranteed: the +namespace body is preserved bit-for-bit (statements and proofs +byte-identical between FlasqueRetract.lean and FlasqueRetract_en.lean). + +Epic #1646, Phase 2 (#2159). All sorries eliminated at creation. +-/ + +import Mathlib.CategoryTheory.Sites.IsSheafFor +import Mathlib.CategoryTheory.Sites.SheafOfTypes +import Mathlib.CategoryTheory.Whiskering +import Grothendieck.Flasque + +namespace Grothendieck.FlasqueRetract_en + +open CategoryTheory CategoryTheory.Limits Opposite + +universe u v + +section Retracte + +variable {C : Type u} [Category.{v} C] + +/-- Flasqueness descends to retracts: if Q is a retract of P +(e : P ⟶ Q, s : Q ⟶ P, s ≫ e = 𝟙 Q) and P is flasque, Q is +flasque. The Q-family pushes to a P-family via the section s, +compatibility follows from naturality, and the amalgamation t comes +back through e. Invariance under isomorphism (Godement II.3.1) is the +symmetric case: here a single composition equal to the identity +suffices. -/ +theorem isFlasqueSieves_of_retract {P Q : Cᵒᵖ ⥤ Type (max v u)} (e : P ⟶ Q) + (s : Q ⟶ P) (h : s ≫ e = 𝟙 Q) [IsFlasqueSieves P] : IsFlasqueSieves Q where + amalgamates := by + intro X S x hx + obtain ⟨t, ht⟩ := IsFlasqueSieves.amalgamates (P := P) S + (fun Y f hf => s.app (op Y) (x f hf)) + (fun Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ h' => by + show P.map g₁.op (s.app (op Y₁) (x f₁ hf₁)) + = P.map g₂.op (s.app (op Y₂) (x f₂ hf₂)) + rw [← NatTrans.naturality_apply (φ := s) g₁.op (x f₁ hf₁), + ← NatTrans.naturality_apply (φ := s) g₂.op (x f₂ hf₂), + hx g₁ g₂ hf₁ hf₂ h']) + refine ⟨e.app (op X) t, ?_⟩ + intro Y f hf + have nat : (Q.map f.op) (e.app (op X) t) + = e.app (op Y) ((P.map f.op) t) := + (NatTrans.naturality_apply (φ := e) f.op t).symm + have hid : ∀ {Y : C} (z : Q.obj (op Y)), + e.app (op Y) (s.app (op Y) z) = z := by + intro Y z + have hz := congrFun (congrArg (fun φ => φ.app (op Y)) h) z + simpa using hz + rw [nat, ht f hf, hid] + +/-- The same reading, roles exchanged: if e ≫ s = 𝟙 P (P is then +the retract of Q) and Q is flasque, P is flasque. Both directions +of a split pair are covered by a single theorem; this named alias serves +downstream consumption. -/ +theorem isFlasqueSieves_of_retract' {P Q : Cᵒᵖ ⥤ Type (max v u)} (e : P ⟶ Q) + (s : Q ⟶ P) (h : e ≫ s = 𝟙 P) [IsFlasqueSieves Q] : IsFlasqueSieves P := + isFlasqueSieves_of_retract s e h + +end Retracte + +section Corollaires + +variable {C : Type u} [Category.{v} C] + +/-- Invariance under isomorphism as a corollary of the retract: the +Part 80 theorem is re-derived here in one line, witnessing that the +one-sided retract is indeed the generalization. -/ +theorem isFlasqueSieves_of_iso' {P Q : Cᵒᵖ ⥤ Type (max v u)} (e : P ≅ Q) + [IsFlasqueSieves P] : IsFlasqueSieves Q := + isFlasqueSieves_of_retract e.hom e.inv e.inv_hom_id + +end Corollaires + +section Abelian + +variable {C : Type u} [Category.{v} C] + +/-- Bridge to the abelian world: for presheaves of abelian groups, +the retract transports through forget (right whiskering preserves +composition and identity), so flasqueness read through forget descends +to retracts of abelian presheaves — the setting where practically useful +retracts live. -/ +theorem isFlasqueSieves_of_retract_addCommGrp + {F G : Cᵒᵖ ⥤ AddCommGrpCat.{max v u}} (e : F ⟶ G) (s : G ⟶ F) + (h : s ≫ e = 𝟙 G) + [IsFlasqueSieves (F ⋙ forget AddCommGrpCat.{max v u})] : + IsFlasqueSieves (G ⋙ forget AddCommGrpCat.{max v u}) := + isFlasqueSieves_of_retract (Functor.whiskerRight e (forget AddCommGrpCat.{max v u})) + (Functor.whiskerRight s (forget AddCommGrpCat.{max v u})) (by rw [← Functor.whiskerRight_comp, h, Functor.whiskerRight_id']) + +end Abelian + +end Grothendieck.FlasqueRetract_en diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md index 542d38bc9f..84acee8b39 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md @@ -186,6 +186,7 @@ La formalisation couvre **78 modules leaf** + **1 umbrella** `Grothendieck.lean` | 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 | +| 81 | `Grothendieck/FlasqueRetract.lean` | `FlasqueRetract_en.lean` | **Flasqueness descends to retracts** — `isFlasqueSieves_of_retract`: if `Q` is a retract of `P` (`e : P ⟶ Q`, `s : Q ⟶ P`, `s ≫ e = 𝟙 Q`) and `P` flasque, then `Q` flasque — **one-sided** generalization of invariance under isomorphism (God58 II.3.1, symmetric case): the family pushes along the section, amalgamates in `P`, comes back through `e`; naturalities + `e ≫ s = 𝟙`, no choice. Alias `isFlasqueSieves_of_retract'` (roles exchanged: `e ≫ s = 𝟙 P`, both directions of a split pair), corollary `isFlasqueSieves_of_iso'` (the iso re-derived from the retract in one line), abelian bridge `isFlasqueSieves_of_retract_addCommGrp` (right whiskering by `forget`: stability passes to abelian-group presheaves, the setting of useful retracts). Mathlib records nothing of the kind, not even topologically. Extends the no-choice boundary of Part 80: any retract transports canonically, only the Zorn link `flasque ⇒ injective` (God58 II.5.2) costs a choice. God58 II.3.1, SGA 4 II, crossings P79/P80. | 164 | | 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é | — | diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md index ebcb92f3fb..c6338e6066 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md @@ -190,6 +190,7 @@ La formalisation couvre **78 modules leaf** + **1 umbrella** `Grothendieck.lean` | 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 | +| 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 | | 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é | — | From 0288b2e822f67559c3fd333457a1f481e42bf925 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sun, 20 Sep 2026 20:20:22 +0200 Subject: [PATCH 2/2] Fix: comptes README Grothendieck 78/79 -> 80 leaf + 81 sources FR (P80+P81 fusionnes) Apres merge origin/main (P80 FlasqueStability, #16980 merge e66e2c3f2) : arbre = 80 leaf FR + 80 siblings _en + 1 umbrella. 12 patches a ancre exacte (6 par README), numeros de Partie intacts. Verifie : table 80/80 des deux cotes, 0 manquant, 0 orphelin. Co-Authored-By: Claude Sonnet 5 --- .../SymbolicAI/Lean/grothendieck_lean/README.en.md | 12 ++++++------ .../SymbolicAI/Lean/grothendieck_lean/README.md | 12 ++++++------ 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md index ccb79e1062..e6a6048352 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md @@ -34,7 +34,7 @@ Three paths are offered depending on your goal: ## The arc -Les **78 modules leaf** (0 `sorry`, 0 axiome ajouté) tracent un chemin cohérent, +Les **80 modules leaf** (0 `sorry`, 0 axiome ajouté) tracent un chemin cohérent, du site brut jusqu'à la cohomologie : ```mermaid @@ -103,7 +103,7 @@ laws and the lattice of topologies. A third vein opens with `Classifier.lean` (P ## Code structure -La formalisation couvre **78 modules leaf** + **1 umbrella** `Grothendieck.lean` +La formalisation couvre **80 modules leaf** + **1 umbrella** `Grothendieck.lean` (imports-only, bilingue inline FR/EN). Les trois sous-modules de `SheafCohomology/` sont les Parties 20, 22 et 23 du tableau. @@ -197,12 +197,12 @@ roughly as much again.* ## Build & status - **Toolchain**: `leanprover/lean4:v4.33.0` (cf. `lean-toolchain` of the lake; migration v4.32.1 → v4.33.0 happened post-#11294, attested by `git log -- lean-toolchain`) -- **Build** : `lake build` (WSL requis). La cible par défaut (`globs := #[`Grothendieck.*]` dans `lakefile.lean`) compile **tous** les modules FR et `_en` (79 sources de modules FR : 1 umbrella + 78 leaf, auxquelles s'ajoutent 78 modules `_en`, soit 157 sources de modules ; le lake contient 158 fichiers `.lean` en comptant aussi `lakefile.lean`, vérifié par `git ls-tree -r HEAD`). Dernier build vérifié sur la branche de cette PR : `lake build Grothendieck` SUCCESS local (preuve jointe dans le body de PR, §Validation). Le compte disque **78 leaf FR + 78 leaf `_en` + 1 umbrella** est contrôlé par `scripts/lean/check_grothendieck_readme.py` (sortie JSON, code non nul en cas de dérive). +- **Build** : `lake build` (WSL requis). La cible par défaut (`globs := #[`Grothendieck.*]` dans `lakefile.lean`) compile **tous** les modules FR et `_en` (81 sources de modules FR : 1 umbrella + 80 leaf, auxquelles s'ajoutent 78 modules `_en`, soit 157 sources de modules ; le lake contient 158 fichiers `.lean` en comptant aussi `lakefile.lean`, vérifié par `git ls-tree -r HEAD`). Dernier build vérifié sur la branche de cette PR : `lake build Grothendieck` SUCCESS local (preuve jointe dans le body de PR, §Validation). Le compte disque **78 leaf FR + 78 leaf `_en` + 1 umbrella** est contrôlé par `scripts/lean/check_grothendieck_readme.py` (sortie JSON, code non nul en cas de dérive). - **Proofs**: **0 `sorry`, 0 axiom added** — every module is complete at creation. (A naive `grep sorry` matches prose mentions in the bilingual docstrings, notably two in `ExceptionalDirect.lean`; CI counts in `real` mode — after comment stripping — and reads 0.) - **Dependencies**: Mathlib 4 (via `lakefile.lean`) -- **i18n** (EPIC #4980, convention Option A ratifiée le 2026-07-04) : couverture bilingue complète — **79 fichiers FR** (1 umbrella `Grothendieck.lean` + 78 leaf canoniques, mesurés par `git ls-tree -r HEAD`) et **78 siblings `_en.lean`**, ratio 1:1 intégral (vérifié par `scripts/lean/check_i18n_siblings.py`). Le gap historique `PullbackFunctor.lean` sans `_en` est fermé depuis c.2026-08-18 : `PullbackFunctor_en.lean` est sur disque, et les **78** modules FR ont leur sibling `_en`. Les namespaces `_en` évitent les collisions et le contenu hors docstrings reste byte-identique, vérifiable par CI. L'umbrella est bilingue inline *by design* (FR canonique d'abord, EN en miroir dans le même fichier). **[`README.md`](./README.md)** est le sibling FR canonique. Hors scope : `.lake/packages/`, bibliothèques vendored. +- **i18n** (EPIC #4980, convention Option A ratifiée le 2026-07-04) : couverture bilingue complète — **81 fichiers FR** (1 umbrella `Grothendieck.lean` + 80 leaf canoniques, mesurés par `git ls-tree -r HEAD`) et **78 siblings `_en.lean`**, ratio 1:1 intégral (vérifié par `scripts/lean/check_i18n_siblings.py`). Le gap historique `PullbackFunctor.lean` sans `_en` est fermé depuis c.2026-08-18 : `PullbackFunctor_en.lean` est sur disque, et les **78** modules FR ont leur sibling `_en`. Les namespaces `_en` évitent les collisions et le contenu hors docstrings reste byte-identique, vérifiable par CI. L'umbrella est bilingue inline *by design* (FR canonique d'abord, EN en miroir dans le même fichier). **[`README.md`](./README.md)** est le sibling FR canonique. Hors scope : `.lake/packages/`, bibliothèques vendored. -*Note de cohérence* : couverture 1:1 intégrale — 78 leaf FR canoniques et 78 siblings `_en` (le gap historique `PullbackFunctor` sans `_en`, nommé dans d'anciennes révisions, est fermé sur disque). Le `globs` du lakefile auto-découvre chaque module présent, FR comme `_en`. Vérification reproductible : `python scripts/lean/check_grothendieck_readme.py` — code non nul à la moindre dérive entre la prose et le disque. +*Note de cohérence* : couverture 1:1 intégrale — 80 leaf FR canoniques et 80 siblings `_en` (le gap historique `PullbackFunctor` sans `_en`, nommé dans d'anciennes révisions, est fermé sur disque). Le `globs` du lakefile auto-découvre chaque module présent, FR comme `_en`. Vérification reproductible : `python scripts/lean/check_grothendieck_readme.py` — code non nul à la moindre dérive entre la prose et le disque. ## References @@ -219,7 +219,7 @@ The language toured here — Grothendieck topologies, sites, sheaves, and scheme ## See also - Epic #1646 (hommage à Grothendieck) — Issue #2159 (profondeur de formalisation : Phase 1 livrée, Phase 2 = #10357, Phase 5 = Parties 35-44, puis Parties 64-77) -- EPIC #4980 — convention i18n Lean (Option A sibling pair ; 78 paires `_en` dans ce lake, ratio 1:1) +- EPIC #4980 — convention i18n Lean (Option A sibling pair ; 80 paires `_en` dans ce lake, ratio 1:1) - Epic #1453 (prover harness calibration) — Issue #8960 (reconciling the two `Part` numberings) - ~~#11286~~ — **CLOSED** 2026-08-16 (PR #11294 MERGED): umbrella import of `ExceptionalDirect` realized; the #10357 orphan lived 6 weeks before this merge - Conway tribute workspace (`../conway_lean/`) — Lean notebook series (`../README.md`) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md index fbed69910c..0dd052346c 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md @@ -35,7 +35,7 @@ Trois parcours sont proposés selon ton but : ## La trajectoire -Les **78 modules leaf** (0 `sorry`, 0 axiome ajouté) tracent un chemin cohérent, +Les **80 modules leaf** (0 `sorry`, 0 axiome ajouté) tracent un chemin cohérent, du site brut jusqu'à la cohomologie : ```mermaid @@ -107,7 +107,7 @@ treillis des topologies. Une troisième veine s'ouvre avec `Classifier.lean` (Pa ## Structure du code -La formalisation couvre **78 modules leaf** + **1 umbrella** `Grothendieck.lean` +La formalisation couvre **80 modules leaf** + **1 umbrella** `Grothendieck.lean` (imports-only, bilingue inline FR/EN). Les trois sous-modules de `SheafCohomology/` sont les Parties 20, 22 et 23 du tableau. @@ -201,13 +201,13 @@ 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.*]` du `lakefile.lean`) compile **tous** les modules FR et `_en` (79 sources de modules FR : 1 umbrella + 78 leaf, auxquelles s'ajoutent 78 modules `_en`, soit 157 sources de modules ; le lake contient 158 fichiers `.lean` en comptant aussi `lakefile.lean`, vérifié par `git ls-tree -r HEAD`). Dernier build vérifié sur la branche de cette PR : `lake build Grothendieck` SUCCESS local (cf. §Validation du body PR — preuve jointe). Le compte disque **78 leaf FR + 78 leaf `_en` + 1 umbrella** est mesuré par le checker anti-récidive `scripts/lean/check_grothendieck_readme.py` (sortie JSON, exit code non-zéro sur dérive). +- **Build** : `lake build` (WSL requis). La cible défaut (`globs := #[`Grothendieck.*]` du `lakefile.lean`) compile **tous** les modules FR et `_en` (81 sources de modules FR : 1 umbrella + 80 leaf, auxquelles s'ajoutent 78 modules `_en`, soit 157 sources de modules ; le lake contient 158 fichiers `.lean` en comptant aussi `lakefile.lean`, vérifié par `git ls-tree -r HEAD`). Dernier build vérifié sur la branche de cette PR : `lake build Grothendieck` SUCCESS local (cf. §Validation du body PR — preuve jointe). Le compte disque **78 leaf FR + 78 leaf `_en` + 1 umbrella** est mesuré par le checker anti-récidive `scripts/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 — **79 fichiers FR** (1 umbrella `Grothendieck.lean` + 78 leaf canoniques mesurés par `git ls-tree -r HEAD`) et **78 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 78 modules FR ont leur sibling `_en`. Namespaces `_en` anti-collision, contenu non-docstring byte-identique, vérifiable par CI. L'umbrella est bilingue inline *by design* (FR canonique d'abord, EN en miroir dans le même fichier). **[`README.en.md`](./README.en.md)** est le miroir EN du présent fichier. Hors-scope : `.lake/packages/`, libs vendored. +- **i18n** (EPIC #4980, convention Option A ratifiée 2026-07-04) : couverture bilingue complète — **81 fichiers FR** (1 umbrella `Grothendieck.lean` + 80 leaf canoniques mesurés par `git ls-tree -r HEAD`) et **78 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 78 modules FR ont leur sibling `_en`. Namespaces `_en` anti-collision, contenu non-docstring byte-identique, vérifiable par CI. L'umbrella est bilingue inline *by design* (FR canonique d'abord, EN en miroir dans le même fichier). **[`README.en.md`](./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 — 78 leaf FR canoniques et 78 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. +*Note de cohérence* : couverture 1:1 intégrale — 80 leaf FR canoniques et 80 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 @@ -227,7 +227,7 @@ formalisation d'EGA/SGA. ## 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 ; 78 paires `_en` dans ce lake, ratio 1:1) +- EPIC #4980 — convention i18n Lean (Option A sibling pair ; 80 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`)