Lean-15c : le lake Grothendieck par ses énoncés (companion formel natif)

Navigation : << Lean-15b Grothendieck en Lean | Lean-15d Visite guidee visuelle >> | Index

Ce notebook est le companion formel natif du lake grothendieck_lean/, en kernel lean4-wsl. Il complète le notebook Python Lean-15b : là où 15b charge et explique les sources, celui-ci importe le lake réel et montre, à travers un parcours représentatif de ses modules, des énoncés qui compilent — la visibilité promise par l’épic #11703.

Un lake enrichi n’existe, pour un lecteur, que si un notebook le montre. Chaque #check ci-dessous affiche le type exact d’un lemme de grothendieck_lean, tel que Mathlib 4 le formalise — on ne lit pas un résumé, on lit l’énoncé compilé.

Comment lire ce notebook. Chaque section suit le même rituel : un paragraphe explique ce que disent les théorèmes (éventuellement ce qu’ils coûtent historiquement), puis une cellule #check interroge le lake — la sortie qui s’affiche sous la cellule est la signature élaborée, pas une citation. La lecture peut être séquentielle (les notions s’empilent : adjonctions → monades → cribles → topologies → faisceaux → cohomologie), mais chaque section est aussi autoporteuse via son lien module. Le kernel lean4-wsl exécute un REPL Lean 4 réel appuyé sur le build du lake — même toolchain (lean-toolchain), mêmes .olean que lake build produit localement.

Positionnement dans la série. Lean-15 (Tribute) présentait la personne et le programme ; Lean-15b (Python) démonte le lake fichier par fichier ; ce companion atteste que le tout compile et ne triche pas. Les trois étages sont représentés : le socle catégorique (§2-3), la machinerie des sites (§4-5), l’édifice cohomologique (§6-7), jusqu’aux ancrages géométriques (§8) et aux micro-preuves de calibration qui ferment la boucle (§9).

1. Import du lake

Le lake entier s’importe par son umbrella racine Grothendieck, qui réexporte ses modules et leurs preuves. C’est une ligne — mais elle est lourdement chargée : derrière elle, le REPL charge plusieurs milliers d’oléans (Mathlib inclus via les dépendances du lake), et chaque #check ultérieur résout ses noms dans cet environnement. Si l’import répond {"env": 0} sans message d’erreur, l’environnement est prêt : les sections suivantes n’ont plus qu’à l’interroger. C’est la différence entre lire un lake et l’avoir chargé : à partir d’ici, chaque identifiant résout (ou échoue) contre le vrai lake, pas contre une doc.

import Grothendieck
import Grothendieck.FlasqueQuotient
import Grothendieck.GodementFunctor
import Grothendieck.GodementMono

import Grothendieck

import Grothendieck.FlasqueQuotient

import Grothendieck.GodementFunctor

import Grothendieck.GodementMono

--% env 0

Raw input

{"cmd": "import Grothendieck\nimport Grothendieck.FlasqueQuotient\nimport Grothendieck.GodementFunctor\nimport Grothendieck.GodementMono"}

Raw output

{"env": 0}

2. Fondations categoriques

Le vocabulaire commun sur lequel tout le reste s’assemble — et le premier endroit où le formalisme paie, car chacun de ces énoncés transporte des données que la prose omet.

Ce que disent les théorèmes. leftAdjoint_preserves_colimits : un foncteur adjoint à gauche préserve les colimites (et symétriquement rightAdjoint_preserves_limits pour l’adjoint à droite). C’est le théorème « RAPL » des catégories — l’exemple canonique : les foncteurs oubli libres (free ⊣ forget) préservent les colimites, ce qui donne toutes les présentations d’algèbres par générateurs et relations. adj_toEquivalence enchaîne : une adjonction dont unité et counité sont des isomorphismes est une équivalence de catégories — le critère pratique pour prouver C ≌ D sans exhiber les deux foncteurs réciproques.

Le lemme de Yoneda (yoneda_equiv_apply, yoneda_full) est le résultat fondateur de la théorie : le plongement C → [Cᵒᵖ, Set] est plein et fidèle — un objet est déterminé par la façon dont les autres le voient. representableByYoneda en donne la reconnaissance. C’est ce plongement qui, appliqué à un site, devient le faisceau de Yoneda — le pont vers la section 6.

Les limites (limit_object, colimit_object) fournissent les cônes universels ; les extensions de Kan (kan_extension_left) étendent un foncteur le long d’un autre de façon universelle — l’outil qui rend rigoureux « prolonger par adjonction », et le cadre des formules de calcul de colimites par points. Leur signature dans la sortie #check montre les univers (u₁ u₂) : Mathlib 4 les gère explicitement.

-- Adjunction : une adjonction distribue sur les limites côté droit et les colimites côté gauche
#check Grothendieck.Adjunction.leftAdjoint_preserves_colimits
#check Grothendieck.Adjunction.rightAdjoint_preserves_limits
#check Grothendieck.Adjunction.adj_toEquivalence
-- YonedaLemma : le plongement de Yoneda est plein
#check Grothendieck.yoneda_equiv_apply
#check Grothendieck.yoneda_full
#check Grothendieck.representableByYoneda
-- Equivalences : les équivalences forment une structure symétrique et transitive
#check Grothendieck.Equivalences.equivalence_symm
#check Grothendieck.Equivalences.equivalence_trans
-- Limits : objets limites (cônes universels)
#check Grothendieck.Limits.limit_object
#check Grothendieck.Limits.colimit_object
-- KanExtensions : l'extension de Kan gauche, adjoint à la précomposition
#check Grothendieck.KanExtensions.kan_extension_left
#check Grothendieck.KanExtensions.lan_functor

3. Categories comma, monades, monoidales

Les structures qui organisent les morphismes plutôt que les objets.

Ce que disent les théorèmes. Une catégorie comma (F ↓ G) a pour objets les triples (X, Y, f : F X → G Y) et pour morphismes les paires qui font commuter le carré. fstFunctor et sndFunctor en sont les deux projections vers les catégories sources. C’est l’usine à catégories de la géométrie : le site de Zariski se construit comme une comma (§8), la catégorie des points d’un topos aussi.

Une adjonction engendre une monade (toMonad_underlying) : composer R ∘ L avec l’unité donne un monoïde dans les endofoncteurs. La catégorie de Kleisli (kleisli_type) est la plus petite catégorie dans laquelle cette monade devient « passage au résultat » — le cadre sémantique des effets en programmation, et l’exemple le plus simple de ce qu’un topos généralise.

Les catégories monoïdales portent deux contraintes de cohérence : le pentagone (l’associativité de ⊗ itère cohéremment — les cinq chemins de (A⊗B)⊗C)⊗D → A⊗(B⊗(C⊗D)) coïncident) et le tressage (braiding_iso : A⊗B ≅ B⊗A, de façon cohérente avec l’associativité). La sortie de pentagon_field est littéralement le diagramme commutatif habituel, encodé comme un champ de structure — la cohérence n’est pas un théorème ici, c’est une donnée transportée par la structure.

-- Comma : les catégories comma avec leurs deux projections
#check Grothendieck.Comma.fstFunctor
#check Grothendieck.Comma.sndFunctor
#check Grothendieck.Comma.comma_category_field
-- Monads : une adjonction engendre une monade et une catégorie de Kleisli
#check Grothendieck.Monads.toMonad_underlying
#check Grothendieck.Monads.kleisli_type
-- MonoidalCategories : la cohérence monoïdale : pentagone et tressage
#check Grothendieck.MonoidalCategories.tensor_product
#check Grothendieck.MonoidalCategories.braiding_iso
#check Grothendieck.MonoidalCategories.pentagon_field

-- Comma : les catégories comma avec leurs deux projections

#check Grothendieck.Comma.fstFunctor Grothendieck.Comma.fstFunctor.{v₁, v₂, v₃, u₁, u₂, u₃} {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂}
  [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} :
  CategoryTheory.Functor (CategoryTheory.Comma L R) A

#check Grothendieck.Comma.sndFunctor Grothendieck.Comma.sndFunctor.{v₁, v₂, v₃, u₁, u₂, u₃} {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂}
  [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} :
  CategoryTheory.Functor (CategoryTheory.Comma L R) B

#check Grothendieck.Comma.comma_category_field Grothendieck.Comma.comma_category_field.{v₁, v₂, v₃, u₁, u₂, u₃} {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} :
  CategoryTheory.Category.{max v₁ v₂, max (max u₂ u₁) v₃} (CategoryTheory.Comma L R)

-- Monads : une adjonction engendre une monade et une catégorie de Kleisli

#check Grothendieck.Monads.toMonad_underlying Grothendieck.Monads.toMonad_underlying.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₁}
  [CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) :
  CategoryTheory.Functor C C

#check Grothendieck.Monads.kleisli_type Grothendieck.Monads.kleisli_type.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C]
  (T : CategoryTheory.Monad C) : Type u₁

-- MonoidalCategories : la cohérence monoïdale : pentagone et tressage

#check Grothendieck.MonoidalCategories.tensor_product Grothendieck.MonoidalCategories.tensor_product.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] (X Y : C) : C

#check Grothendieck.MonoidalCategories.braiding_iso Grothendieck.MonoidalCategories.braiding_iso.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) :
  CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X

#check Grothendieck.MonoidalCategories.pentagon_field Grothendieck.MonoidalCategories.pentagon_field.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.MonoidalCategoryStruct C] (Y₁ Y₂ Y₃ Y₄ : C) : Prop

--% env 2

Raw input

{"cmd": "-- Comma : les cat\u00e9gories comma avec leurs deux projections\n#check Grothendieck.Comma.fstFunctor\n#check Grothendieck.Comma.sndFunctor\n#check Grothendieck.Comma.comma_category_field\n-- Monads : une adjonction engendre une monade et une cat\u00e9gorie de Kleisli\n#check Grothendieck.Monads.toMonad_underlying\n#check Grothendieck.Monads.kleisli_type\n-- MonoidalCategories : la coh\u00e9rence mono\u00efdale : pentagone et tressage\n#check Grothendieck.MonoidalCategories.tensor_product\n#check Grothendieck.MonoidalCategories.braiding_iso\n#check Grothendieck.MonoidalCategories.pentagon_field", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Grothendieck.Comma.fstFunctor.{v₁, v₂, v₃, u₁, u₂, u₃} {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂}\n  [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T]\n  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} :\n  CategoryTheory.Functor (CategoryTheory.Comma L R) A"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Grothendieck.Comma.sndFunctor.{v₁, v₂, v₃, u₁, u₂, u₃} {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂}\n  [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T]\n  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} :\n  CategoryTheory.Functor (CategoryTheory.Comma L R) B"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Grothendieck.Comma.comma_category_field.{v₁, v₂, v₃, u₁, u₂, u₃} {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A]\n  {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T]\n  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} :\n  CategoryTheory.Category.{max v₁ v₂, max (max u₂ u₁) v₃} (CategoryTheory.Comma L R)"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "Grothendieck.Monads.toMonad_underlying.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₁}\n  [CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) :\n  CategoryTheory.Functor C C"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "Grothendieck.Monads.kleisli_type.{v₁, u₁} {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C]\n  (T : CategoryTheory.Monad C) : Type u₁"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "Grothendieck.MonoidalCategories.tensor_product.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  [CategoryTheory.MonoidalCategory C] (X Y : C) : C"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "Grothendieck.MonoidalCategories.braiding_iso.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) :\n  CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 6},
   "data":
   "Grothendieck.MonoidalCategories.pentagon_field.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  [CategoryTheory.MonoidalCategoryStruct C] (Y₁ Y₂ Y₃ Y₄ : C) : Prop"}],
 "env": 2}

4. Cribles, topologies et generation

Le sol grothendieckien : on remplace « un recouvrement est une famille » par « un crible est un ensemble de flèches saturé par composition », et toute la théorie des sites devient calcul de treillis.

Ce que disent les théorèmes. Un crible (sieve) sur X est un ensemble de flèches vers X tel que si f ∈ S alors f ∘ g ∈ S pour tout g composable. La génération est monotone : agrandir le générateur agrandid le crible engendré. L’ordre des topologies a un plus petit élément (la triviale : seuls les isomorphismes couvrent), un plus grand (la discrète : tout couvre) et entre les deux la dense — le lake formalise triviale ≤ discrète (§9), chaque inégalité étant un lemme. Le pullback de cribles transporte un crible le long d’une flèche, et c’est ce qui rend la stabilité par changement de base possible.

Pourquoi cette section est le cœur du lake. La famille Covers* (section suivante) redéfinira chaque notion en « forme flèche » — mais la forme crible reste le langage dans lequel les topologies se comparent. La génération d’une topologie à partir d’une coverage (CoverageGen) est le pont pratique : c’est ainsi qu’on spécifie un site (donner les recouvrements de base) et que le lake reconstruit la topologie complète.

-- SieveGenerate : la génération d'un crible est monotone
#check Grothendieck.generate_monotone
-- SieveOps : la topologie triviale est la plus petite
#check Grothendieck.trivial_le_any
-- SieveLattice : le pullback de cribles est une structure d'action
#check Grothendieck.pullback_pullback
-- TopologyLattice : l'ordre des topologies est porté par les recouvrements
#check Grothendieck.TopologyLattice.le_covers
-- DenseTopology : dense est strictement entre triviale et discrète
#check Grothendieck.DenseTopology.dense_le_discrete
-- CoverageGen : une coverage engendre une topologie de Grothendieck
#check Grothendieck.coverageToTopology

-- SieveGenerate : la génération d'un crible est monotone

#check Grothendieck.generate_monotone Grothendieck.generate_monotone.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C}
  {R₁ R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂) :
  CategoryTheory.Sieve.generate R₁ ≤ CategoryTheory.Sieve.generate R₂

-- SieveOps : la topologie triviale est la plus petite

#check Grothendieck.trivial_le_any Grothendieck.trivial_le_any.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C]
  (J : CategoryTheory.GrothendieckTopology C) : CategoryTheory.GrothendieckTopology.trivial C ≤ J

-- SieveLattice : le pullback de cribles est une structure d'action

#check Grothendieck.pullback_pullback Grothendieck.pullback_pullback.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : C}
  (S : CategoryTheory.Sieve X) (f : Y ⟶ X) (g : Z ⟶ Y) :
  CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.pullback f S) =
    CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp g f) S

-- TopologyLattice : l'ordre des topologies est porté par les recouvrements

#check Grothendieck.TopologyLattice.le_covers Grothendieck.TopologyLattice.le_covers.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C}
  {J₁ J₂ : CategoryTheory.GrothendieckTopology C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X) :
  J₁ ≤ J₂ → J₁.Covers S f → J₂.Covers S f

-- DenseTopology : dense est strictement entre triviale et discrète

#check Grothendieck.DenseTopology.dense_le_discrete Grothendieck.DenseTopology.dense_le_discrete.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
  CategoryTheory.GrothendieckTopology.dense ≤ CategoryTheory.GrothendieckTopology.discrete C

-- CoverageGen : une coverage engendre une topologie de Grothendieck

#check Grothendieck.coverageToTopology Grothendieck.coverageToTopology.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C]
  (K : CategoryTheory.Coverage C) : CategoryTheory.GrothendieckTopology C

--% env 3

Raw input

{"cmd": "-- SieveGenerate : la g\u00e9n\u00e9ration d'un crible est monotone\n#check Grothendieck.generate_monotone\n-- SieveOps : la topologie triviale est la plus petite\n#check Grothendieck.trivial_le_any\n-- SieveLattice : le pullback de cribles est une structure d'action\n#check Grothendieck.pullback_pullback\n-- TopologyLattice : l'ordre des topologies est port\u00e9 par les recouvrements\n#check Grothendieck.TopologyLattice.le_covers\n-- DenseTopology : dense est strictement entre triviale et discr\u00e8te\n#check Grothendieck.DenseTopology.dense_le_discrete\n-- CoverageGen : une coverage engendre une topologie de Grothendieck\n#check Grothendieck.coverageToTopology", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Grothendieck.generate_monotone.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C}\n  {R₁ R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂) :\n  CategoryTheory.Sieve.generate R₁ ≤ CategoryTheory.Sieve.generate R₂"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Grothendieck.trivial_le_any.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C]\n  (J : CategoryTheory.GrothendieckTopology C) : CategoryTheory.GrothendieckTopology.trivial C ≤ J"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "Grothendieck.pullback_pullback.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : C}\n  (S : CategoryTheory.Sieve X) (f : Y ⟶ X) (g : Z ⟶ Y) :\n  CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.pullback f S) =\n    CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp g f) S"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "Grothendieck.TopologyLattice.le_covers.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C}\n  {J₁ J₂ : CategoryTheory.GrothendieckTopology C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X) :\n  J₁ ≤ J₂ → J₁.Covers S f → J₂.Covers S f"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "Grothendieck.DenseTopology.dense_le_discrete.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :\n  CategoryTheory.GrothendieckTopology.dense ≤ CategoryTheory.GrothendieckTopology.discrete C"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 6},
   "data":
   "Grothendieck.coverageToTopology.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C]\n  (K : CategoryTheory.Coverage C) : CategoryTheory.GrothendieckTopology C"}],
 "env": 3}

5. La forme fleche des recouvrements (famille Covers*)

Le cœur original du lake : remplacer « une famille de flèches couvre » par un prédicat binaire J.Covers S f — la flèche f est couverte par la structure S. Chaque topologie de la section 4 possède sa version arrow (atomique, Zariski, dense, coverage, pré-coverage, pré-topologie), et chaque opération a ses lois.

Ce que disent les théorèmes. covers_iff_covers_id : recouvrir f équivaut à recouvrir l’identité après pullback — la forme flèche est auto-équivalente à la forme famille, mais se compose mieux. covers_bind est l’axiome de liaison : si f est couverte et que chaque flèche du recouvrement est elle-même couverte, alors f est couverte — c’est la transitivité des recouvrements, l’ingrédient qui distingue une topologie d’une simple coverage. covers_top : le recouvrement maximal existe (tout couvre). sInf_covers : le treillis — l’intersection de familles couvrantes couvre. cover_pullback_covers : la stabilité par changement de base, l’axiome le plus important pour la géométrie (un recouvrement reste un recouvrement après pullback le long de n’importe quelle flèche — sans elle, pas de faisceaux). pushforward_pullback_fixed : l’image directe et le pullback sont adjoints sur les recouvrements.

Pourquoi c’est la famille la plus étendue du lake. C’est ici que la pédagogie des topologies de Grothendieck devient opératoire : chaque loi correspond à une manipulation concrète de recouvrements, et le lake prouve chacune comme théorème — pas comme axiome. La sortie #check de cette section est la plus longue du notebook : c’est la preuve que la formalisation de la « famille » au sens de SAGA est complète jusqu’à l’associativité de la liaison.

-- CoversArrow : forme flèche : recouvrir `f` équivaut à recouvrir `id`
#check Grothendieck.CoversArrow.covers_iff_covers_id
-- CoversAtomicArrow : la topologie atomique en forme flèche
#check Grothendieck.CoversAtomicArrow.atomic_covering
#check Grothendieck.CoversAtomicArrow.covers_iff_atomic
-- CoversBind : l'axiome de liaison des topologies en forme flèche
#check Grothendieck.CoversBind.covers_bind
-- CoversLattice : structure de treillis sur les recouvrements
#check Grothendieck.CoversLattice.sInf_covers
-- CoversOrder : le recouvrement maximal est top
#check Grothendieck.CoversOrder.covers_top
-- CoversPullback : stabilité par pullback des recouvrements
#check Grothendieck.CoversPullback.cover_pullback_covers
-- CoversPushforward : image directe des recouvrements
#check Grothendieck.CoversPushforward.pushforward_pullback_fixed
#check Grothendieck.CoversPushforward.pullback_pushforward_fixed
-- CoversTopologies : recouvrements de la topologie dense
#check Grothendieck.CoversTopologies.dense_covers_iff
-- CoversZariskiArrow : le site de Zariski en forme flèche
#check Grothendieck.CoversZariskiArrow.covers_iff_zariski
-- CoversCoverageArrow : la conversion coverage → topologie en forme flèche
#check Grothendieck.CoversCoverageArrow.covers_iff_toGrothendieck
-- CoversPrecoverageArrow : la conversion pré-coverage → topologie
#check Grothendieck.CoversPrecoverageArrow.covers_iff_toGrothendieck
-- CoversPretopologyArrow : la conversion pré-topologie → topologie
#check Grothendieck.CoversPretopologyArrow.covers_toGrothendieck_of_of
-- PullbackCoversLaws : l'associativité du pullback de recouvrements
#check Grothendieck.PullbackCoversLaws.covers_pullback_assoc
-- PullbackFunctor : le foncteur pullback et ses unités
#check Grothendieck.PullbackFunctor.pullback_triple
-- PullbackFunctorLaws : les lois du foncteur pullback
#check Grothendieck.PullbackFunctorLaws.covers_pullback_comp

6. Faisceaux, faisceautisation, sous-canonicalite

Au-dessus du site, les faisceaux : les préfaisceaux qui « collent » les sections locales en sections globales. Cette section est le cœur conceptuel du topos — un faisceau n’est pas une donnée, c’est une manière de répondre aux recouvrements.

Ce que disent les théorèmes. sheaf_is_separated : un faisceau est en particulier séparé — deux sections qui coïncident localement coïncident (la moitié « unicité » de la condition de faisceau ; isSheaf_of_le raffine : si la topologie est plus petite, le faisceau l’est aussi). sheafHom_isSheaf : le faisceau interne des homomorphismes ℋ𝗈𝗆(F, G) est un faisceau — l’objet qui rend les morphismes de faisceaux eux-mêmes manipulables géométriquement. sheafification_universal est le théorème d’existence clé : la faisceautisation est adjointe à l’inclusion Sheaf α J ↪ Presheaf α — tout préfaisceau se transforme en faisceau de façon universelle. C’est « the plus construction » : itérée une fois pour les topologies finitaires, transfinie en général. plus_preserves_finite_limits : l’exactitude à gauche — la faisceautisation préserve les limites finies, ce qui fait des faisceaux une catégorie abélienne-en-esprit, le prérequis pour la cohomologie de la section 7. isConstant_iff_counit_iso : un faisceau constant est caractérisé par son adjonction avec le foncteur sections constantes. canonical_is_subcanonical : la sous-canonicalité — le faisceau de Yoneda est un faisceau pour la topologie canonique, la topologie la plus fine pour laquelle ça reste vrai. C’est le plongement de Yoneda (§2) qui devient faisceau — la boucle est bouclée.

-- SheafBasics : un faisceau est en particulier séparé
#check Grothendieck.sheaf_is_separated
#check Grothendieck.isSheaf_of_le
-- SheafHom : le faisceau interne des homomorphismes
#check Grothendieck.SheafHom.sheafHom_isSheaf
-- Sheafification : la propriété universelle de la faisceautisation
#check Grothendieck.sheafification_universal
-- ConstantSheaf : un faisceau constant caractérisé par son adjonction
#check Grothendieck.ConstantSheaf.isConstant_iff_counit_iso
-- LeftExact : la faisceautisation préserve les limites finies (exactitude à gauche)
#check Grothendieck.plus_preserves_finite_limits
-- Subcanonical : sous-canonicalité : le plongement de Yoneda est un faisceau
#check Grothendieck.Subcanonical.subcanonical_of_yoneda_sheaf
-- CanonicalProps : la topologie canonique est sous-canonique
#check Grothendieck.canonical_is_subcanonical

-- SheafBasics : un faisceau est en particulier séparé

#check Grothendieck.sheaf_is_separated Grothendieck.sheaf_is_separated.{u_1, u_2, u_3} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C]
  {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ (Type u_2)}
  (h : CategoryTheory.Presieve.IsSheaf J P) : CategoryTheory.Presieve.IsSeparated J P

#check Grothendieck.isSheaf_of_le Grothendieck.isSheaf_of_le.{u_1, u_2, u_3} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C]
  {J₁ J₂ : CategoryTheory.GrothendieckTopology C} (h : J₁ ≤ J₂) {P : CategoryTheory.Functor Cᵒᵖ (Type u_2)}
  (hP : CategoryTheory.Presieve.IsSheaf J₂ P) : CategoryTheory.Presieve.IsSheaf J₁ P

-- SheafHom : le faisceau interne des homomorphismes

#check Grothendieck.SheafHom.sheafHom_isSheaf Grothendieck.SheafHom.sheafHom_isSheaf.{v, v', u, u'} {C : Type u} [CategoryTheory.Category.{v, u} C]
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A]
  (F G : CategoryTheory.Sheaf J A) : CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.sheafHom F G).obj

-- Sheafification : la propriété universelle de la faisceautisation

#check Grothendieck.sheafification_universal Grothendieck.sheafification_universal.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  (J : CategoryTheory.GrothendieckTopology C) :
  CategoryTheory.presheafToSheaf J (Type (max u v)) ⊣ CategoryTheory.sheafToPresheaf J (Type (max u v))

-- ConstantSheaf : un faisceau constant caractérisé par son adjonction

#check Grothendieck.ConstantSheaf.isConstant_iff_counit_iso Grothendieck.ConstantSheaf.isConstant_iff_counit_iso.{v, v', u, u'} {C : Type u} [CategoryTheory.Category.{v, u} C]
  (J : CategoryTheory.GrothendieckTopology C) {D : Type u'} [CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.HasWeakSheafify J D] [(CategoryTheory.constantSheaf J D).Faithful]
  [(CategoryTheory.constantSheaf J D).Full] (F : CategoryTheory.Sheaf J D) {T : C}
  (hT : CategoryTheory.Limits.IsTerminal T) :
  CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.IsIso ((CategoryTheory.constantSheafAdj J D hT).counit.app F)

-- LeftExact : la faisceautisation préserve les limites finies (exactitude à gauche)

#check Grothendieck.plus_preserves_finite_limits Grothendieck.plus_preserves_finite_limits.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  (J : CategoryTheory.GrothendieckTopology C) :
  CategoryTheory.Limits.PreservesFiniteLimits (J.plusFunctor (Type (max u v)))

-- Subcanonical : sous-canonicalité : le plongement de Yoneda est un faisceau

#check Grothendieck.Subcanonical.subcanonical_of_yoneda_sheaf Grothendieck.Subcanonical.subcanonical_of_yoneda_sheaf.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  (J : CategoryTheory.GrothendieckTopology C)
  (h : ∀ (X : C), CategoryTheory.Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)) : J.Subcanonical

-- CanonicalProps : la topologie canonique est sous-canonique

#check Grothendieck.canonical_is_subcanonical Grothendieck.canonical_is_subcanonical.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
  (CategoryTheory.Sheaf.canonicalTopology C).Subcanonical

--% env 5

Raw input

{"cmd": "-- SheafBasics : un faisceau est en particulier s\u00e9par\u00e9\n#check Grothendieck.sheaf_is_separated\n#check Grothendieck.isSheaf_of_le\n-- SheafHom : le faisceau interne des homomorphismes\n#check Grothendieck.SheafHom.sheafHom_isSheaf\n-- Sheafification : la propri\u00e9t\u00e9 universelle de la faisceautisation\n#check Grothendieck.sheafification_universal\n-- ConstantSheaf : un faisceau constant caract\u00e9ris\u00e9 par son adjonction\n#check Grothendieck.ConstantSheaf.isConstant_iff_counit_iso\n-- LeftExact : la faisceautisation pr\u00e9serve les limites finies (exactitude \u00e0 gauche)\n#check Grothendieck.plus_preserves_finite_limits\n-- Subcanonical : sous-canonicalit\u00e9 : le plongement de Yoneda est un faisceau\n#check Grothendieck.Subcanonical.subcanonical_of_yoneda_sheaf\n-- CanonicalProps : la topologie canonique est sous-canonique\n#check Grothendieck.canonical_is_subcanonical", "env": 4}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Grothendieck.sheaf_is_separated.{u_1, u_2, u_3} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C]\n  {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ (Type u_2)}\n  (h : CategoryTheory.Presieve.IsSheaf J P) : CategoryTheory.Presieve.IsSeparated J P"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Grothendieck.isSheaf_of_le.{u_1, u_2, u_3} {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C]\n  {J₁ J₂ : CategoryTheory.GrothendieckTopology C} (h : J₁ ≤ J₂) {P : CategoryTheory.Functor Cᵒᵖ (Type u_2)}\n  (hP : CategoryTheory.Presieve.IsSheaf J₂ P) : CategoryTheory.Presieve.IsSheaf J₁ P"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "Grothendieck.SheafHom.sheafHom_isSheaf.{v, v', u, u'} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A]\n  (F G : CategoryTheory.Sheaf J A) : CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.sheafHom F G).obj"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "Grothendieck.sheafification_universal.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  (J : CategoryTheory.GrothendieckTopology C) :\n  CategoryTheory.presheafToSheaf J (Type (max u v)) ⊣ CategoryTheory.sheafToPresheaf J (Type (max u v))"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "Grothendieck.ConstantSheaf.isConstant_iff_counit_iso.{v, v', u, u'} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  (J : CategoryTheory.GrothendieckTopology C) {D : Type u'} [CategoryTheory.Category.{v', u'} D]\n  [CategoryTheory.HasWeakSheafify J D] [(CategoryTheory.constantSheaf J D).Faithful]\n  [(CategoryTheory.constantSheaf J D).Full] (F : CategoryTheory.Sheaf J D) {T : C}\n  (hT : CategoryTheory.Limits.IsTerminal T) :\n  CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.IsIso ((CategoryTheory.constantSheafAdj J D hT).counit.app F)"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 6},
   "data":
   "Grothendieck.plus_preserves_finite_limits.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  (J : CategoryTheory.GrothendieckTopology C) :\n  CategoryTheory.Limits.PreservesFiniteLimits (J.plusFunctor (Type (max u v)))"},
  {"severity": "info",
   "pos": {"line": 13, "column": 0},
   "endPos": {"line": 13, "column": 6},
   "data":
   "Grothendieck.Subcanonical.subcanonical_of_yoneda_sheaf.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  (J : CategoryTheory.GrothendieckTopology C)\n  (h : ∀ (X : C), CategoryTheory.Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)) : J.Subcanonical"},
  {"severity": "info",
   "pos": {"line": 15, "column": 0},
   "endPos": {"line": 15, "column": 6},
   "data":
   "Grothendieck.canonical_is_subcanonical.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :\n  (CategoryTheory.Sheaf.canonicalTopology C).Subcanonical"}],
 "env": 5}

7. Points, images directes et cohomologie

Les outils calculatoires du topos : si un topos ne se calcule pas directement, ses points et sa cohomologie, si.

Ce que disent les théorèmes. is_colimit_presheaf_fiber : la fibre d’un point (l’ensemble des sections « au-dessus » d’un point du topos) est une colimite filtrante — c’est le théorème des points : tout topos de faisceaux a assez de points, et la fibre résume ce que le point « voit ». pushforward_functor_field et exceptionalDirectImage : les foncteurs image directe — pousser un faisceau le long d’un morphisme de sites — l’image directe exceptionnelle étant la version raffinée pour les morphismes non propres.

H⁰ est la section globale (H0_equiv_global_sections) : le H⁰ de la cohomologie de faisceaux n’est pas analogue aux sections globales, il est l’espace des sections globales — le théorème qui fonde toute l’analogie « cohomologie = obstruction à recoller ». cechComplexObj : l’objet du complexe de Čech, la machine combinatoire qui approche la cohomologie par les recouvrements. mv_sequence_exact : la suite de Mayer-Vietoris est exacte — sur un carré de recouvrement, les cohomologies s’assemblent en suite exacte ; c’est l’outil de calcul effectif (celui qui calcule H*(ℙ¹) par recouvrements de deux affines). preserves_finite_limits_and_colimits : les foncteurs de points préservent limites et colimites — la régularité qui rend le calcul par points fidèle.

-- SitePoints : la fibre d'un point est une colimite
#check Grothendieck.is_colimit_presheaf_fiber
-- DirectImage : le foncteur image directe
#check Grothendieck.DirectImage.pushforward_functor_field
-- ExceptionalDirect : l'image directe exceptionnelle
#check Grothendieck.ExceptionalDirect.exceptionalDirectImage
-- SheafCohomology.Basic : H⁰ est la section globale
#check Grothendieck.SheafCohomology.H0_equiv_global_sections
-- SheafCohomology.Cech : l'objet du complexe de Čech
#check Grothendieck.SheafCohomology.Cech.cechComplexObj
-- SheafCohomology.MayerVietoris : l'exactitude de la suite de Mayer-Vietoris
#check Grothendieck.SheafCohomology.MayerVietoris.mv_sequence_exact
-- MayerVietorisSquare : le complexe court du carré de Mayer-Vietoris
#check Grothendieck.MayerVietorisSquare.mv_short_complex

-- SitePoints : la fibre d'un point est une colimite

#check Grothendieck.is_colimit_presheaf_fiber Grothendieck.is_colimit_presheaf_fiber.{v, u, w} {C : Type u} [CategoryTheory.Category.{v, u} C]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (P : CategoryTheory.Functor Cᵒᵖ (Type (max u w))) :
  CategoryTheory.Limits.IsColimit (Φ.presheafFiberCocone P)

-- DirectImage : le foncteur image directe

#check Grothendieck.DirectImage.pushforward_functor_field Grothendieck.DirectImage.pushforward_functor_field.{u} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
  CategoryTheory.Functor X.Modules Y.Modules

-- ExceptionalDirect : l'image directe exceptionnelle

#check Grothendieck.ExceptionalDirect.exceptionalDirectImage Grothendieck.ExceptionalDirect.exceptionalDirectImage.{v₁, v₂, v₃, u₁, u₂, u₃} {C : Type u₁}
  [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {H : Type u₃}
  [CategoryTheory.Category.{v₃, u₃} H] (f : CategoryTheory.Functor C D)
  [∀ (F : CategoryTheory.Functor Cᵒᵖ H), f.op.HasLeftKanExtension F] :
  CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ H) (CategoryTheory.Functor Dᵒᵖ H)

-- SheafCohomology.Basic : H⁰ est la section globale

#check Grothendieck.SheafCohomology.H0_equiv_global_sections Grothendieck.SheafCohomology.H0_equiv_global_sections.{w', w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  {J : CategoryTheory.GrothendieckTopology C} (F : CategoryTheory.Sheaf J AddCommGrpCat) {T : C}
  (hT : CategoryTheory.Limits.IsTerminal T) [CategoryTheory.HasSheafify J AddCommGrpCat]
  [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] : F.H 0 ≃+ ↑(F.obj.obj (Opposite.op T))

-- SheafCohomology.Cech : l'objet du complexe de Čech

#check Grothendieck.SheafCohomology.Cech.cechComplexObj Grothendieck.SheafCohomology.Cech.cechComplexObj.{w, v, v', u, u'} {C : Type u} [CategoryTheory.Category.{v, u} C]
  {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A]
  [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasFiniteProducts C] {ι : Type w} (U : ι → C)
  (P : CategoryTheory.Functor Cᵒᵖ A) (n : ℕ) : A

-- SheafCohomology.MayerVietoris : l'exactitude de la suite de Mayer-Vietoris

#check Grothendieck.SheafCohomology.MayerVietoris.mv_sequence_exact Grothendieck.SheafCohomology.MayerVietoris.mv_sequence_exact.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)]
  [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)]
  (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
  (S.sequence F n₀ n₁ h).Exact

-- MayerVietorisSquare : le complexe court du carré de Mayer-Vietoris

#check Grothendieck.MayerVietorisSquare.mv_short_complex Grothendieck.MayerVietorisSquare.mv_short_complex.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)]
  [CategoryTheory.HasSheafify J AddCommGrpCat] (S : J.MayerVietorisSquare) :
  CategoryTheory.ShortComplex (CategoryTheory.Sheaf J AddCommGrpCat)

--% env 6

Raw input

{"cmd": "-- SitePoints : la fibre d'un point est une colimite\n#check Grothendieck.is_colimit_presheaf_fiber\n-- DirectImage : le foncteur image directe\n#check Grothendieck.DirectImage.pushforward_functor_field\n-- ExceptionalDirect : l'image directe exceptionnelle\n#check Grothendieck.ExceptionalDirect.exceptionalDirectImage\n-- SheafCohomology.Basic : H\u2070 est la section globale\n#check Grothendieck.SheafCohomology.H0_equiv_global_sections\n-- SheafCohomology.Cech : l'objet du complexe de \u010cech\n#check Grothendieck.SheafCohomology.Cech.cechComplexObj\n-- SheafCohomology.MayerVietoris : l'exactitude de la suite de Mayer-Vietoris\n#check Grothendieck.SheafCohomology.MayerVietoris.mv_sequence_exact\n-- MayerVietorisSquare : le complexe court du carr\u00e9 de Mayer-Vietoris\n#check Grothendieck.MayerVietorisSquare.mv_short_complex", "env": 5}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Grothendieck.is_colimit_presheaf_fiber.{v, u, w} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (P : CategoryTheory.Functor Cᵒᵖ (Type (max u w))) :\n  CategoryTheory.Limits.IsColimit (Φ.presheafFiberCocone P)"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Grothendieck.DirectImage.pushforward_functor_field.{u} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :\n  CategoryTheory.Functor X.Modules Y.Modules"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "Grothendieck.ExceptionalDirect.exceptionalDirectImage.{v₁, v₂, v₃, u₁, u₂, u₃} {C : Type u₁}\n  [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {H : Type u₃}\n  [CategoryTheory.Category.{v₃, u₃} H] (f : CategoryTheory.Functor C D)\n  [∀ (F : CategoryTheory.Functor Cᵒᵖ H), f.op.HasLeftKanExtension F] :\n  CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ H) (CategoryTheory.Functor Dᵒᵖ H)"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "Grothendieck.SheafCohomology.H0_equiv_global_sections.{w', w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  {J : CategoryTheory.GrothendieckTopology C} (F : CategoryTheory.Sheaf J AddCommGrpCat) {T : C}\n  (hT : CategoryTheory.Limits.IsTerminal T) [CategoryTheory.HasSheafify J AddCommGrpCat]\n  [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] : F.H 0 ≃+ ↑(F.obj.obj (Opposite.op T))"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "Grothendieck.SheafCohomology.Cech.cechComplexObj.{w, v, v', u, u'} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A]\n  [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasFiniteProducts C] {ι : Type w} (U : ι → C)\n  (P : CategoryTheory.Functor Cᵒᵖ A) (n : ℕ) : A"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 6},
   "data":
   "Grothendieck.SheafCohomology.MayerVietoris.mv_sequence_exact.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)]\n  [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)]\n  (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :\n  (S.sequence F n₀ n₁ h).Exact"},
  {"severity": "info",
   "pos": {"line": 14, "column": 0},
   "endPos": {"line": 14, "column": 6},
   "data":
   "Grothendieck.MayerVietorisSquare.mv_short_complex.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)]\n  [CategoryTheory.HasSheafify J AddCommGrpCat] (S : J.MayerVietorisSquare) :\n  CategoryTheory.ShortComplex (CategoryTheory.Sheaf J AddCommGrpCat)"}],
 "env": 6}

8. Geometrie : schemas, Zariski, construction, points

L’ancrage géométrique : tout ce qui précède devient de la géométrie algébrique effective.

Ce que disent les théorèmes. scheme_hom_continuous : un morphisme de schémas est une application continue sur les espaces topologiques sous-jacents — le formalisme donne gratuitement le socle topologique. zariski_topology_eq : la topologie de Zariski est une topologie de Grothendieck — l’identification qui rend le site de Zariski un objet du langage des sections 4-5, pas une analogie. grothendieck_field et forget_family : la construction de Grothendieck — le préfaisceau X ↦ ∐ familles qui associe à chaque objet ses familles de flèches ; c’est le germe de la construction Spec, le pont fonctoriel entre algèbre et géométrie. has_enough_points_field : une famille conservatrice de points — assez de points pour que l’isomorphisme sur tous les points implique l’isomorphisme ; c’est le théorème des points suffisants, le passage « local → global » pour les propriétés vérifiables fibre par fibre (W_iff_field : une propriété W vaut ssi elle vaut sur chaque point).

Pourquoi ce “Tour”. Ces modules sont volontairement une ** visite guidée** plutôt qu’un traité : ils attestent que le lake descend jusqu’aux objets géométriques concrets (schémas, Zariski), et que la chaîne complète Yoneda → sites → faisceaux → cohomologie → géométrie tient dans un seul environnement Lean 4 chargé d’un seul import.

-- SchemesTour : les morphismes de schémas sont continus
#check Grothendieck.scheme_hom_continuous
-- ZariskiSite : la topologie de Zariski est une topologie de Grothendieck
#check Grothendieck.zariski_topology_eq
-- Construction : la construction du préfaisceau de Grothendieck
#check Grothendieck.Construction.grothendieck_field
#check Grothendieck.Construction.forget_family
-- Conservative : une famille conservatrice de points
#check Grothendieck.Conservative.has_enough_points_field
#check Grothendieck.Conservative.W_iff_field

-- SchemesTour : les morphismes de schémas sont continus

#check Grothendieck.scheme_hom_continuous Grothendieck.scheme_hom_continuous.{u_1} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Continuous ⇑f

-- ZariskiSite : la topologie de Zariski est une topologie de Grothendieck

#check Grothendieck.zariski_topology_eq Grothendieck.zariski_topology_eq.{u_1} :
  AlgebraicGeometry.Scheme.zariskiTopology = AlgebraicGeometry.Scheme.zariskiPretopology.toGrothendieck

-- Construction : la construction du préfaisceau de Grothendieck

#check Grothendieck.Construction.grothendieck_field Grothendieck.Construction.grothendieck_field.{v, v₂, u, u₂} {C : Type u} [CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor C CategoryTheory.Cat) : Type (max u₂ u)

#check Grothendieck.Construction.forget_family Grothendieck.Construction.forget_family.{v, v₂, u, u₂} {C : Type u} [CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor C CategoryTheory.Cat) : CategoryTheory.Functor (CategoryTheory.Grothendieck F) C

-- Conservative : une famille conservatrice de points

#check Grothendieck.Conservative.has_enough_points_field Grothendieck.Conservative.has_enough_points_field.{v, u, w} {C : Type u} [CategoryTheory.Category.{v, u} C]
  (J : CategoryTheory.GrothendieckTopology C) : Prop

#check Grothendieck.Conservative.W_iff_field Grothendieck.Conservative.W_iff_field.{v, v', u, u', w, u_1} {C : Type u} [CategoryTheory.Category.{v, u} C]
  {J : CategoryTheory.GrothendieckTopology C} (P : CategoryTheory.ObjectProperty J.Point) {A : Type u'}
  [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w}
  [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC]
  [(CategoryTheory.forget A).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)]
  [J.HasSheafCompose (CategoryTheory.forget A)] (hP : P.IsConservativeFamilyOfPoints)
  [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] {F G : CategoryTheory.Functor Cᵒᵖ A}
  (f : F ⟶ G) : J.W f ↔ ∀ (Φ : P.FullSubcategory), CategoryTheory.IsIso (Φ.obj.presheafFiber.map f)

--% env 7

Raw input

{"cmd": "-- SchemesTour : les morphismes de sch\u00e9mas sont continus\n#check Grothendieck.scheme_hom_continuous\n-- ZariskiSite : la topologie de Zariski est une topologie de Grothendieck\n#check Grothendieck.zariski_topology_eq\n-- Construction : la construction du pr\u00e9faisceau de Grothendieck\n#check Grothendieck.Construction.grothendieck_field\n#check Grothendieck.Construction.forget_family\n-- Conservative : une famille conservatrice de points\n#check Grothendieck.Conservative.has_enough_points_field\n#check Grothendieck.Conservative.W_iff_field", "env": 6}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Grothendieck.scheme_hom_continuous.{u_1} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Continuous ⇑f"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Grothendieck.zariski_topology_eq.{u_1} :\n  AlgebraicGeometry.Scheme.zariskiTopology = AlgebraicGeometry.Scheme.zariskiPretopology.toGrothendieck"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "Grothendieck.Construction.grothendieck_field.{v, v₂, u, u₂} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  (F : CategoryTheory.Functor C CategoryTheory.Cat) : Type (max u₂ u)"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "Grothendieck.Construction.forget_family.{v, v₂, u, u₂} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  (F : CategoryTheory.Functor C CategoryTheory.Cat) : CategoryTheory.Functor (CategoryTheory.Grothendieck F) C"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "Grothendieck.Conservative.has_enough_points_field.{v, u, w} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  (J : CategoryTheory.GrothendieckTopology C) : Prop"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "Grothendieck.Conservative.W_iff_field.{v, v', u, u', w, u_1} {C : Type u} [CategoryTheory.Category.{v, u} C]\n  {J : CategoryTheory.GrothendieckTopology C} (P : CategoryTheory.ObjectProperty J.Point) {A : Type u'}\n  [CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]\n  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w}\n  [(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory A FC]\n  [(CategoryTheory.forget A).ReflectsIsomorphisms]\n  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (CategoryTheory.forget A)]\n  [J.HasSheafCompose (CategoryTheory.forget A)] (hP : P.IsConservativeFamilyOfPoints)\n  [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasProducts A] {F G : CategoryTheory.Functor Cᵒᵖ A}\n  (f : F ⟶ G) : J.W f ↔ ∀ (Φ : P.FullSubcategory), CategoryTheory.IsIso (Φ.obj.presheafFiber.map f)"}],
 "env": 7}

9. Calibration et couverture bundlee

Les micro-preuves qui ferment la boucle — petites en taille, capitales en fonction : elles calibrent les définitions abstraites contre des cas limites que l’on sait juger à la main.

Ce que disent les théorèmes. trivial_le_discrete : la topologie triviale est plus petite que la discrète — un théorème de un sourire, mais qui vérifie que l’ordre du treillis des topologies va dans le bon sens. pullback_top : tirer en arrière le recouvrement maximal redonne le maximal — la stabilité par changement de base ne perd pas le sommet du treillis. top_covers : l’axiome « top couvre » de la structure de topologie, prouvé ici pour la couverture bundlée. cover_iff_coe_mem : la couverture bundlée J.Cover X = { S : Sieve X // S ∈ J X } est équivalente à l’appartenance du crible — le subtype est fidèle à la théorie, on n’a rien perdu en bundlant. bind_mem_iff : la liaison des couvertures bundlées est l’application membre-pour-membre de la théorie des cribles.

Pourquoi clôturer par la calibration. Un lake qui prouve tout sauf ses propres fondations de définition serait un château sur nuage : ces micro-preuves attestent que les définitions choisies (couverture bundlée, ordre des topologies) sont les bonnes — chaque lemme trivial est un test de non-régression de la formalisation entière.

-- Calibration : micro-preuves : triviale ≤ discrète, pullback de top
#check Grothendieck.trivial_le_discrete
#check Grothendieck.pullback_top
-- CategoryAndSites : les axiomes de topologie (top couvre)
#check Grothendieck.top_covers
-- Cover : la couverture bundlée : `J.Cover X = { S : Sieve X // S ∈ J X }`
#check Grothendieck.Cover.cover_iff_coe_mem
#check Grothendieck.Cover.bind_mem_iff

-- Calibration : micro-preuves : triviale ≤ discrète, pullback de top

#check Grothendieck.trivial_le_discrete Grothendieck.trivial_le_discrete.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :
  CategoryTheory.GrothendieckTopology.trivial C ≤ CategoryTheory.GrothendieckTopology.discrete C

#check Grothendieck.pullback_top Grothendieck.pullback_top.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : Y ⟶ X) :
  CategoryTheory.Sieve.pullback f ⊤ = ⊤

-- CategoryAndSites : les axiomes de topologie (top couvre)

#check Grothendieck.top_covers Grothendieck.top_covers.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C]
  (J : CategoryTheory.GrothendieckTopology C) (X : C) : ⊤ ∈ J.sieves X

-- Cover : la couverture bundlée : `J.Cover X = { S : Sieve X // S ∈ J X }`

#check Grothendieck.Cover.cover_iff_coe_mem Grothendieck.Cover.cover_iff_coe_mem.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C}
  (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve X) : S ∈ J X ↔ ∃ T, ↑T = S

#check Grothendieck.Cover.bind_mem_iff Grothendieck.Cover.bind_mem_iff.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C}
  (J : CategoryTheory.GrothendieckTopology C) {S : J.Cover X} (T : (I : S.Arrow) → J.Cover I.Y) (f : Y ⟶ X) :
  (↑(S.bind T)).arrows f ↔
    ∃ Z e1 e2,
      ∃ (hS : (↑S).arrows e2),
        (↑(T { Y := Z, f := e2, hf := hS })).arrows e1 ∧ CategoryTheory.CategoryStruct.comp e1 e2 = f

--% env 8

Raw input

{"cmd": "-- Calibration : micro-preuves : triviale \u2264 discr\u00e8te, pullback de top\n#check Grothendieck.trivial_le_discrete\n#check Grothendieck.pullback_top\n-- CategoryAndSites : les axiomes de topologie (top couvre)\n#check Grothendieck.top_covers\n-- Cover : la couverture bundl\u00e9e : `J.Cover X = { S : Sieve X // S \u2208 J X }`\n#check Grothendieck.Cover.cover_iff_coe_mem\n#check Grothendieck.Cover.bind_mem_iff", "env": 7}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Grothendieck.trivial_le_discrete.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] :\n  CategoryTheory.GrothendieckTopology.trivial C ≤ CategoryTheory.GrothendieckTopology.discrete C"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Grothendieck.pullback_top.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : Y ⟶ X) :\n  CategoryTheory.Sieve.pullback f ⊤ = ⊤"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "Grothendieck.top_covers.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C]\n  (J : CategoryTheory.GrothendieckTopology C) (X : C) : ⊤ ∈ J.sieves X"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "Grothendieck.Cover.cover_iff_coe_mem.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C}\n  (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve X) : S ∈ J X ↔ ∃ T, ↑T = S"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "Grothendieck.Cover.bind_mem_iff.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C}\n  (J : CategoryTheory.GrothendieckTopology C) {S : J.Cover X} (T : (I : S.Arrow) → J.Cover I.Y) (f : Y ⟶ X) :\n  (↑(S.bind T)).arrows f ↔\n    ∃ Z e1 e2,\n      ∃ (hS : (↑S).arrows e2),\n        (↑(T { Y := Z, f := e2, hf := hS })).arrows e1 ∧ CategoryTheory.CategoryStruct.comp e1 e2 = f"}],
 "env": 8}

10. Integrite des preuves : `#print axioms`

Le moment de vérité : un théorème Lean n’est honnête que si l’on sait sur quoi il repose. #print axioms énumère les axiomes dont dépend un nom — et dans Lean 4 il n’en existe que trois de « standards » : propext (extensionnalité des Prop), Classical.choice (choix global) et Quot.sound (les quotients sont sains). Toute autre entrée — et surtout sorryAx, l’axiome du « trou laissé à compléter » — serait un signal d’alarme : soit un sorry caché, soit un axiome sur mesure qui fait prouver n’importe quoi.

On interroge trois énoncés représentatifs des trois étages du lake : trivial_le_discrete (calibration), adj_toEquivalence (adjonctions), H0_equiv_global_sections (cohomologie).

-- Chaque theoreme du lake ne depend que des axiomes standards de Lean
#print axioms Grothendieck.trivial_le_discrete
#print axioms Grothendieck.Adjunction.adj_toEquivalence
#print axioms Grothendieck.SheafCohomology.H0_equiv_global_sections

-- Chaque theoreme du lake ne depend que des axiomes standards de Lean

#print axioms Grothendieck.trivial_le_discrete 'Grothendieck.trivial_le_discrete' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms Grothendieck.Adjunction.adj_toEquivalence 'Grothendieck.Adjunction.adj_toEquivalence' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms Grothendieck.SheafCohomology.H0_equiv_global_sections 'Grothendieck.SheafCohomology.H0_equiv_global_sections' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 9

Raw input

{"cmd": "-- Chaque theoreme du lake ne depend que des axiomes standards de Lean\n#print axioms Grothendieck.trivial_le_discrete\n#print axioms Grothendieck.Adjunction.adj_toEquivalence\n#print axioms Grothendieck.SheafCohomology.H0_equiv_global_sections\n", "env": 8}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "'Grothendieck.trivial_le_discrete' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "'Grothendieck.Adjunction.adj_toEquivalence' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "'Grothendieck.SheafCohomology.H0_equiv_global_sections' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 9}

Lecture de la sortie

La sortie ci-dessus répond trois fois la même chose : depends on axioms: [propext, Classical.choice, Quot.sound]. Détaillons ce que chaque axiome affirme — et pourquoi leur présence est une bonne nouvelle, pas une réserve :

propext (extensionnalité des propositions) : deux Props équivalentes sont égales. C’est ce qui permet à Lean de traiter les énoncés à équivalence logique près — sans lui, aucune bibliothèque sérieuse ne se construit.
Classical.choice (axiome du choix global) : toute relation totale admet un choix. C’est le prix du raisonnement classique (tiers exclu, preuves par contradiction) — Mathlib l’assume partout.
Quot.sound : les quotients (colimites de relations d’équivalence) sont sains. C’est lui qui rend possibles les constructions à la ℤ = ℕ × ℕ / ~ — et donc une grande partie de l’algèbre.

Ce qui compte est ce qui est absent : pas de sorryAx (aucun trou), pas d’axiome sur mesure (rien n’est admis qui ne soit dans le standard). Autrement dit : chaque preuve du lake se déplie, en principe, jusqu’à ces trois axiomes et aux règles de la logique. C’est ce que « la preuve ne triche pas » signifie mécaniquement — et c’est pourquoi on l’affiche après la cellule qui la produit : la sortie est la preuve, ce paragraphe en est la lecture.

11. Exercices

Cinq exercices pour manipuler les énoncés du lake, du décommentage guidé à la micro-preuve. Ce sont des stubs volontaires (convention C.1 : pass, pas d’erreur) : le notebook s’exécute de bout en bout, à vous de décommenter et de compléter. Les trois premiers sont des explorations guidées du lake par #check ; les deux derniers demandent d’écrire une (toute petite) preuve en Lean — les indices donnent les tactiques.

-- Exercice 1 : verifier que la symetrie d'une equivalence est involutive
-- (indice : la declaration existe dans le namespace Equivalences)
-- #check Grothendieck.Equivalences.equivalence_symm_symm

-- Exercice 2 : trouver la declaration de la topologie canonique
-- (indice : elle s'appelle canonical_is_subcanonical)
-- #check Grothendieck.canonical_is_subcanonical

-- Exercice 3 : quel enonce relie H0 aux sections globales ?
-- #check Grothendieck.SheafCohomology.H0_equiv_global_sections

-- Exercice 4 : micro-preuve — la triviale est bien une topologie
-- (indice : trivial_le_discrete existe deja ; cherchez l'ordre)
-- example : True := trivial  -- TODO etudiant : remplacez trivial par une preuve de trivial_le_discrete

-- Exercice 5 : micro-preuve — composer deux equivalences
-- (indice : equivalence_trans ; tactique exact)
-- example : True := trivial  -- TODO etudiant : utilisez equivalence_trans pour prouver une transitivity

-- Le notebook reste executable : les stubs ne levent aucune erreur (C.1)
example : True := trivial

-- Exercice 1 : verifier que la symetrie d'une equivalence est involutive

-- (indice : la declaration existe dans le namespace Equivalences)

-- #check Grothendieck.Equivalences.equivalence_symm_symm

-- Exercice 2 : trouver la declaration de la topologie canonique

-- (indice : elle s'appelle canonical_is_subcanonical)

-- #check Grothendieck.canonical_is_subcanonical

-- Exercice 3 : quel enonce relie H0 aux sections globales ?

-- #check Grothendieck.SheafCohomology.H0_equiv_global_sections

-- Exercice 4 : micro-preuve — la triviale est bien une topologie

-- (indice : trivial_le_discrete existe deja ; cherchez l'ordre)

-- example : True := trivial  -- TODO etudiant : remplacez trivial par une preuve de trivial_le_discrete

-- Exercice 5 : micro-preuve — composer deux equivalences

-- (indice : equivalence_trans ; tactique exact)

-- example : True := trivial  -- TODO etudiant : utilisez equivalence_trans pour prouver une transitivity

-- Le notebook reste executable : les stubs ne levent aucune erreur (C.1)

example : True := trivial

--% env 10

Raw input

{"cmd": "-- Exercice 1 : verifier que la symetrie d'une equivalence est involutive\n-- (indice : la declaration existe dans le namespace Equivalences)\n-- #check Grothendieck.Equivalences.equivalence_symm_symm\n\n-- Exercice 2 : trouver la declaration de la topologie canonique\n-- (indice : elle s'appelle canonical_is_subcanonical)\n-- #check Grothendieck.canonical_is_subcanonical\n\n-- Exercice 3 : quel enonce relie H0 aux sections globales ?\n-- #check Grothendieck.SheafCohomology.H0_equiv_global_sections\n\n-- Exercice 4 : micro-preuve \u2014 la triviale est bien une topologie\n-- (indice : trivial_le_discrete existe deja ; cherchez l'ordre)\n-- example : True := trivial  -- TODO etudiant : remplacez trivial par une preuve de trivial_le_discrete\n\n-- Exercice 5 : micro-preuve \u2014 composer deux equivalences\n-- (indice : equivalence_trans ; tactique exact)\n-- example : True := trivial  -- TODO etudiant : utilisez equivalence_trans pour prouver une transitivity\n\n-- Le notebook reste executable : les stubs ne levent aucune erreur (C.1)\nexample : True := trivial", "env": 9}

Raw output

{"env": 10}

Annexe — SheafCondition : le coeur egaliseur rendu visible (#11703)

Le scan de visibilite du lake (scan_lake_notebook_visibility.py) comptait SheafCondition.lean parmi les modules invisibles : ses trois enonces n’etaient cites nulle part dans ce compagnon. C’est pourtant la Partie 63 du lake, et son sujet en est le coeur conceptuel : la condition de faisceau exprimee comme un diagramme produit-egaliseur. Pour tout crible couvrant S ∈ J X, un prefaisceau P est un faisceau si le diagramme de restriction

P(X)  →  ∏ᵢ P(U_i)  ⇉  ∏ᵢⱼ P(U_i ×_X U_j)

est un egaliseur : une section sur X est exactement une famille de sections locales deux a deux compatibles sur les produits fibres. Le module enregistre trois ponts derives de Mathlib (Stacks 00VM / 00VL) :

sheaf_iff_equalizer_sieve — forme cribles : Presieve.IsSheaf J P si et seulement si chaque fork de restriction w P S est un diagramme egaliseur ;
sheaf_iff_equalizer_arrows — forme familles d’arrows sous HasPullbacks C : la meme assertion pour une famille couvrante π : X i ⟶ B ;
sheaf_pretopology_iff — forme pretopologie : verifier la condition sur chaque famille couvrante d’une base de couvertures suffit.

-- SheafCondition (Partie 63) : les trois ponts produit-egaliseur du lake,
-- module invisible du scan de visibilite (#11703) -- voici ses enonces executes.
#check @Grothendieck.sheaf_iff_equalizer_sieve
#check @Grothendieck.sheaf_iff_equalizer_arrows
#check @Grothendieck.sheaf_pretopology_iff

-- Integrite (meme protocole que la section 10) : aucun pont ne depend de sorryAx
#print axioms Grothendieck.sheaf_iff_equalizer_sieve
#print axioms Grothendieck.sheaf_iff_equalizer_arrows
#print axioms Grothendieck.sheaf_pretopology_iff

-- SheafCondition (Partie 63) : les trois ponts produit-egaliseur du lake,

-- module invisible du scan de visibilite (#11703) -- voici ses enonces executes.

#check @Grothendieck.sheaf_iff_equalizer_sieve @Grothendieck.sheaf_iff_equalizer_sieve : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type (max u_2 u_1))),
  CategoryTheory.Presieve.IsSheaf J P ↔
    ∀ ⦃X : C⦄,
      ∀ S ∈ J X,
        Nonempty
          (CategoryTheory.Limits.IsLimit
            (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap P S.arrows) ⋯))

#check @Grothendieck.sheaf_iff_equalizer_arrows @Grothendieck.sheaf_iff_equalizer_arrows : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (P : CategoryTheory.Functor Cᵒᵖ (Type (max u_2 u_1))) [inst_1 : CategoryTheory.Limits.HasPullbacks C] {B : C}
  {I : Type (max u_2 u_1)} (X : I → C) (π : (i : I) → X i ⟶ B),
  CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔
    Nonempty
      (CategoryTheory.Limits.IsLimit
        (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π) ⋯))

#check @Grothendieck.sheaf_pretopology_iff @Grothendieck.sheaf_pretopology_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (P : CategoryTheory.Functor Cᵒᵖ (Type (max u_2 u_1))) [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (K : CategoryTheory.Pretopology C),
  CategoryTheory.Presieve.IsSheaf K.toGrothendieck P ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R

-- Integrite (meme protocole que la section 10) : aucun pont ne depend de sorryAx

#print axioms Grothendieck.sheaf_iff_equalizer_sieve 'Grothendieck.sheaf_iff_equalizer_sieve' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms Grothendieck.sheaf_iff_equalizer_arrows 'Grothendieck.sheaf_iff_equalizer_arrows' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms Grothendieck.sheaf_pretopology_iff 'Grothendieck.sheaf_pretopology_iff' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 11

Raw input

{"cmd": "-- SheafCondition (Partie 63) : les trois ponts produit-egaliseur du lake,\n-- module invisible du scan de visibilite (#11703) -- voici ses enonces executes.\n#check @Grothendieck.sheaf_iff_equalizer_sieve\n#check @Grothendieck.sheaf_iff_equalizer_arrows\n#check @Grothendieck.sheaf_pretopology_iff\n\n-- Integrite (meme protocole que la section 10) : aucun pont ne depend de sorryAx\n#print axioms Grothendieck.sheaf_iff_equalizer_sieve\n#print axioms Grothendieck.sheaf_iff_equalizer_arrows\n#print axioms Grothendieck.sheaf_pretopology_iff\n", "env": 10}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@Grothendieck.sheaf_iff_equalizer_sieve : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]\n  (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type (max u_2 u_1))),\n  CategoryTheory.Presieve.IsSheaf J P ↔\n    ∀ ⦃X : C⦄,\n      ∀ S ∈ J X,\n        Nonempty\n          (CategoryTheory.Limits.IsLimit\n            (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap P S.arrows) ⋯))"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@Grothendieck.sheaf_iff_equalizer_arrows : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]\n  (P : CategoryTheory.Functor Cᵒᵖ (Type (max u_2 u_1))) [inst_1 : CategoryTheory.Limits.HasPullbacks C] {B : C}\n  {I : Type (max u_2 u_1)} (X : I → C) (π : (i : I) → X i ⟶ B),\n  CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔\n    Nonempty\n      (CategoryTheory.Limits.IsLimit\n        (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π) ⋯))"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@Grothendieck.sheaf_pretopology_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]\n  (P : CategoryTheory.Functor Cᵒᵖ (Type (max u_2 u_1))) [inst_1 : CategoryTheory.Limits.HasPullbacks C]\n  (K : CategoryTheory.Pretopology C),\n  CategoryTheory.Presieve.IsSheaf K.toGrothendieck P ↔\n    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "'Grothendieck.sheaf_iff_equalizer_sieve' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "'Grothendieck.sheaf_iff_equalizer_arrows' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "'Grothendieck.sheaf_pretopology_iff' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 11}

Lecture de la sortie

Les #check affichent les signatures. Les deux premiers ponts sont des équivalences vers Nonempty (IsLimit ...) : être un faisceau, ce n’est pas seulement que le fork de restriction commute, c’est qu’il soit un égaliseur — une limite. Le troisième pont remplace « pour tous les cribles de la topologie » par « pour chaque famille couvrante de la prétopologie » : c’est le levier opérationnel, on vérifie la condition sur une base plutôt que sur tous les cribles.

Les #print axioms répondent [propext, Classical.choice, Quot.sound] — les axiomes standards de Lean, même protocole que la section 10 : aucun des ponts ne dépend de sorryAx. Le module SheafCondition.lean est désormais visible depuis ce compagnon. Après l’enrichissement de ces deux annexes, la mesure fraîche laisse encore des modules invisibles : le lake a gagné des modules depuis, et l’annexe finale en retire plusieurs (dont Spaces.lean).

Annexe — Du crible fermé à la faisceautisation Plus

Des modules voisins rendent explicite une même chaîne de construction. Dans LawvereTierney.lean, un opérateur de Lawvere–Tierney ferme les cribles de façon extensive, idempotente, monotone et compatible au changement de base. TopologyDictionary.lean traduit ensuite une topologie de Grothendieck en un tel opérateur et reconstruit la topologie initiale : la donnée des cribles couvrants et celle de leur clôture sont deux présentations équivalentes. Enfin, PlusConstruction.lean transporte cette logique vers les préfaisceaux : la transformation toPlus est naturelle, son itération mène au point fixe des faisceaux, et plusLift_unique_field exprime la propriété universelle de la factorisation vers un faisceau.

La cellule suivante interroge les modules à travers l’import racine déjà chargé. Les paramètres implicites affichés par #check @... rendent visibles les hypothèses catégoriques ; les #print axioms contrôlent l’intégrité d’un théorème pivot par module.

-- Lawvere–Tierney : fermeture extensive, idempotente et monotone des cribles
#check @Grothendieck.LawvereTierney.lawvereTierneyDiscrete
#check @Grothendieck.LawvereTierney.j_monotone
#check @Grothendieck.LawvereTierney.closure_isClosed

-- Dictionnaire : topologie de Grothendieck et opérateur de Lawvere–Tierney
#check @Grothendieck.TopologyDictionary.grothendieckToLawvereTierney
#check @Grothendieck.TopologyDictionary.lawvereTierneyToGrothendieck_comp_grothendieckToLawvereTierney
#check @Grothendieck.TopologyDictionary.grothendieckToLawvereTierney_comp_lawvereTierneyToGrothendieck_closure

-- Construction Plus : naturalité, itération et propriété universelle
#check @Grothendieck.toPlus_naturality_field
#check @Grothendieck.plusMap_toPlus_field
#check @Grothendieck.plusLift_unique_field

#print axioms Grothendieck.LawvereTierney.j_monotone
#print axioms Grothendieck.TopologyDictionary.lawvereTierneyToGrothendieck_comp_grothendieckToLawvereTierney
#print axioms Grothendieck.plusLift_unique_field

Lecture de la sortie

Le premier groupe expose l’opérateur de clôture sur les cribles. La signature de j_monotone dit que l’inclusion S ≤ T est préservée par la clôture, tandis que closure_isClosed matérialise l’idempotence : fermer un crible produit déjà un point fixe.

Le deuxième groupe donne le dictionnaire bidirectionnel. Le premier théorème de composition reconstruit exactement la topologie J; le second reconstruit la fonction de clôture de j. L’asymétrie des conclusions est informative : l’égalité de structures suffit côté topologies, tandis que le retour côté Lawvere–Tierney est formulé sur le champ closure qui porte la donnée utile.

Le troisième groupe affiche les hypothèses de limites et colimites nécessaires à la construction Plus. toPlus_naturality_field contrôle la naturalité, plusMap_toPlus_field relie les deux itérations, et plusLift_unique_field exprime l’unicité de toute factorisation de P ⟶ Q par toPlus P lorsque Q est déjà un faisceau.

Les trois sorties #print axioms ne mentionnent que les axiomes standards propext, Classical.choice et Quot.sound. En particulier, aucune ne contient sorryAx : les trois maillons observés sont bien des déclarations compilées, pas des énoncés admis dans le notebook.

Annexe — Les tiges (stalks) : du germe au recollement (#11703)

Des modules voisins déclarent la théorie ponctuelle du lake — les tiges (stalk) et leurs germes — et n’étaient cités nulle part dans ce compagnon : le scan de visibilité les comptait parmi ses modules noirs. Certains ne sont atteignables depuis aucun autre module du lake, pas même depuis l’agrégateur racine Grothendieck.lean, qui importe StalkGluing mais ni Stalks ni StalkPoints : la cellule d’import de la section 1 les charge donc explicitement, seule façon de les rendre lisibles ici. La cellule suivante interroge leurs déclarations.

Stalks.lean (Partie 72) — la tige du préfaisceau représentable, en deux cas disjoints. unique_stalk_yoneda traite le cas intérieur : pour x ∈ U, la tige de yoneda.obj U est un singleton, dont l’unique élément est le germe de l’identité de U. isEmpty_stalk_yoneda traite le cas extérieur : pour x ∉ U, la même tige est vide — tout germe proviendrait d’une flèche W ⟶ U au-dessus d’un voisinage de x, qui forcerait x ∈ U. nonempty_stalk_yoneda_iff joint les deux en une équivalence : la tige est habitée exactement aux points de U.
StalkSeparated.lean (Partie 74) — les tiges détectent l’égalité des sections. eq_of_germ_eq_of_isSeparated conclut s = t des seules égalités de germes en tout point de U pour un préfaisceau séparé ; eq_of_germ_eq_of_isSheaf fait de même pour un faisceau de types sans exiger d’hypothèse de limite, là où le section_ext de Mathlib demande [HasLimits C] et compagnie. injective_germ_family_of_isSeparated en donne la forme combinatoire : une section est déterminée par sa famille de germes.
StalkGluing.lean (Partie 75) — le recollement des familles de germes. Une famille est localement représentable (GermFamily.IsLocallyRepresentable) si chaque point de U admet un voisinage muni d’une section la réalisant — condition entièrement locale, qui ne suppose aucune section sur U. existsUnique_section_of_isLocallyRepresentable établit que toute famille localement représentable d’un faisceau de types provient d’une unique section de U, et surjective_germ_family_to_locallyRepresentable en donne la lecture en surjectivité sur le sous-type des familles localement représentables.
StalkPoints.lean (Partie 73) — la tige vue comme fibre du point du site. opensPoint construit le point du site des ouverts associé à x, fiberToStalk et stalkToFiber les deux cônes de colimite qui le relient à la tige topologique, et stalkFiberIso l’iso canonique entre fibre et tige — précisément l’énoncé que Mathlib.Topology.Sheaves.Points laisse en TODO. stalkFiberIso_naturality en contrôle la naturalité.

-- Tiges (stalks) : les 25 declarations des quatre modules Stalk* du lake,
-- modules invisibles du scan de visibilite (#11703) -- voici leurs enonces.

-- Stalks (Partie 72) : la tige du representable, cas interieur et exterieur
#check @Grothendieck.unique_stalk_yoneda
#check @Grothendieck.isEmpty_stalk_yoneda
#check @Grothendieck.nonempty_stalk_yoneda_iff

-- StalkSeparated (Partie 74) : les tiges detectent l'egalite des sections
#check @Grothendieck.eq_of_germ_eq_of_isSeparated
#check @Grothendieck.eq_of_germ_eq_of_isSheaf
#check @Grothendieck.injective_germ_family_of_isSeparated

-- StalkGluing (Partie 75) : les familles de germes et leur recollement
#check @Grothendieck.GermFamily
#check @Grothendieck.GermFamily.IsLocallyRepresentable
#check @Grothendieck.germFamily_isLocallyRepresentable
#check @Grothendieck.existsUnique_gluing'_of_isSheaf
#check @Grothendieck.existsUnique_section_of_isLocallyRepresentable
#check @Grothendieck.surjective_germ_family_to_locallyRepresentable

-- StalkPoints (Partie 73) : la tige comme fibre du point du site
#check @Grothendieck.opensPoint
#check @Grothendieck.mem_of_fiber
#check @Grothendieck.fiberElem
#check @Grothendieck.fiberToStalkCocone
#check @Grothendieck.fiberToStalk
#check @Grothendieck.stalkToFiberCocone
#check @Grothendieck.stalkToFiber
#check @Grothendieck.toPresheafFiber_fiberToStalk
#check @Grothendieck.germ_stalkToFiber
#check @Grothendieck.stalkToFiber_comp_fiberToStalk
#check @Grothendieck.fiberToStalk_comp_stalkToFiber
#check @Grothendieck.stalkFiberIso
#check @Grothendieck.stalkFiberIso_naturality

-- Integrite (meme protocole que la section 10) : un pivot par module, aucun
-- ne doit dependre de sorryAx
#print axioms Grothendieck.nonempty_stalk_yoneda_iff
#print axioms Grothendieck.eq_of_germ_eq_of_isSheaf
#print axioms Grothendieck.existsUnique_section_of_isLocallyRepresentable
#print axioms Grothendieck.stalkFiberIso_naturality

Lecture de la sortie

Le premier groupe expose la paire intérieure / extérieure sur la tige du représentable. unique_stalk_yoneda rend un Unique (stalk (yoneda.obj U) x) sous l’hypothèse x ∈ U : la tige n’a qu’un seul élément, le germe de l’identité de U. isEmpty_stalk_yoneda porte l’hypothèse opposée x ∉ U et conclut IsEmpty du même type. nonempty_stalk_yoneda_iff referme les deux en une équivalence Nonempty (stalk …) ↔︎ x ∈ U : la tige du représentable détecte l’appartenance du point.

Le groupe StalkSeparated montre la forme des énoncés de détection. Les deux premiers prennent une famille de germes indexée par les points de U, l’égalité des germes en chaque point, et concluent s = t ; le second le fait sous l’hypothèse de faisceau plutôt que de séparabilité, sans ajouter d’hypothèse de limite. Le troisième affiche le type Function.Injective de l’application qui envoie une section sur sa famille de germes.

Le groupe StalkGluing expose l’aller-retour section ↔︎ famille de germes. germFamily_isLocallyRepresentable donne le sens direct — la famille des germes d’une section est localement représentable — et existsUnique_section_of_isLocallyRepresentable la réciproque, sous forme d’un ∃! qui porte à la fois l’existence et l’unicité. surjective_germ_family_to_locallyRepresentable en est la reformulation en surjectivité, le type de l’application laissant voir que le but est le sous-type des familles localement représentables.

Le groupe StalkPoints affiche la construction du point du site puis les deux cônes de colimite — fiberToStalk des germes vers la fibre, stalkToFiber en sens inverse — et stalkFiberIso qui les compose en un iso. Ses paramètres implicites laissent voir que l’énoncé est posé pour un préfaisceau F sur un espace T arbitraires, sans hypothèse de faisceau : l’iso est une propriété de la construction, pas de la condition de recollement. stalkFiberIso_naturality ajoute la naturalité en F.

Les #print axioms répondent [propext, Classical.choice, Quot.sound] — les axiomes standards de Lean, même protocole que la section 10 : aucun des pivots ne dépend de sorryAx. La mesure fraîche du scan réduit encore le nombre de modules invisibles du lake grothendieck, et le nombre de déclarations distinctes citées continue de croître. Les modules Stalk* sortent du noir, et Spaces.lean avec eux : opensTopology, qu’il déclare, apparaît dans le type rendu de opensPoint et des lemmes de séparation — citer ces énoncés cite aussi le sien.

Annexe — Des ouverts au préfaisceau gratte-ciel (#11703)

Cette annexe relie quatre modules qui forment une même chaîne topologique. SpacesMathlib identifie le site des ouverts construit dans le lake à celui de Mathlib. SpacesSubcanonical montre ensuite que les représentables y sont des faisceaux. StalkCharacterization reformule la condition de faisceau par séparation et recollement des germes. Enfin, Skyscraper applique ce vocabulaire à un préfaisceau concentré autour d’un point.

Les signatures ci-dessous sont vérifiées par Lean dans le lake réel. Elles rendent visibles les propriétés structurantes plutôt que les détails de leurs preuves.

-- SpacesMathlib : le site construit dans le lake coïncide avec celui de Mathlib
#check @Grothendieck.opensTopology_eq
#check @Grothendieck.isSheaf_opensTopology_iff
#check @Grothendieck.coversTop_opensTopology_iff

-- SpacesSubcanonical : tout représentable sur le site des ouverts est un faisceau
#check @Grothendieck.isSheaf_yoneda_opensTopology
#check @Grothendieck.opensTopology_subcanonical

-- StalkCharacterization : séparation et recollement se lisent sur les germes
#check @Grothendieck.GermSeparated
#check @Grothendieck.GermGluing
#check @Grothendieck.germ_eq_of_isCompatible
#check @Grothendieck.isSheaf_iff_germSeparated_and_germGluing

-- Skyscraper : support et dichotomie des tiges autour du point choisi
#check @Grothendieck.Contenu.skyscraper
#check @Grothendieck.Contenu.stalkIsoOfMemClosure
#check @Grothendieck.Contenu.stalkIsoOfNotMemClosure
#check @Grothendieck.Contenu.support_skyscraper
#check @Grothendieck.Contenu.support_skyscraper_of_closed
#check @Grothendieck.Contenu.stalk_dichotomy

-- Les résultats pivots restent auditables par le noyau Lean
#print axioms Grothendieck.opensTopology_subcanonical
#print axioms Grothendieck.isSheaf_iff_germSeparated_and_germGluing
#print axioms Grothendieck.Contenu.support_skyscraper

Lecture du résultat

Le premier groupe de signatures établit un pont sans couche de traduction : la topologie des ouverts du lake est celle de Mathlib, puis sa sous-canonicité autorise Yoneda à produire des faisceaux. La caractérisation par les germes sépare ensuite les deux obligations d’un faisceau : l’unicité locale (GermSeparated) et l’existence d’un recollement (GermGluing).

Le gratte-ciel rend cette abstraction géométrique. Sa tige est isomorphe à la valeur choisie dans l’adhérence du point et terminale hors de cette adhérence. Sous l’hypothèse que la valeur n’est pas terminale, support_skyscraper identifie donc exactement le support à cette adhérence. Les commandes #print axioms permettent enfin de contrôler les dépendances logiques des trois résultats pivots.

Exercice — retrouver la concentration au point fermé

Objectif. Identifier le corollaire qui réduit le support du préfaisceau gratte-ciel au singleton du point lorsque celui-ci est fermé.

Repérez la déclaration dont le nom prolonge support_skyscraper.
Comparez son hypothèse de fermeture avec celle du théorème général.
Décommentez le #check, puis ajoutez sous le message exécutable une micro-preuve qui applique ce corollaire dans un contexte de votre choix.

-- Exercice : retrouver le corollaire pour un point ferme
-- #check Grothendieck.Contenu.support_skyscraper_of_closed

-- TODO etudiant : instanciez le corollaire avec un espace, un point et une valeur adaptes.
-- Indice : partez de `support_skyscraper`, puis utilisez `IsClosed.closure_eq`.

-- Le stub reste executable de bout en bout (C.1) sans pre-remplir une preuve.
#eval "Exercice a completer : instancier le corollaire pour un point ferme"

-- Exercice : retrouver le corollaire pour un point ferme

-- #check Grothendieck.Contenu.support_skyscraper_of_closed

-- TODO etudiant : instanciez le corollaire avec un espace, un point et une valeur adaptes.

-- Indice : partez de `support_skyscraper`, puis utilisez `IsClosed.closure_eq`.

-- Le stub reste executable de bout en bout (C.1) sans pre-remplir une preuve.

#eval "Exercice a completer : instancier le corollaire pour un point ferme" "Exercice a completer : instancier le corollaire pour un point ferme"

--% env 15

Raw input

{"cmd": "-- Exercice : retrouver le corollaire pour un point ferme\n-- #check Grothendieck.Contenu.support_skyscraper_of_closed\n\n-- TODO etudiant : instanciez le corollaire avec un espace, un point et une valeur adaptes.\n-- Indice : partez de `support_skyscraper`, puis utilisez `IsClosed.closure_eq`.\n\n-- Le stub reste executable de bout en bout (C.1) sans pre-remplir une preuve.\n#eval \"Exercice a completer : instancier le corollaire pour un point ferme\"", "env": 14}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 5},
   "data":
   "\"Exercice a completer : instancier le corollaire pour un point ferme\""}],
 "env": 15}

Annexe — Faisceaux flasques et résolution de Godement (#11703)

Huit modules du lake déclarent la théorie flasque du corpus — les cinq modules Flasque* (définition, exactitude, quotients, rétracts, stabilité) et les trois Godement* (construction, fonctorialité, monomorphismes) — et étaient les géants noirs du scan de visibilité : plus aucun autre groupe de modules du lake n’en comptait autant d’invisibles d’un seul tenant (16 noirs restants sur 83, dont ces 8). Cette annexe les rend visibles dans le fil du compagnon.

Le récit mathématique. Un préfaisceau est flasque (« flabby ») quand toute section sur un ouvert s’étend à tout l’espace — l’obstruction au recollement y est nulle par construction. La classe est remarquablement stable : invariante par isomorphisme, par rétract, transmise aux quotients d’une suite exacte courte flasque-flasque, et aux produits. C’est la stabilité qui paie : dans une suite exacte courte de faisceaux abélians à terme gauche flasque, le foncteur sections globales la préserve exacte — le flasque est acyclique. Le théorème de Godement (Tôhoku, II) en tire la résolution canonique : tout faisceau se plonge dans un faisceau flasque construit section par section (godementSection : germes à gauche), le plongement est fonctoriel et additif, et le foncteur préserve les monomorphismes — d’où la résolution flasque universelle qui définit la cohomologie des faisceaux.

-- Faisceaux flasques et resolution de Godement : les declarations des
-- huit modules Flasque*/Godement* du lake, noirs du scan de visibilite
-- (#11703) -- voici leurs enonces. Les huit familles sont chargees dans
-- la session par le preambule d'imports de la premiere cellule : cinq
-- par l'umbrela `import Grothendieck`, trois explicitement (le REPL
-- n'accepte les imports qu'en tout debut de session).

-- Flasque : la definition par cribles, et ses premiers ponts
#check @Grothendieck.IsFlasqueSieves
#check @Grothendieck.isFlasqueSieves_iff
#check @Grothendieck.nonempty_obj_of_isFlasqueSieves
#check @Grothendieck.isSheaf_of_isFlasqueSieves_of_isSeparated
#check @Grothendieck.isFlasqueSieves_const_of_subsingleton
#check @Grothendieck.pushforward_isFlasque_bridge
#check @Grothendieck.isFlasque_skyscraper_bridge

-- FlasqueExact : l'acyclicite -- amalgamation sans obstruction
#check @Grothendieck.exists_isAmalgamation_of_sieveTop
#check @Grothendieck.exists_lift_of_isFlasqueSieves_of_mono
#check @Grothendieck.epi_of_shortExact_of_isFlasqueSieves

-- FlasqueQuotient : stabilite par quotient d'une suite exacte flasque-flasque
#check @Grothendieck.isFlasque_of_isFlasqueSieves
#check @Grothendieck.isFlasqueSieves_of_isFlasque_of_isSheaf
#check @Grothendieck.isFlasqueSieves_of_shortExact_of_isFlasque₁₂

-- FlasqueRetract : la classe est stable par retract (et donc par iso)
#check @Grothendieck.isFlasqueSieves_of_retract
#check @Grothendieck.isFlasqueSieves_of_retract'
#check @Grothendieck.isFlasqueSieves_of_iso'
#check @Grothendieck.isFlasqueSieves_of_retract_addCommGrp

-- FlasqueStability : produits, isomorphismes, et l'echelle cohomologique
#check @Grothendieck.isFlasqueSieves_of_iso
#check @Grothendieck.isFlasqueSieves_pi
#check @Grothendieck.subsingleton_H_succ_of_flasque_of_injective

-- Godement : la construction section par section, flasque par construction
#check @Grothendieck.godementSection
#check @Grothendieck.godementObj
#check @Grothendieck.godementMap
#check @Grothendieck.godementPresheaf
#check @Grothendieck.godementExtend
#check @Grothendieck.toGodement
#check @Grothendieck.isFlasque_godementPresheaf
#check @Grothendieck.isSheaf_godementPresheaf
#check @Grothendieck.injective_toGodement_of_isSheaf

-- GodementFunctor : le plongement est fonctoriel et additif
#check @Grothendieck.godementHomApp
#check @Grothendieck.godementMapHom
#check @Grothendieck.godementFunctor
#check @Grothendieck.toGodementNatTrans
#check @Grothendieck.godementMapHom_id
#check @Grothendieck.godementMapHom_comp
#check @Grothendieck.toGodement_naturality

-- GodementMono : le foncteur preserve les monomorphismes
#check @Grothendieck.injective_app_of_mono
#check @Grothendieck.godementHomApp_injective
#check @Grothendieck.godementMapHom_mono
#check @Grothendieck.godementFunctor_preservesMonomorphisms

Lecture de la sortie

Le premier groupe fixe la définition : IsFlasqueSieves est une classe de propositions sur un préfaisceau de cribles — toute section sur un crible s’amalgame sur le crible maximal — et isFlasqueSieves_iff en donne la caractérisation. Les deux « ponts » relient cette définition générale aux notions déjà visibles du compagnon : pushforward_isFlasque_bridge (l’image directe d’un flasque reste flasque) et isFlasque_skyscraper_bridge (le gratte-ciel de l’annexe précédente est flasque — il vit au-dessus d’un point, rien ne peut l’y gêner).

Le groupe exactitude est le théorème qui justifie l’investissement : exists_isAmalgamation_of_sieveTop dit que l’amalgamation sur le crible maximal existe toujours — l’obstruction au recollement est littéralement nulle — et epi_of_shortExact_of_isFlasqueSieves en conclut que dans une suite exacte courte 0 → F' → F → F'' → 0 de faisceaux abélians où F' est flasque, la flèche sur les sections globales est épique : le foncteur Γ préserve l’exactitude. C’est l’acyclicité. subsingleton_H_succ_of_flasque_of_injective en est l’échelle cohomologique : au-delà du degré 0, les groupes d’extension d’un flasque s’effondrent.

Les groupes stabilité sont la plomberie catégorie-théorique : la classe flasque passe aux quotients (FlasqueQuotient), aux rétracts (FlasqueRetract — un rétract d’un flasque est flasque, donc un isomorphe aussi) et aux produits (isFlasqueSieves_pi).

Les trois groupes Godement construisent la résolution : godementSection envoie un ouvert U sur la somme des germes au-dessus de ses points — assez de places pour étendre n’importe quelle section — et isFlasque_godementPresheaf prouve que le préfaisceau obtenu est flasque par construction : c’est le cœur du théorème II de Godement. toGodement plonge le faisceau de départ dans le sien (injective_toGodement_of_isSheaf), le plongement est fonctoriel et additif (GodementFunctor : godementMapHom_add-compatible via godementMapHom_id/comp, naturel via toGodement_naturality), et godementFunctor_preservesMonomorphisms garantit que la résolution s’itère sans perdre l’injectivité. La cohomologie des faisceaux — section 7 du compagnon — a ici sa résolution canonique.

Annexe — Sites, topologies et comparaisons (#11703)

Les huit derniers modules noirs du scan de visibilité forment un bloc cohérent : la hiérarchie des topologies sur les schémas (Zariski, étale, fppf), le classifieur de sous-objets Ω du topos, la condition de faisceau vue par égaliseurs et son invariance, les faisceaux pour une infinité de topologies, et le comparaison des sites par image directe continue. Cette annexe les rend visibles dans le fil du compagnon — après celle des faisceaux flasques, le lake n’a plus de module noir.

Le récit mathématique. Une topologie de Grothendieck se raffine : le Zariski voit les ouverts, l’étale voit les revêtements étales, le fppf (« fidèlement plat de présentation finie ») les voit tous — chacune contenant la précédente, à la fois comme propriétés de morphismes, comme prétopologies et comme topologies engendrées. Sur n’importe quel site, l’égaliseur de la condition de faisceau se caractérise par le couple séparé + compatible, passe aux quotients par équivalence naturelle, et se lit sur les cribles engendrés ; la faisceauté se propage aux bornes supérieures et inférieures de topologies. Le classifieur Ω — le préfaisceau des cribles, dont les valeurs caractéristiques distinguent les sous-objets — referme le chapitre topos. Et entre deux sites, l’image directe continue devient un foncteur qui respecte composition et identités, adjoint au changement de base : c’est la machinerie qui permet de comparer les faisceaux d’un site à l’autre.

-- Sites, topologies et comparaisons : les declarations des huit derniers
-- modules noirs du lake (#11703) -- tous charges par le preambule
-- d'imports de la premiere cellule.

-- Classifier : le classifieur de sous-objets, Omega = le prefaisceau des cribles
#check @Grothendieck.Classifier.truth_picks_top
#check @Grothendieck.Classifier.chi_app_mem_iff
#check @Grothendieck.Classifier.chi_app_downward_closed
#check @Grothendieck.Classifier.chi_app_eq_top_of_app

-- CoversEtaleArrow : la topologie etale sur les schemas, vue par fleches
#check @Grothendieck.CoversEtaleArrow.etale_topology_eq_pretopology
#check @Grothendieck.CoversEtaleArrow.covers_iff_etale
#check @Grothendieck.CoversEtaleArrow.covers_etale_of_cover
#check @Grothendieck.CoversEtaleArrow.zariski_covers_etale
#check @Grothendieck.CoversEtaleArrow.covers_etale_of_mem
#check @Grothendieck.CoversEtaleArrow.covers_etale_precomp
#check @Grothendieck.CoversEtaleArrow.covers_etale_id
#check @Grothendieck.CoversEtaleArrow.covers_etale_top

-- Fppf : la topologie fppf et la chaine Zariski <= etale <= fppf
#check @Grothendieck.Fppf.fppfProperty
#check @Grothendieck.Fppf.fppfPrecoverage_eq_precoverage_fppfProperty
#check @Grothendieck.Fppf.fppfPretopology
#check @Grothendieck.Fppf.fppfTopology_eq_grothendieckTopology
#check @Grothendieck.Fppf.fppfTopology_eq_toGrothendieck_fppfPretopology
#check @Grothendieck.Fppf.etale_le_fppfProperty
#check @Grothendieck.Fppf.etalePrecoverage_le_fppfPrecoverage
#check @Grothendieck.Fppf.etaleTopology_le_fppfTopology
#check @Grothendieck.Fppf.zariskiTopology_le_fppfTopology

-- LocalSurjectivitySpectrum : la surjectivite locale a travers les bornes
#check @Grothendieck.isLocallySurjective_top
#check @Grothendieck.isLocallySurjective_sup
#check @Grothendieck.isLocallySurjective_iSup
#check @Grothendieck.isLocallySurjective_bot_iff

-- SheafConditionCharacterization : la condition de faisceau par egaliseurs
#check @Grothendieck.equalizer_sheaf_condition_mono
#check @Grothendieck.equalizer_sheaf_condition_iff_separated_compatible

-- SheafConditionInvariance : invariance de la condition par equivalence
#check @Grothendieck.equalizer_sheaf_condition_iff_of_nat_equiv
#check @Grothendieck.equalizer_arrows_iff_sieve_generate

-- SheafTopologySpectrum : faisceaux et bornes de topologies
#check @Grothendieck.isSheaf_const_unit
#check @Grothendieck.isSheaf_inf
#check @Grothendieck.isSheaf_iInf

-- SitesComparison : l'image directe continue, foncteur et adjonction
#check @Grothendieck.sheafPushforwardContinuous_comp_sheafToPresheaf
#check @Grothendieck.sheafPushforwardContinuous_id
#check @Grothendieck.sheafPushforwardContinuous_comp
#check @Grothendieck.adjunction_sheafPushforwardContinuous

Lecture de la sortie

Le groupe Classifier décrit Ω vu comme classifieur : truth_picks_top dit que la flèche « vrai » choisit le crible maximal, et les trois chi_app_* gouvernent la fonction caractéristique d’un monomorphisme — appartenance, descendance, et le cas où la valeur est le maximum : c’est la mécanique qui classe les sous-préfaisceaux par des cribles.

Les groupes CoversEtaleArrow et Fppf établissent la hiérarchie des topologies : etale_topology_eq_pretopology identifie la topologie étale à celle engendrée par sa prétopologie, covers_iff_etale traduit « couvrir » en un prédicat sur les flèches, et les lemmes covers_etale_* en vérifient les axiomes (stabilité par composition precomp, identité, top). Côté fppf : fppfProperty est la propriété de morphismes, fppfPretopology la prétopologie, fppfTopology_eq_* disent que tout se recolle, et les trois _le_ mesurent la chaîne Zariski ≤ étale ≤ fppf — à chaque niveau (propriétés, prétopologies, topologies).

LocalSurjectivitySpectrum lit la surjectivité locale dans le spectre des topologies : stable par sup et iSup, caractérisée au minimum par isLocallySurjective_bot_iff. SheafConditionCharacterization donne la condition de faisceau en forme d’égaliseur — le cas mono, puis l’équivalence avec « séparé + compatible » ; SheafConditionInvariance la transporte le long d’une équivalence naturelle et la relie aux cribles engendrés (equalizer_arrows_iff_sieve_generate).

SheafTopologySpectrum montre que le faisceau constant unité est faisceau pour toute topologie et que la faisceauté passe aux inf et iInf de topologies — le spectre des topologies pour lesquelles un préfaisceau est faisceau est stable par bornes. Enfin SitesComparison compare les sites : sheafPushforwardContinuous est un foncteur (identité id, composition comp), compatible avec l’oubli vers les préfaisceaux (comp_sheafToPresheaf), et adjunction_sheafPushforwardContinuous en est l’adjonction — l’outil qui identifie les faisceaux d’un site à ceux d’un site raffiné, la pierre angulaire de toute comparaison de sites.

12. Conclusion

Le lake grothendieck_lean couvre tout le spectre — de Yoneda à la cohomologie de Čech, en passant par la forme flèche des recouvrements et le site de Zariski. Ce notebook rend visibles par leurs énoncés une large part de ces modules : chaque #check est un lemme qui compile dans Mathlib 4.

Ce que l’on a appris en chemin. Que le formalisme catégorique n’est pas du verbalisme : chaque théorème du §2 transporte des données calculables (univers, adjonctions, extensions de Kan), et la machinerie des sites (§4-5) est ce qui rend « recouvrir » une opération plutôt qu’une métaphore. Que les faisceaux (§6) sont la réponse à une question précise — quand les sections locales se recollent-elles ? — et que la cohomologie (§7) mesure quand elles ne se recollent pas : H⁰ est l’espace des sections globales, le H¹ est l’obstruction. Que la géométrie (§8) est atteinte par une chaîne d’identifications, chacune prouvée : Zariski est une topologie de Grothendieck, les fibres sont des colimites. Et que la calibration (§9) n’est pas l’annexe du lake : c’est ce qui garantit que ses définitions ne sont pas vides.

Ce que le #print axioms garantit. Les théorèmes sondés ne dépendent que des trois axiomes standards (propext, Classical.choice, Quot.sound) — ceux de la logique sous-jacente de Lean, aucun autre. Aucun sorry : rien n’est promis sans preuve. C’est la différence entre un lake qui raconte Grothendieck et un lake qui le prouve.

La mesure fraîche de visibilité liée à #11703 laisse encore des modules invisibles. Ce notebook démontre ainsi que la suite est un travail d’enrichissement, plus de déblocage.

Retour au sommet

1. Import du lake

2. Fondations categoriques

3. Categories comma, monades, monoidales

4. Cribles, topologies et generation

5. La forme fleche des recouvrements (famille Covers*)

6. Faisceaux, faisceautisation, sous-canonicalite

7. Points, images directes et cohomologie

8. Geometrie : schemas, Zariski, construction, points

9. Calibration et couverture bundlee

10. Integrite des preuves : #print axioms

Lecture de la sortie

11. Exercices

Annexe — SheafCondition : le coeur egaliseur rendu visible (#11703)

Lecture de la sortie

Annexe — Du crible fermé à la faisceautisation Plus

Lecture de la sortie

Annexe — Les tiges (stalks) : du germe au recollement (#11703)

Lecture de la sortie

Annexe — Des ouverts au préfaisceau gratte-ciel (#11703)

Lecture du résultat

Exercice — retrouver la concentration au point fermé

Annexe — Faisceaux flasques et résolution de Godement (#11703)

Lecture de la sortie

Annexe — Sites, topologies et comparaisons (#11703)

Lecture de la sortie

12. Conclusion

10. Integrite des preuves : `#print axioms`