diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean index 0ada5ded7e..8643db6680 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean @@ -44,6 +44,7 @@ import Grothendieck.FlasqueRetract import Grothendieck.FlasqueExact import Grothendieck.FlasqueQuotient import Grothendieck.Fppf +import Grothendieck.Godement import Grothendieck.KanExtensions import Grothendieck.LawvereTierney import Grothendieck.LeftExact diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Godement.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Godement.lean new file mode 100644 index 0000000000..9c7bee76cc --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Godement.lean @@ -0,0 +1,218 @@ +/- +Copyright (c) 2026 CoursIA. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +import Mathlib.CategoryTheory.Sites.IsSheafFor +import Mathlib.Topology.Sheaves.Flasque +import Mathlib.Topology.Sheaves.SheafCondition.Sites +import Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing +import Mathlib.Topology.Sheaves.Stalks + +/-! +# Le faisceau de Godement : sections discontinues + +Suite du fil God58 après la clôture de la veine flasque (P79-P83) : la +construction de Godement [God58, Chap. II §4.1], l'application directe des +tiges (P73) et des critères de flasquité. Pour un préfaisceau `F` de groupes +abéliens sur `X`, la section de Godement sur `U` est la famille de germes +`C⁰(U) = ∏_{x ∈ U} Fₓ` — toute fonction choisissant un germe à chaque point, +sans aucune condition de continuité. D'où le nom : sections discontinues. + +Trois faits, dans l'ordre du récit : + +1. `isFlasque_godementPresheaf` : `C⁰F` est **flasque** — une section sur `U` + s'étend à tout `V ⊇ U` en prolongeant par zéro hors de `U` (les germes + vivent dans des groupes abéliens, le zéro est toujours disponible). C'est + l'extension la plus brutale qui soit : aucune donnée à préserver. +2. `isSheaf_godementPresheaf` : `C⁰F` est un **faisceau** — une famille + compatible sur un recouvrement se recolle point par point : deux valeurs + coïncident sur les intersections parce que la compatibilité, pour des + sections qui SONT des fonctions, est une égalité pointwise. +3. `injective_toGodement_of_isSheaf` : l'unité `F → C⁰F` (prendre le germe de + chaque point) est **injective quand `F` est un faisceau** — deux sections + aux germes égaux partout coïncident sur un voisinage de chaque point + (`Presheaf.germ_eq`), et le recollement unique les identifie. C'est la + localité, l'autre moitié de la condition de faisceau. + +La construction est absente de Mathlib (vérifié v4.33.0) ; elle ouvre la voie +à la résolution canonique de Godement (itérer `C⁰` sur les noyaux), fil +prochain du lac. + +## Références + + - R. Godement, *Topologie algébrique et théorie des faisceaux* [God58], + Chap. II §4.1. Le faisceau `C⁰(F)` des sections discontinues. +-/ + +universe u + +open CategoryTheory Category Limits TopCat TopologicalSpace Opposite + +namespace Grothendieck + +variable {X : TopCat.{u}} (F : X.Presheaf AddCommGrpCat.{u}) + +/-- Une section de Godement sur `U` : un germe en chaque point de `U`. +Le `AddCommGroup` est ponctuel (produit de groupes). -/ +noncomputable def godementSection (U : Opens X) : Type u := + ∀ x : U, ↥(F.stalk (x : X)) + +noncomputable instance (U : Opens X) : AddCommGroup (godementSection F U) := + Pi.addCommGroup + +/-- Le faisceau de Godement, objet par objet : `AddCommGrp.of` du produit. -/ +noncomputable def godementObj (U : Opens X) : AddCommGrpCat.{u} := + AddCommGrpCat.of (godementSection F U) + +/-- Restriction d'une section de Godement le long de `i : V ⟶ U` : +précomposition — la fonction se restreint. -/ +noncomputable def godementMap {V U : Opens X} (i : V ⟶ U) : + godementObj F U ⟶ godementObj F V := + AddCommGrpCat.ofHom + { toFun := fun f x => f ⟨x.1, leOfHom i x.2⟩ + map_zero' := rfl + map_add' := fun _ _ => rfl } + +/-- Le préfaisceau de Godement `C⁰F : U ↦ ∏_{x ∈ U} Fₓ`. -/ +noncomputable def godementPresheaf : X.Presheaf AddCommGrpCat where + obj U := godementObj F U.unop + map f := godementMap F f.unop + map_id U := by + ext f + funext x + rfl + map_comp f g := by + ext s + funext x + rfl + +/-- La restriction d'une section de Godement est l'évaluation sur le point +transporté : compte tenu de la définition de `godementMap`, c'est une +réduction définitionnelle. C'est la clé de calcul de tout le module. -/ +theorem godementPresheaf_map_apply {V U : Opens X} (i : V ⟶ U) + (s : godementSection F U) (x : V) : + (godementPresheaf F).map i.op s x = s ⟨(x : X), leOfHom i x.2⟩ := + rfl + +open scoped Classical in +/-- Extension par zéro : une section de Godement sur `U` se prolonge à +tout `V ⊇ U` en choisissant le germe nul hors de `U`. C'est l'ingrédient +de flasquité — le zéro des tiges rend le prolongement toujours possible. -/ +noncomputable def godementExtend {U V : Opens X} + (s : godementSection F U) : godementSection F V := + fun x => if h : (x : X) ∈ U then s ⟨x, h⟩ else 0 + +/-- **Le faisceau de Godement est flasque** : toute section sur `U` se +prolonge à tout `V ⊇ U` (par zéro hors de `U`) — la restriction est +surjective, donc épimorphe. Aucune hypothèse sur `F` : la flasquité de +`C⁰F` est gratuite, c'est tout l'intérêt de la construction. +[God58] Chap. II §4.1. -/ +theorem isFlasque_godementPresheaf : godementPresheaf F |>.IsFlasque where + epi i := by + refine (AddCommGrpCat.epi_iff_surjective _).mpr fun s => ⟨?_, ?_⟩ + · exact godementExtend F s + · funext x + exact dif_pos x.2 + +/-- L'unité de Godement : une section devient la famille de ses germes. +Naturelle par `Presheaf.germ_res` — prendre le germe commute aux +restrictions. -/ +noncomputable def toGodement : F ⟶ godementPresheaf F where + app U := + AddCommGrpCat.ofHom + { toFun := fun s x => F.germ U.unop (x : X) x.2 s + map_zero' := by funext x; rw [map_zero]; rfl + map_add' := fun a b => by funext x; rw [map_add]; rfl } + naturality U V f := by + ext s + funext x + exact F.germ_res_apply' f (x : X) x.2 s + +/-- **Le faisceau de Godement est un faisceau** : toute famille compatible +de sections sur une famille d'ouverts `U i` se recolle en une unique section +sur `⋃ U i`. Le recollement est littéralement pointwise : chaque point `z` de +la réunion vit dans un certain `U i` (choisi par `Classical.choice`), et la +compatibilité — pour des sections qui SONT des fonctions — garantit que le +choix de l'indice n'affecte pas la valeur en `z`. L'unicité est de même +entièrement ponctuelle : deux recollements coïncident sur chaque `U i`, +donc en chaque point de la réunion. La preuve passe par la caractérisation +`isSheaf_iff_isSheafUniqueGluing` de la condition de faisceau, disponible +pour `AddCommGrpCat` (catégorie concrète complète). -/ +theorem isSheaf_godementPresheaf : TopCat.Presheaf.IsSheaf (godementPresheaf F) := by + rw [TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing] + intro ι U sf hcomp + have hcover : ∀ z : ((iSup U : Opens X)), ∃ i, (z : X) ∈ U i := + fun z => Opens.mem_iSup.mp z.2 + choose f hf using hcover + have hglue : TopCat.Presheaf.IsGluing (godementPresheaf F) U sf + (fun z => sf (f z) ⟨(z : X), hf z⟩) := by + intro i + funext x + have hW := congrFun (hcomp i (f ⟨(x : X), leOfHom (Opens.leSupr U i) x.2⟩)) + ⟨(x : X), ⟨x.2, hf ⟨(x : X), leOfHom (Opens.leSupr U i) x.2⟩⟩⟩ + exact hW.symm + refine ⟨_, hglue, fun s hs => ?_⟩ + funext z + exact congrFun (hs (f z)) ⟨(z : X), hf z⟩ + +/-- **L'unité de Godement est injective sur les faisceaux** : si `F` est un +faisceau, deux sections dont les germes coïncident en chaque point de `U` +sont égales. La preuve est la localité : `Presheaf.germ_eq` (P73) fournit +pour chaque point un voisinage `W z ⊆ U` où les restrictions coïncident ; +les `W z` recouvrent `U` (donc `⨆ W = U`), et `s` comme `t` recollent la +même famille — l'unicité du recollement (`isSheaf_iff_isSheafUniqueGluing`) +les identifie. Toutes les égalités de morphismes d'ouverts passent par +`Subsingleton` : deux inclusions `V ⟶ U` sont égales. +C'est la réciproque attendue : le faisceau de Godement contient `F` +entièrement dès que `F` est un faisceau. [God58] Chap. II §4.1. -/ +theorem injective_toGodement_of_isSheaf (hF : TopCat.Presheaf.IsSheaf F) + (U : Opens X) : Function.Injective ((toGodement F).app (op U)) := by + intro s t hst + have hgerm : ∀ z : U, F.germ U (z : X) z.2 s = F.germ U (z : X) z.2 t := + fun z => congrFun hst ⟨(z : X), z.2⟩ + have hloc : ∀ z : U, ∃ W : Opens X, (z : X) ∈ W ∧ ∃ iWU : W ⟶ U, + F.map iWU.op s = F.map iWU.op t := by + intro z + obtain ⟨W, hxW, iU', iV', heq⟩ := F.germ_eq (z : X) z.2 z.2 s t (hgerm z) + refine ⟨W, hxW, iU', ?_⟩ + rw [Subsingleton.elim iV' iU'] at heq + exact heq + choose W hW iWU hagree using hloc + rw [TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing] at hF + have hcompf : TopCat.Presheaf.IsCompatible F W (fun z => F.map (iWU z).op s) := by + intro i j + rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, + ← Functor.map_comp, ← Functor.map_comp, ← op_comp, ← op_comp, + Subsingleton.elim (Opens.infLELeft (W i) (W j) ≫ iWU i) + (Opens.infLERight (W i) (W j) ≫ iWU j)] + obtain ⟨t₀, _, huniq⟩ := hF W (fun z => F.map (iWU z).op s) hcompf + have hsupU : (iSup W : Opens X) = U := by + refine le_antisymm (iSup_le fun z => leOfHom (iWU z)) ?_ + intro x hxU + exact Opens.mem_iSup.mpr ⟨⟨x, hxU⟩, hW ⟨x, hxU⟩⟩ + have hsG : TopCat.Presheaf.IsGluing F W (fun z => F.map (iWU z).op s) + (F.map (homOfLE (le_of_eq hsupU)).op s) := by + intro z + rw [← ConcreteCategory.comp_apply, ← Functor.map_comp, ← op_comp, + Subsingleton.elim (Opens.leSupr W z ≫ homOfLE (le_of_eq hsupU)) (iWU z)] + have htG : TopCat.Presheaf.IsGluing F W (fun z => F.map (iWU z).op s) + (F.map (homOfLE (le_of_eq hsupU)).op t) := by + intro z + rw [← ConcreteCategory.comp_apply, ← Functor.map_comp, ← op_comp, + Subsingleton.elim (Opens.leSupr W z ≫ homOfLE (le_of_eq hsupU)) (iWU z)] + exact (hagree z).symm + have hd : F.map (homOfLE (le_of_eq hsupU)).op s + = F.map (homOfLE (le_of_eq hsupU)).op t := + (huniq _ hsG).trans (huniq _ htG).symm + have key : ∀ u : ToType (F.obj (op U)), + F.map (homOfLE (le_of_eq hsupU.symm)).op + (F.map (homOfLE (le_of_eq hsupU)).op u) = u := by + intro u + rw [← ConcreteCategory.comp_apply, ← Functor.map_comp, ← op_comp, + Subsingleton.elim (homOfLE (le_of_eq hsupU.symm) + ≫ homOfLE (le_of_eq hsupU)) (𝟙 U)] + rw [show (𝟙 U).op = 𝟙 (op U) from rfl, F.map_id] + rfl + exact (key s).symm.trans ((congrArg _ hd).trans (key t)) + +end Grothendieck diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Godement_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Godement_en.lean new file mode 100644 index 0000000000..065f98c767 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/Godement_en.lean @@ -0,0 +1,225 @@ +/- +Copyright (c) 2026 CoursIA. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +import Mathlib.CategoryTheory.Sites.IsSheafFor +import Mathlib.Topology.Sheaves.Flasque +import Mathlib.Topology.Sheaves.SheafCondition.Sites +import Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing +import Mathlib.Topology.Sheaves.Stalks + +/-! +# The Godement sheaf: discontinuous sections + +English canonical sibling of `Grothendieck/Godement.lean` (Partie 84). + +Continuation of the God58 thread after the flasque vein closed (P79-P83): +Godement's construction [God58, Chap. II §4.1], with direct use of stalks +(P73) and of the flasqueness criteria. For a presheaf `F` of abelian groups +on `X`, the Godement section over `U` is the family of germs +`C⁰(U) = ∏_{x ∈ U} Fₓ` — any function choosing a germ at each point, with +no continuity condition whatsoever. Hence the name: discontinuous sections. + +Three facts, in the narrative order: + +1. `isFlasque_godementPresheaf`: `C⁰F` is **flasque** — a section over `U` + extends to any `V ⊇ U` by zero outside `U` (germs live in abelian + groups, zero is always available). This is the most brutal extension + possible: no data to preserve. +2. `isSheaf_godementPresheaf`: `C⁰F` is a **sheaf** — a compatible family + over a cover glues point by point: two values agree on intersections + because compatibility, for sections that ARE functions, is a pointwise + equality. +3. `injective_toGodement_of_isSheaf`: the unit `F → C⁰F` (take the germ at + each point) is **injective when `F` is a sheaf** — two sections with + equal germs everywhere agree on a neighbourhood of each point + (`Presheaf.germ_eq`), and unique gluing identifies them. This is + locality, the other half of the sheaf condition. + +The construction is absent from Mathlib (checked v4.33.0); it opens the way +to Godement's canonical resolution (iterating `C⁰` on kernels), the next +thread of this lake. + +i18n convention (EPIC #4980 ratified 2026-07-04): `_en` suffix on the +namespace (`Grothendieck.Godement_en`), mirror imports, translated +docstrings and comments. Theorem statements, Lean tactics, lemma names and +Mathlib references remain in English. Anti-§D byte-identity guaranteed: +the namespace body is preserved bit for bit (statements and proofs +byte-identical between `Godement.lean` and `Godement_en.lean`). + +## References + + - R. Godement, *Topologie algébrique et théorie des faisceaux* [God58], + Chap. II §4.1. The sheaf `C⁰(F)` of discontinuous sections. +-/ + +universe u + +open CategoryTheory Category Limits TopCat TopologicalSpace Opposite + +namespace Grothendieck.Godement_en + +variable {X : TopCat.{u}} (F : X.Presheaf AddCommGrpCat.{u}) + +/-- A Godement section over `U`: a germ at each point of `U`. +The `AddCommGroup` is pointwise (product of groups). -/ +noncomputable def godementSection (U : Opens X) : Type u := + ∀ x : U, ↥(F.stalk (x : X)) + +noncomputable instance (U : Opens X) : AddCommGroup (godementSection F U) := + Pi.addCommGroup + +/-- The Godement sheaf, objectwise: `AddCommGrp.of` the product. -/ +noncomputable def godementObj (U : Opens X) : AddCommGrpCat.{u} := + AddCommGrpCat.of (godementSection F U) + +/-- Restriction of a Godement section along `i : V ⟶ U`: +precomposition — the function restricts. -/ +noncomputable def godementMap {V U : Opens X} (i : V ⟶ U) : + godementObj F U ⟶ godementObj F V := + AddCommGrpCat.ofHom + { toFun := fun f x => f ⟨x.1, leOfHom i x.2⟩ + map_zero' := rfl + map_add' := fun _ _ => rfl } + +/-- The Godement presheaf `C⁰F : U ↦ ∏_{x ∈ U} Fₓ`. -/ +noncomputable def godementPresheaf : X.Presheaf AddCommGrpCat where + obj U := godementObj F U.unop + map f := godementMap F f.unop + map_id U := by + ext f + funext x + rfl + map_comp f g := by + ext s + funext x + rfl + +/-- Restricting a Godement section is evaluation at the transported +point: given the definition of `godementMap`, this is a definitional +reduction. This is the computation key of the whole module. -/ +theorem godementPresheaf_map_apply {V U : Opens X} (i : V ⟶ U) + (s : godementSection F U) (x : V) : + (godementPresheaf F).map i.op s x = s ⟨(x : X), leOfHom i x.2⟩ := + rfl + +open scoped Classical in +/-- Zero extension: a Godement section over `U` extends to any `V ⊇ U` +by choosing the zero germ outside `U`. This is the flasqueness ingredient +— the zero of stalks makes the extension always possible. -/ +noncomputable def godementExtend {U V : Opens X} + (s : godementSection F U) : godementSection F V := + fun x => if h : (x : X) ∈ U then s ⟨x, h⟩ else 0 + +/-- **The Godement sheaf is flasque**: every section over `U` extends to +any `V ⊇ U` (by zero outside `U`) — the restriction is surjective, hence +epimorphic. No hypothesis on `F`: the flasqueness of `C⁰F` is free, which +is the whole point of the construction. [God58] Chap. II §4.1. -/ +theorem isFlasque_godementPresheaf : godementPresheaf F |>.IsFlasque where + epi i := by + refine (AddCommGrpCat.epi_iff_surjective _).mpr fun s => ⟨?_, ?_⟩ + · exact godementExtend F s + · funext x + exact dif_pos x.2 + +/-- The Godement unit: a section becomes the family of its germs. +Natural by `Presheaf.germ_res` — taking germs commutes with +restrictions. -/ +noncomputable def toGodement : F ⟶ godementPresheaf F where + app U := + AddCommGrpCat.ofHom + { toFun := fun s x => F.germ U.unop (x : X) x.2 s + map_zero' := by funext x; rw [map_zero]; rfl + map_add' := fun a b => by funext x; rw [map_add]; rfl } + naturality U V f := by + ext s + funext x + exact F.germ_res_apply' f (x : X) x.2 s + +/-- **The Godement sheaf is a sheaf**: every compatible family of sections +over a family of opens `U i` glues to a unique section over `⋃ U i`. The +gluing is literally pointwise: each point `z` of the union lives in some +`U i` (chosen by `Classical.choice`), and compatibility — for sections +that ARE functions — guarantees that the choice of index does not affect +the value at `z`. Uniqueness is likewise entirely punctual: two gluings +agree on each `U i`, hence at every point of the union. The proof goes +through the `isSheaf_iff_isSheafUniqueGluing` characterisation of the +sheaf condition, available for `AddCommGrpCat` (concrete complete +category). -/ +theorem isSheaf_godementPresheaf : TopCat.Presheaf.IsSheaf (godementPresheaf F) := by + rw [TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing] + intro ι U sf hcomp + have hcover : ∀ z : ((iSup U : Opens X)), ∃ i, (z : X) ∈ U i := + fun z => Opens.mem_iSup.mp z.2 + choose f hf using hcover + have hglue : TopCat.Presheaf.IsGluing (godementPresheaf F) U sf + (fun z => sf (f z) ⟨(z : X), hf z⟩) := by + intro i + funext x + have hW := congrFun (hcomp i (f ⟨(x : X), leOfHom (Opens.leSupr U i) x.2⟩)) + ⟨(x : X), ⟨x.2, hf ⟨(x : X), leOfHom (Opens.leSupr U i) x.2⟩⟩⟩ + exact hW.symm + refine ⟨_, hglue, fun s hs => ?_⟩ + funext z + exact congrFun (hs (f z)) ⟨(z : X), hf z⟩ + +/-- **The Godement unit is injective on sheaves**: if `F` is a sheaf, two +sections whose germs coincide at every point of `U` are equal. The proof +is locality: `Presheaf.germ_eq` (P73) provides, for each point, a +neighbourhood `W z ⊆ U` where the restrictions coincide; the `W z` cover +`U` (so `⨆ W = U`), and both `s` and `t` glue the same family — unique +gluing (`isSheaf_iff_isSheafUniqueGluing`) identifies them. All equalities +of morphisms of opens go through `Subsingleton`: two inclusions +`V ⟶ U` are equal. This is the expected converse: the Godement sheaf +contains `F` entirely as soon as `F` is a sheaf. [God58] Chap. II §4.1. -/ +theorem injective_toGodement_of_isSheaf (hF : TopCat.Presheaf.IsSheaf F) + (U : Opens X) : Function.Injective ((toGodement F).app (op U)) := by + intro s t hst + have hgerm : ∀ z : U, F.germ U (z : X) z.2 s = F.germ U (z : X) z.2 t := + fun z => congrFun hst ⟨(z : X), z.2⟩ + have hloc : ∀ z : U, ∃ W : Opens X, (z : X) ∈ W ∧ ∃ iWU : W ⟶ U, + F.map iWU.op s = F.map iWU.op t := by + intro z + obtain ⟨W, hxW, iU', iV', heq⟩ := F.germ_eq (z : X) z.2 z.2 s t (hgerm z) + refine ⟨W, hxW, iU', ?_⟩ + rw [Subsingleton.elim iV' iU'] at heq + exact heq + choose W hW iWU hagree using hloc + rw [TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing] at hF + have hcompf : TopCat.Presheaf.IsCompatible F W (fun z => F.map (iWU z).op s) := by + intro i j + rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, + ← Functor.map_comp, ← Functor.map_comp, ← op_comp, ← op_comp, + Subsingleton.elim (Opens.infLELeft (W i) (W j) ≫ iWU i) + (Opens.infLERight (W i) (W j) ≫ iWU j)] + obtain ⟨t₀, _, huniq⟩ := hF W (fun z => F.map (iWU z).op s) hcompf + have hsupU : (iSup W : Opens X) = U := by + refine le_antisymm (iSup_le fun z => leOfHom (iWU z)) ?_ + intro x hxU + exact Opens.mem_iSup.mpr ⟨⟨x, hxU⟩, hW ⟨x, hxU⟩⟩ + have hsG : TopCat.Presheaf.IsGluing F W (fun z => F.map (iWU z).op s) + (F.map (homOfLE (le_of_eq hsupU)).op s) := by + intro z + rw [← ConcreteCategory.comp_apply, ← Functor.map_comp, ← op_comp, + Subsingleton.elim (Opens.leSupr W z ≫ homOfLE (le_of_eq hsupU)) (iWU z)] + have htG : TopCat.Presheaf.IsGluing F W (fun z => F.map (iWU z).op s) + (F.map (homOfLE (le_of_eq hsupU)).op t) := by + intro z + rw [← ConcreteCategory.comp_apply, ← Functor.map_comp, ← op_comp, + Subsingleton.elim (Opens.leSupr W z ≫ homOfLE (le_of_eq hsupU)) (iWU z)] + exact (hagree z).symm + have hd : F.map (homOfLE (le_of_eq hsupU)).op s + = F.map (homOfLE (le_of_eq hsupU)).op t := + (huniq _ hsG).trans (huniq _ htG).symm + have key : ∀ u : ToType (F.obj (op U)), + F.map (homOfLE (le_of_eq hsupU.symm)).op + (F.map (homOfLE (le_of_eq hsupU)).op u) = u := by + intro u + rw [← ConcreteCategory.comp_apply, ← Functor.map_comp, ← op_comp, + Subsingleton.elim (homOfLE (le_of_eq hsupU.symm) + ≫ homOfLE (le_of_eq hsupU)) (𝟙 U)] + rw [show (𝟙 U).op = 𝟙 (op U) from rfl, F.map_id] + rfl + exact (key s).symm.trans ((congrArg _ hd).trans (key t)) + +end Grothendieck.Godement_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 e80f215a9c..b13d59af65 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 **82 modules leaf** (0 `sorry`, 0 axiome ajouté) tracent un chemin cohérent, +Les **83 modules leaf** (0 `sorry`, 0 axiome ajouté) tracent un chemin cohérent, du site brut jusqu'à la cohomologie : ```mermaid @@ -103,13 +103,13 @@ laws and the lattice of topologies. A third vein opens with `Classifier.lean` (P ## Code structure -La formalisation couvre **82 modules leaf** + **1 umbrella** `Grothendieck.lean` +La formalisation couvre **83 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. | Part | File | `_en` | Content | Lines | |------|------|-------|---------|-------| -| racine | `Grothendieck.lean` | (aucun — FR-only) | **Racine umbrella** (imports-only + commentaire d'invariant FR-only) ; importe **chaque** leaf FR (82) et **jamais** un sibling `_en` (invariant #16154 ; les 82 siblings `_en` restent compilés par les `globs` du lakefile) ; `ExceptionalDirect` importé c.2026-08-15, **fermeture #11286** | 290 | +| racine | `Grothendieck.lean` | (aucun — FR-only) | **Racine umbrella** (imports-only + commentaire d'invariant FR-only) ; importe **chaque** leaf FR (83) et **jamais** un sibling `_en` (invariant #16154 ; les 83 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` | Sieves, Grothendieck topologies (trivial/discrete/dense), three axioms | 243 | | 2 | `Grothendieck/SchemesTour.lean` | `SchemesTour_en.lean` | Scheme type, Spec functor, Γ, `homeoOfIso`, fully-faithful | 196 | | 3 | `Grothendieck/ZariskiSite.lean` | `ZariskiSite_en.lean` | Zariski pretopology, `zariskiTopology_eq` bridge theorem, subcanonical | 139 | @@ -190,6 +190,7 @@ La formalisation couvre **82 modules leaf** + **1 umbrella** `Grothendieck.lean` | 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 | | 82 | `Grothendieck/FlasqueExact.lean` | `FlasqueExact_en.lean` | **From the sieve to the epimorphism** — `exists_isAmalgamation_of_sieveTop` (the **maximal** sieve always amalgamates, no hypothesis on `P`: sieve-flasqueness is a condition on proper sieves only), `exists_lift_of_isFlasqueSieves_of_mono` (sieve-flasque ⇒ extension along any **mono**, arbitrary site — the "subobject" reading of section extension), `exists_isAmalgamation_of_isFlasque_generate_singleton` (partial converse: `Presheaf.IsFlasque` ⇒ amalgamation on any sieve **generated by a single arrow**; the residual gap towards `IsFlasqueSieves` = exactly the multi-generator sieves), and `epi_of_shortExact_of_isFlasqueSieves` (**Godement II.3 on the site side**: Mathlib's Zorn proof `epi_of_shortExact` consumes the flasqueness of `X₁` exactly once, at the inclusion `homOfLE inf_le_right` — the local replay substituting this single link by the mono-extension shows that "epi on every arrow" yields to "amalgamation on every sieve": the short exact sequence theorem already lives in the world of sites). Documented frontier: the full converse would require Zorn on multi-arrow families. God58 II.3/II.5, SGA 4 II, MM92 II.3/III.4. | 235 | | 83 | `Grothendieck/FlasqueQuotient.lean` | `FlasqueQuotient_en.lean` | **The bridge closes** — `isFlasque_of_isFlasqueSieves` (**return** bridge: sieve-flasque ⇒ Mathlib-flasque for every arrow of `Opens X` — the site is thin, every arrow there is mono, the mono lift of Part 82 applies to each restriction, no sheaf hypothesis), `isFlasqueSieves_of_isFlasque_of_isSheaf` (**forward** bridge: sheaf + Mathlib-flasque ⇒ sieve-flasque, **without Zorn** — the multi-generator frontier of Part 82 disappears on `Opens X`: the supremum `V₀` of the sieve's members bounds the family in the lattice of opens, the sheaf condition glues the family there (`presieveOfCovering.mem_grothendieckTopology`), flasqueness extends the section from `V₀` to `U`), and `isFlasqueSieves_of_shortExact_of_isFlasque₁₂` (**Godement II.3.1 second half on the sieve side**: `X₁` and `X₂` sieve-flasque ⇒ `X₃` sieve-flasque, mirror of `TopCat.Sheaf.IsFlasque.of_shortExact_of_isFlasque₁₂` — the epi of `S.g` comes from Part 82, the restrictions of `X₂` from the return bridge, the conclusion from the forward bridge). On `Opens X`, the two flasqueness notions coincide for sheaves. God58 II.3.1, SGA 4 II, MM92 II.3. | 206 | +| 84 | `Grothendieck/Godement.lean` | `Godement_en.lean` | **The Godement sheaf C⁰: discontinuous sections** — `godementPresheaf` (`U ↦ ∏_{x ∈ U} Fₓ`, the product of stalks (P73), with no continuity condition whatsoever), `isFlasque_godementPresheaf` (**C⁰F is flasque with no hypothesis on F**: zero extension outside `U`, the zero of stalks makes the extension always possible — consumes Mathlib's `Presheaf.IsFlasque`), `isSheaf_godementPresheaf` (**C⁰F is a sheaf**: pointwise gluing via `isSheaf_iff_isSheafUniqueGluing`, the per-point choice of index is harmless since compatibility, for sections that ARE functions, is a pointwise equality), `injective_toGodement_of_isSheaf` (**the germ unit `F → C⁰F` is injective when `F` is a sheaf**: `germ_eq` provides a neighbourhood at each point, `⨆ W = U`, unique gluing identifies — all morphism equalities of opens go through `Subsingleton`). Construction absent from Mathlib (checked v4.33.0, 0 hit); opens the way to Godement's canonical resolution (iterating `C⁰` on kernels), the next thread. God58 II.4.1, crossings P73/P79-P83. | 218 | | 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é | — | @@ -199,12 +200,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` (83 sources de modules FR : 1 umbrella + 82 leaf, auxquelles s'ajoutent 82 modules `_en`, soit 165 sources de modules ; le lake contient 166 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 **82 leaf FR + 82 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` (84 sources de modules FR : 1 umbrella + 83 leaf, auxquelles s'ajoutent 83 modules `_en`, soit 167 sources de modules ; le lake contient 168 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 **83 leaf FR + 83 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 — **83 fichiers FR** (1 umbrella `Grothendieck.lean` + 82 leaf canoniques, mesurés par `git ls-tree -r HEAD`) et **82 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 **82** 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 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.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 — **84 fichiers FR** (1 umbrella `Grothendieck.lean` + 83 leaf canoniques, mesurés par `git ls-tree -r HEAD`) et **83 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 **83** 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 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.md`](./README.md)** est le sibling FR canonique. Hors scope : `.lake/packages/`, bibliothèques vendored. -*Note de cohérence* : couverture 1:1 intégrale — 82 leaf FR canoniques et 82 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 — 83 leaf FR canoniques et 83 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 @@ -221,7 +222,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 ; 82 paires `_en` dans ce lake, ratio 1:1) +- EPIC #4980 — convention i18n Lean (Option A sibling pair ; 83 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`) @@ -264,7 +265,7 @@ Four real frictions, documented at source: 1. **Self-imposed anti-regression constraint**: every module complete at creation (0 `sorry`, 0 added axiom) — the lake's ceiling is bounded by what Mathlib already exposes, not by a choice of sub-formalisation. This is a **scope** friction: when a concept is missing from Mathlib, it is either reconstructed locally or deferred. 2. **Living Mathlib boundary**: `Classifier.lean:190` — `ElementaryTopos` "not yet available in this revision": the lake's bound moves with Mathlib. -3. **Reconnection debt resolved**: `#11286` — umbrella import of `ExceptionalDirect` **CLOSED 2026-08-16** (PR #11294, cf §See also); the umbrella now imports every FR leaf (82) and never an `_en` (#16154), while the lakefile `globs` also build the 82 `_en` siblings. +3. **Reconnection debt resolved**: `#11286` — umbrella import of `ExceptionalDirect` **CLOSED 2026-08-16** (PR #11294, cf §See also); the umbrella now imports every FR leaf (83) and never an `_en` (#16154), while the lakefile `globs` also build the 83 `_en` siblings. 4. **Historical i18n friction**: a missing `_en` sibling for `PullbackFunctor` (filled since, cf §Build & status) — the bilingual pair is a maintenance constraint, not just a format. ### Point 7 — discovery path (fill) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md index a2c1a30050..83e9c16119 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 **82 modules leaf** (0 `sorry`, 0 axiome ajouté) tracent un chemin cohérent, +Les **83 modules leaf** (0 `sorry`, 0 axiome ajouté) tracent un chemin cohérent, du site brut jusqu'à la cohomologie : ```mermaid @@ -107,13 +107,13 @@ treillis des topologies. Une troisième veine s'ouvre avec `Classifier.lean` (Pa ## Structure du code -La formalisation couvre **82 modules leaf** + **1 umbrella** `Grothendieck.lean` +La formalisation couvre **83 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 (82) et **jamais** un sibling `_en` (invariant #16154 ; les 82 siblings `_en` restent compilés par les `globs` du lakefile) ; `ExceptionalDirect` importé c.2026-08-15, **fermeture #11286** | 290 | +| racine | `Grothendieck.lean` | (aucun — FR-only) | **Racine umbrella** (imports-only + commentaire d'invariant FR-only) ; importe **chaque** leaf FR (83) et **jamais** un sibling `_en` (invariant #16154 ; les 83 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 | @@ -194,6 +194,7 @@ La formalisation couvre **82 modules leaf** + **1 umbrella** `Grothendieck.lean` | 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 | | 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é | — | @@ -203,13 +204,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` (83 sources de modules FR : 1 umbrella + 82 leaf, auxquelles s'ajoutent 82 modules `_en`, soit 165 sources de modules ; le lake contient 166 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 **82 leaf FR + 82 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` (84 sources de modules FR : 1 umbrella + 83 leaf, auxquelles s'ajoutent 83 modules `_en`, soit 167 sources de modules ; le lake contient 168 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 **83 leaf FR + 83 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 — **83 fichiers FR** (1 umbrella `Grothendieck.lean` + 82 leaf canoniques mesurés par `git ls-tree -r HEAD`) et **82 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 82 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`](./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 — **84 fichiers FR** (1 umbrella `Grothendieck.lean` + 83 leaf canoniques mesurés par `git ls-tree -r HEAD`) et **83 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 83 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`](./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 — 82 leaf FR canoniques et 82 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 — 83 leaf FR canoniques et 83 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 @@ -229,7 +230,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 ; 82 paires `_en` dans ce lake, ratio 1:1) +- EPIC #4980 — convention i18n Lean (Option A sibling pair ; 83 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`) @@ -272,7 +273,7 @@ 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 (82) et jamais un `_en` (#16154), tandis que le `globs` du lakefile assure aussi la compilation des 82 siblings `_en`. +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 (83) 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)