\n",
"
-- Adjunction : une adjonction distribue sur les limites côté droit et les colimites côté gauche \n",
- "
#check Grothendieck.Adjunction.leftAdjoint_preserves_colimits Grothendieck.Adjunction.leftAdjoint_preserves_colimits. {v₁, v₂, u₁, u₂, u_1, u_2} {C : Type u₁}\n",
- " [CategoryTheory.Category. {v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category. {v₂, u₂} D]\n",
- " {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) :\n",
- " CategoryTheory.Limits.PreservesColimitsOfSize. {u_1, u_2, v₁, v₂, u₁, u₂} L \n",
- "
#check Grothendieck.Adjunction.rightAdjoint_preserves_limits Grothendieck.Adjunction.rightAdjoint_preserves_limits. {v₁, v₂, u₁, u₂, u_1, u_2} {C : Type u₁}\n",
- " [CategoryTheory.Category. {v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category. {v₂, u₂} D]\n",
- " {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) :\n",
- " CategoryTheory.Limits.PreservesLimitsOfSize. {u_1, u_2, v₂, v₁, u₂, u₁} R \n",
- "
#check Grothendieck.Adjunction.adj_toEquivalence Grothendieck.Adjunction.adj_toEquivalence. {v₁, v₂, u₁, u₂} {C : Type u₁} [CategoryTheory.Category. {v₁, u₁} C]\n",
- " {D : Type u₂} [CategoryTheory.Category. {v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}\n",
- " (h : L ⊣ R) [∀ (X : C), CategoryTheory.IsIso (h.unit.app X)] [∀ (Y : D), CategoryTheory.IsIso (h.counit.app Y)] :\n",
+ "# check Grothendieck. Adjunction. leftAdjoint_preserves_colimits Grothendieck. Adjunction. leftAdjoint_preserves_colimits. {v₁, v₂, u₁, u₂, u_1, u_2} {C : Type u₁}\n",
+ " [CategoryTheory. Category. {v₁, u₁} C] {D : Type u₂} [CategoryTheory. Category. {v₂, u₂} D]\n",
+ " {L : CategoryTheory. Functor C D} {R : CategoryTheory. Functor D C} (h : L ⊣ R) :\n",
+ " CategoryTheory. Limits. PreservesColimitsOfSize. {u_1, u_2, v₁, v₂, u₁, u₂} L # check Grothendieck. Adjunction. rightAdjoint_preserves_limits Grothendieck. Adjunction. rightAdjoint_preserves_limits. {v₁, v₂, u₁, u₂, u_1, u_2} {C : Type u₁}\n",
+ " [CategoryTheory. Category. {v₁, u₁} C] {D : Type u₂} [CategoryTheory. Category. {v₂, u₂} D]\n",
+ " {L : CategoryTheory. Functor C D} {R : CategoryTheory. Functor D C} (h : L ⊣ R) :\n",
+ " CategoryTheory. Limits. PreservesLimitsOfSize. {u_1, u_2, v₂, v₁, u₂, u₁} R # check Grothendieck. Adjunction. adj_toEquivalence Grothendieck. Adjunction. adj_toEquivalence. {v₁, v₂, u₁, u₂} {C : Type u₁} [CategoryTheory. Category. {v₁, u₁} C]\n",
+ " {D : Type u₂} [CategoryTheory. Category. {v₂, u₂} D] {L : CategoryTheory. Functor C D} {R : CategoryTheory. Functor D C}\n",
+ " (h : L ⊣ R) [∀ (X : C), CategoryTheory. IsIso (h. unit. app X)] [∀ (Y : D), CategoryTheory. IsIso (h. counit. app Y)] :\n",
" C ≌ D -- YonedaLemma : le plongement de Yoneda est plein #check Grothendieck.yoneda_equiv_apply Grothendieck.yoneda_equiv_apply. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C] {X : C}\n",
- " {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} (η : CategoryTheory.yoneda.obj X ⟶ F) :\n",
- " CategoryTheory.yonedaEquiv η = \n",
- " (CategoryTheory.ConcreteCategory.hom (η.app (Opposite.op X))) (CategoryTheory.CategoryStruct.id X) #check Grothendieck.yoneda_full Grothendieck.yoneda_full. {u_1, u_2} (C : Type u_1) [CategoryTheory.Category. {u_2, u_1} C] : CategoryTheory.yoneda.Full #check Grothendieck.representableByYoneda Grothendieck.representableByYoneda. {u_1, u_2} (C : Type u_1) [CategoryTheory.Category. {u_2, u_1} C] (Y : C) :\n",
- " (CategoryTheory.yoneda.obj Y). RepresentableBy Y # check Grothendieck. yoneda_equiv_apply Grothendieck. yoneda_equiv_apply. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C] {X : C}\n",
+ " {F : CategoryTheory. Functor Cᵒᵖ (Type u_2)} (η : CategoryTheory. yoneda. obj X ⟶ F) :\n",
+ " CategoryTheory. yonedaEquiv η = \n",
+ " (CategoryTheory. ConcreteCategory. hom (η. app (Opposite. op X))) (CategoryTheory. CategoryStruct. id X) # check Grothendieck. yoneda_full Grothendieck. yoneda_full. {u_1, u_2} (C : Type u_1) [CategoryTheory. Category. {u_2, u_1} C] : CategoryTheory. yoneda. Full # check Grothendieck. representableByYoneda Grothendieck. representableByYoneda. {u_1, u_2} (C : Type u_1) [CategoryTheory. Category. {u_2, u_1} C] (Y : C) :\n",
+ " (CategoryTheory. yoneda. obj Y). RepresentableBy Y -- Equivalences : les équivalences forment une structure symétrique et transitive #check Grothendieck.Equivalences.equivalence_symm Grothendieck.Equivalences.equivalence_symm. {v₁, v₂, u₁, u₂} {C : Type u₁} [CategoryTheory.Category. {v₁, u₁} C]\n",
- " {D : Type u₂} [CategoryTheory.Category. {v₂, u₂} D] (e : C ≌ D) : D ≌ C #check Grothendieck.Equivalences.equivalence_trans Grothendieck.Equivalences.equivalence_trans. {v₁, v₂, u₁, u₂, u_1, u_2} {C : Type u₁}\n",
- " [CategoryTheory.Category. {v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category. {v₂, u₂} D] {E : Type u_1}\n",
- " [CategoryTheory.Category. {u_2, u_1} E] (e : C ≌ D) (f : D ≌ E) : C ≌ E # check Grothendieck. Equivalences. equivalence_symm Grothendieck. Equivalences. equivalence_symm. {v₁, v₂, u₁, u₂} {C : Type u₁} [CategoryTheory. Category. {v₁, u₁} C]\n",
+ " {D : Type u₂} [CategoryTheory. Category. {v₂, u₂} D] (e : C ≌ D) : D ≌ C # check Grothendieck. Equivalences. equivalence_trans Grothendieck. Equivalences. equivalence_trans. {v₁, v₂, u₁, u₂, u_1, u_2} {C : Type u₁}\n",
+ " [CategoryTheory. Category. {v₁, u₁} C] {D : Type u₂} [CategoryTheory. Category. {v₂, u₂} D] {E : Type u_1}\n",
+ " [CategoryTheory. Category. {u_2, u_1} E] (e : C ≌ D) (f : D ≌ E) : C ≌ E -- Limits : objets limites (cônes universels) #check Grothendieck.Limits.limit_object Grothendieck.Limits.limit_object. {v, v', u, u'} {J : Type u} [CategoryTheory.Category. {v, u} J] {C : Type u'}\n",
- " [CategoryTheory.Category. {v', u'} C] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] : C #check Grothendieck.Limits.colimit_object Grothendieck.Limits.colimit_object. {v, v', u, u'} {J : Type u} [CategoryTheory.Category. {v, u} J] {C : Type u'}\n",
- " [CategoryTheory.Category. {v', u'} C] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] : C -- KanExtensions : l'extension de Kan gauche, adjoint à la précomposition #check Grothendieck.KanExtensions.kan_extension_left Grothendieck.KanExtensions.kan_extension_left. {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] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)\n",
- " [L.HasLeftKanExtension F] : CategoryTheory.Functor D H #check Grothendieck.KanExtensions.lan_functor Grothendieck.KanExtensions.lan_functor. {v₁, v₂, v₃, u₁, u₂, u₃} {C : Type u₁} [CategoryTheory.Category. {v₁, u₁} C]\n",
- " {D : Type u₂} [CategoryTheory.Category. {v₂, u₂} D] {H : Type u₃} [CategoryTheory.Category. {v₃, u₃} H]\n",
- " (L : CategoryTheory.Functor C D) [∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] :\n",
- " CategoryTheory.Functor (CategoryTheory.Functor C H) (CategoryTheory.Functor D H) # check Grothendieck. Limits. limit_object Grothendieck. Limits. limit_object. {v, v', u, u'} {J : Type u} [CategoryTheory. Category. {v, u} J] {C : Type u'}\n",
+ " [CategoryTheory. Category. {v', u'} C] (F : CategoryTheory. Functor J C) [CategoryTheory. Limits. HasLimit F] : C # check Grothendieck. Limits. colimit_object Grothendieck. Limits. colimit_object. {v, v', u, u'} {J : Type u} [CategoryTheory. Category. {v, u} J] {C : Type u'}\n",
+ " [CategoryTheory. Category. {v', u'} C] (F : CategoryTheory. Functor J C) [CategoryTheory. Limits. HasColimit F] : C -- KanExtensions : l'extension de Kan gauche, adjoint à la précomposition # check Grothendieck. KanExtensions. kan_extension_left Grothendieck. KanExtensions. kan_extension_left. {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] (L : CategoryTheory. Functor C D) (F : CategoryTheory. Functor C H)\n",
+ " [L. HasLeftKanExtension F] : CategoryTheory. Functor D H # check Grothendieck. KanExtensions. lan_functor Grothendieck. KanExtensions. lan_functor. {v₁, v₂, v₃, u₁, u₂, u₃} {C : Type u₁} [CategoryTheory. Category. {v₁, u₁} C]\n",
+ " {D : Type u₂} [CategoryTheory. Category. {v₂, u₂} D] {H : Type u₃} [CategoryTheory. Category. {v₃, u₃} H]\n",
+ " (L : CategoryTheory. Functor C D) [∀ (F : CategoryTheory. Functor C H), L. HasLeftKanExtension F] :\n",
+ " CategoryTheory. Functor (CategoryTheory. Functor C H) (CategoryTheory. Functor D H) --% env 1 \n",
"
\n",
@@ -499,10 +461,10 @@
"id": "76cff3a2",
"metadata": {
"papermill": {
- "duration": 0.002866,
- "end_time": "2026-09-07T11:09:53.001371+00:00",
+ "duration": 0.003588,
+ "end_time": "2026-09-20T09:10:44.500399+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:52.998505+00:00",
+ "start_time": "2026-09-20T09:10:44.496811+00:00",
"status": "completed"
},
"tags": []
@@ -535,16 +497,16 @@
"id": "751cd9f2",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-09-12T21:52:04.990466Z",
- "iopub.status.busy": "2026-09-12T21:52:04.990255Z",
- "iopub.status.idle": "2026-09-12T21:52:05.180348Z",
- "shell.execute_reply": "2026-09-12T21:52:05.179179Z"
+ "iopub.execute_input": "2026-09-20T09:10:44.508608Z",
+ "iopub.status.busy": "2026-09-20T09:10:44.508440Z",
+ "iopub.status.idle": "2026-09-20T09:10:44.724878Z",
+ "shell.execute_reply": "2026-09-20T09:10:44.723932Z"
},
"papermill": {
- "duration": 0.197322,
- "end_time": "2026-09-07T11:09:53.201286+00:00",
+ "duration": 0.221672,
+ "end_time": "2026-09-20T09:10:44.725482+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:53.003964+00:00",
+ "start_time": "2026-09-20T09:10:44.503810+00:00",
"status": "completed"
},
"tags": []
@@ -563,32 +525,32 @@
" \n",
" \n",
"
-- Comma : les catégories comma avec leurs deux projections \n",
- "
#check Grothendieck.Comma.fstFunctor 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 \n",
- "
#check Grothendieck.Comma.sndFunctor 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 \n",
- "
#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]\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) \n",
+ "
# check Grothendieck. Comma. fstFunctor 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 \n",
+ "
# check Grothendieck. Comma. sndFunctor 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 \n",
+ "
# 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]\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) \n",
"
-- Monads : une adjonction engendre une monade et une catégorie de Kleisli \n",
- "
#check Grothendieck.Monads.toMonad_underlying 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 \n",
- "
#check Grothendieck.Monads.kleisli_type Grothendieck.Monads.kleisli_type. {v₁, u₁} {C : Type u₁} [CategoryTheory.Category. {v₁, u₁} C]\n",
- " (T : CategoryTheory.Monad C) : Type u₁ \n",
+ "
# check Grothendieck. Monads. toMonad_underlying 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 \n",
+ "
# check Grothendieck. Monads. kleisli_type Grothendieck. Monads. kleisli_type. {v₁, u₁} {C : Type u₁} [CategoryTheory. Category. {v₁, u₁} C]\n",
+ " (T : CategoryTheory. Monad C) : Type u₁ \n",
"
-- MonoidalCategories : la cohérence monoïdale : pentagone et tressage \n",
- "
#check Grothendieck.MonoidalCategories.tensor_product Grothendieck.MonoidalCategories.tensor_product. {v, u} {C : Type u} [CategoryTheory.Category. {v, u} C]\n",
- " [CategoryTheory.MonoidalCategory C] (X Y : C) : C \n",
- "
#check Grothendieck.MonoidalCategories.braiding_iso 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 \n",
- "
#check Grothendieck.MonoidalCategories.pentagon_field Grothendieck.MonoidalCategories.pentagon_field. {v, u} {C : Type u} [CategoryTheory.Category. {v, u} C]\n",
- " [CategoryTheory.MonoidalCategoryStruct C] (Y₁ Y₂ Y₃ Y₄ : C) : Prop \n",
+ "
# check Grothendieck. MonoidalCategories. tensor_product Grothendieck. MonoidalCategories. tensor_product. {v, u} {C : Type u} [CategoryTheory. Category. {v, u} C]\n",
+ " [CategoryTheory. MonoidalCategory C] (X Y : C) : C \n",
+ "
# check Grothendieck. MonoidalCategories. braiding_iso 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 \n",
+ "
# check Grothendieck. MonoidalCategories. pentagon_field Grothendieck. MonoidalCategories. pentagon_field. {v, u} {C : Type u} [CategoryTheory. Category. {v, u} C]\n",
+ " [CategoryTheory. MonoidalCategoryStruct C] (Y₁ Y₂ Y₃ Y₄ : C) : Prop \n",
"
--% env 2 \n",
"
\n",
@@ -750,10 +712,10 @@
"id": "2b91b69d",
"metadata": {
"papermill": {
- "duration": 0.003088,
- "end_time": "2026-09-07T11:09:53.207565+00:00",
+ "duration": 0.004505,
+ "end_time": "2026-09-20T09:10:44.733946+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:53.204477+00:00",
+ "start_time": "2026-09-20T09:10:44.729441+00:00",
"status": "completed"
},
"tags": []
@@ -783,16 +745,16 @@
"id": "22f7b8b2",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-09-12T21:52:05.183973Z",
- "iopub.status.busy": "2026-09-12T21:52:05.183808Z",
- "iopub.status.idle": "2026-09-12T21:52:05.365137Z",
- "shell.execute_reply": "2026-09-12T21:52:05.363931Z"
+ "iopub.execute_input": "2026-09-20T09:10:44.742923Z",
+ "iopub.status.busy": "2026-09-20T09:10:44.742751Z",
+ "iopub.status.idle": "2026-09-20T09:10:44.973544Z",
+ "shell.execute_reply": "2026-09-20T09:10:44.972012Z"
},
"papermill": {
- "duration": 0.209339,
- "end_time": "2026-09-07T11:09:53.420007+00:00",
+ "duration": 0.237656,
+ "end_time": "2026-09-20T09:10:44.975376+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:53.210668+00:00",
+ "start_time": "2026-09-20T09:10:44.737720+00:00",
"status": "completed"
},
"tags": []
@@ -810,28 +772,28 @@
" \n",
" \n",
" \n",
- "
-- SieveGenerate : la génération d'un crible est monotone \n",
- "
#check Grothendieck.generate_monotone 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₂ \n",
+ "
-- SieveGenerate : la génération d'un crible est monotone \n",
+ "
# check Grothendieck. generate_monotone 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₂ \n",
"
-- SieveOps : la topologie triviale est la plus petite \n",
- "
#check Grothendieck.trivial_le_any 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 \n",
- "
-- SieveLattice : le pullback de cribles est une structure d'action \n",
- "
#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}\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 \n",
- "
-- TopologyLattice : l'ordre des topologies est porté par les recouvrements \n",
- "
#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}\n",
- " {J₁ J₂ : CategoryTheory.GrothendieckTopology C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X) :\n",
- " J₁ ≤ J₂ → J₁.Covers S f → J₂.Covers S f \n",
+ "
# check Grothendieck. trivial_le_any 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 \n",
+ "
-- SieveLattice : le pullback de cribles est une structure d'action \n",
+ "
# 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}\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 \n",
+ "
-- TopologyLattice : l'ordre des topologies est porté par les recouvrements \n",
+ "
# 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}\n",
+ " {J₁ J₂ : CategoryTheory. GrothendieckTopology C} (S : CategoryTheory. Sieve X) (f : Y ⟶ X) :\n",
+ " J₁ ≤ J₂ → J₁. Covers S f → J₂. Covers S f \n",
"
-- DenseTopology : dense est strictement entre triviale et discrète \n",
- "
#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] :\n",
- " CategoryTheory.GrothendieckTopology.dense ≤ CategoryTheory.GrothendieckTopology.discrete C \n",
+ "
# 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] :\n",
+ " CategoryTheory. GrothendieckTopology. dense ≤ CategoryTheory. GrothendieckTopology. discrete C \n",
"
-- CoverageGen : une coverage engendre une topologie de Grothendieck \n",
- "
#check Grothendieck.coverageToTopology 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 \n",
+ "
# check Grothendieck. coverageToTopology 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 \n",
"
--% env 3 \n",
"
\n",
@@ -967,10 +929,10 @@
"id": "65637b09",
"metadata": {
"papermill": {
- "duration": 0.003224,
- "end_time": "2026-09-07T11:09:53.426820+00:00",
+ "duration": 0.00446,
+ "end_time": "2026-09-20T09:10:44.984971+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:53.423596+00:00",
+ "start_time": "2026-09-20T09:10:44.980511+00:00",
"status": "completed"
},
"tags": []
@@ -1005,16 +967,16 @@
"id": "a7b44d56",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-09-12T21:52:05.368447Z",
- "iopub.status.busy": "2026-09-12T21:52:05.368280Z",
- "iopub.status.idle": "2026-09-12T21:52:05.588498Z",
- "shell.execute_reply": "2026-09-12T21:52:05.587514Z"
+ "iopub.execute_input": "2026-09-20T09:10:44.994332Z",
+ "iopub.status.busy": "2026-09-20T09:10:44.994151Z",
+ "iopub.status.idle": "2026-09-20T09:10:45.231478Z",
+ "shell.execute_reply": "2026-09-20T09:10:45.230434Z"
},
"papermill": {
- "duration": 0.219907,
- "end_time": "2026-09-07T11:09:53.650050+00:00",
+ "duration": 0.243083,
+ "end_time": "2026-09-20T09:10:45.232148+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:53.430143+00:00",
+ "start_time": "2026-09-20T09:10:44.989065+00:00",
"status": "completed"
},
"tags": []
@@ -1033,79 +995,79 @@
" \n",
" \n",
"
-- CoversArrow : forme flèche : recouvrir `f` équivaut à recouvrir `id` \n",
- "
#check Grothendieck.CoversArrow.covers_iff_covers_id Grothendieck.CoversArrow.covers_iff_covers_id. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C] {X Y : C}\n",
- " (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve X) (f : Y ⟶ X) :\n",
- " J.Covers S f ↔ J.Covers (CategoryTheory.Sieve.pullback f S) (CategoryTheory.CategoryStruct.id Y) \n",
+ "
# check Grothendieck. CoversArrow. covers_iff_covers_id Grothendieck. CoversArrow. covers_iff_covers_id. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C] {X Y : C}\n",
+ " (J : CategoryTheory. GrothendieckTopology C) (S : CategoryTheory. Sieve X) (f : Y ⟶ X) :\n",
+ " J. Covers S f ↔ J. Covers (CategoryTheory. Sieve. pullback f S) (CategoryTheory. CategoryStruct. id Y) \n",
"
-- CoversAtomicArrow : la topologie atomique en forme flèche \n",
- "
#check Grothendieck.CoversAtomicArrow.atomic_covering Grothendieck.CoversAtomicArrow.atomic_covering. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C]\n",
- " (hro : CategoryTheory.GrothendieckTopology.RightOreCondition C) {X : C} (S : CategoryTheory.Sieve X) :\n",
- " S ∈ (CategoryTheory.GrothendieckTopology.atomic ⋯ ) X ↔ ∃ Y f, S.arrows f \n",
- "
#check Grothendieck.CoversAtomicArrow.covers_iff_atomic Grothendieck.CoversAtomicArrow.covers_iff_atomic. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C]\n",
- " (hro : CategoryTheory.GrothendieckTopology.RightOreCondition C) {X Y : C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X) :\n",
- " (CategoryTheory.GrothendieckTopology.atomic ⋯ ). Covers S f ↔ ∃ Z g, S.arrows (CategoryTheory.CategoryStruct.comp g f) \n",
- "
-- CoversBind : l'axiome de liaison des topologies en forme flèche \n",
- "
#check Grothendieck.CoversBind.covers_bind Grothendieck.CoversBind.covers_bind. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C] {X Y : C}\n",
- " (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve X) (f : Y ⟶ X) (hS : J.Covers S f)\n",
- " (T : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S.arrows g → CategoryTheory.Sieve Z)\n",
- " (hT : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (hg : S.arrows g), J.Covers (T hg) (CategoryTheory.CategoryStruct.id Z)) :\n",
- " J.Covers (CategoryTheory.Sieve.bind S.arrows T) f \n",
+ "
# check Grothendieck. CoversAtomicArrow. atomic_covering Grothendieck. CoversAtomicArrow. atomic_covering. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C]\n",
+ " (hro : CategoryTheory. GrothendieckTopology. RightOreCondition C) {X : C} (S : CategoryTheory. Sieve X) :\n",
+ " S ∈ (CategoryTheory. GrothendieckTopology. atomic ⋯ ) X ↔ ∃ Y f, S. arrows f \n",
+ "
# check Grothendieck. CoversAtomicArrow. covers_iff_atomic Grothendieck. CoversAtomicArrow. covers_iff_atomic. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C]\n",
+ " (hro : CategoryTheory. GrothendieckTopology. RightOreCondition C) {X Y : C} (S : CategoryTheory. Sieve X) (f : Y ⟶ X) :\n",
+ " (CategoryTheory. GrothendieckTopology. atomic ⋯ ). Covers S f ↔ ∃ Z g, S. arrows (CategoryTheory. CategoryStruct. comp g f) \n",
+ "
-- CoversBind : l'axiome de liaison des topologies en forme flèche \n",
+ "
# check Grothendieck. CoversBind. covers_bind Grothendieck. CoversBind. covers_bind. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C] {X Y : C}\n",
+ " (J : CategoryTheory. GrothendieckTopology C) (S : CategoryTheory. Sieve X) (f : Y ⟶ X) (hS : J. Covers S f)\n",
+ " (T : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S. arrows g → CategoryTheory. Sieve Z)\n",
+ " (hT : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (hg : S. arrows g), J. Covers (T hg) (CategoryTheory. CategoryStruct. id Z)) :\n",
+ " J. Covers (CategoryTheory. Sieve. bind S. arrows T) f \n",
"
-- CoversLattice : structure de treillis sur les recouvrements \n",
- "
#check Grothendieck.CoversLattice.sInf_covers Grothendieck.CoversLattice.sInf_covers. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C]\n",
- " {s : Set (CategoryTheory.GrothendieckTopology C)} {X Y : C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X) :\n",
- " (sInf s). Covers S f ↔ ∀ J ∈ s, J.Covers S f \n",
+ "
# check Grothendieck. CoversLattice. sInf_covers Grothendieck. CoversLattice. sInf_covers. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C]\n",
+ " {s : Set (CategoryTheory. GrothendieckTopology C)} {X Y : C} (S : CategoryTheory. Sieve X) (f : Y ⟶ X) :\n",
+ " (sInf s). Covers S f ↔ ∀ J ∈ s, J. Covers S f \n",
"
-- CoversOrder : le recouvrement maximal est top \n",
- "
#check Grothendieck.CoversOrder.covers_top Grothendieck.CoversOrder.covers_top. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C] {X Y : C}\n",
- " (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) : J.Covers ⊤ f \n",
+ "
# check Grothendieck. CoversOrder. covers_top Grothendieck. CoversOrder. covers_top. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C] {X Y : C}\n",
+ " (J : CategoryTheory. GrothendieckTopology C) (f : Y ⟶ X) : J. Covers ⊤ f \n",
"
-- CoversPullback : stabilité par pullback des recouvrements \n",
- "
#check Grothendieck.CoversPullback.cover_pullback_covers Grothendieck.CoversPullback.cover_pullback_covers. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C]\n",
- " {X Y : C} (J : CategoryTheory.GrothendieckTopology C) (S : J.Cover X) (f : Y ⟶ X) :\n",
- " J.Covers (↑ (S.pullback f)) (CategoryTheory.CategoryStruct.id Y) \n",
+ "
# check Grothendieck. CoversPullback. cover_pullback_covers Grothendieck. CoversPullback. cover_pullback_covers. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C]\n",
+ " {X Y : C} (J : CategoryTheory. GrothendieckTopology C) (S : J. Cover X) (f : Y ⟶ X) :\n",
+ " J. Covers (↑ (S. pullback f)) (CategoryTheory. CategoryStruct. id Y) \n",
"
-- CoversPushforward : image directe des recouvrements \n",
- "
#check Grothendieck.CoversPushforward.pushforward_pullback_fixed Grothendieck.CoversPushforward.pushforward_pullback_fixed. {u_1, u_2} {C : Type u_1}\n",
- " [CategoryTheory.Category. {u_2, u_1} C] {X Y : C} {f : Y ⟶ X} [CategoryTheory.Mono f] (S : CategoryTheory.Sieve Y) :\n",
- " CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.pushforward f S) = S \n",
- "
#check Grothendieck.CoversPushforward.pullback_pushforward_fixed Grothendieck.CoversPushforward.pullback_pushforward_fixed. {u_1, u_2} {C : Type u_1}\n",
- " [CategoryTheory.Category. {u_2, u_1} C] {X Y : C} {f : Y ⟶ X} [CategoryTheory.IsSplitEpi f]\n",
- " (R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.pullback f R) = R \n",
+ "
# check Grothendieck. CoversPushforward. pushforward_pullback_fixed Grothendieck. CoversPushforward. pushforward_pullback_fixed. {u_1, u_2} {C : Type u_1}\n",
+ " [CategoryTheory. Category. {u_2, u_1} C] {X Y : C} {f : Y ⟶ X} [CategoryTheory. Mono f] (S : CategoryTheory. Sieve Y) :\n",
+ " CategoryTheory. Sieve. pullback f (CategoryTheory. Sieve. pushforward f S) = S \n",
+ "
# check Grothendieck. CoversPushforward. pullback_pushforward_fixed Grothendieck. CoversPushforward. pullback_pushforward_fixed. {u_1, u_2} {C : Type u_1}\n",
+ " [CategoryTheory. Category. {u_2, u_1} C] {X Y : C} {f : Y ⟶ X} [CategoryTheory. IsSplitEpi f]\n",
+ " (R : CategoryTheory. Sieve X) : CategoryTheory. Sieve. pushforward f (CategoryTheory. Sieve. pullback f R) = R \n",
"
-- CoversTopologies : recouvrements de la topologie dense \n",
- "
#check Grothendieck.CoversTopologies.dense_covers_iff Grothendieck.CoversTopologies.dense_covers_iff. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C]\n",
- " {X Y : C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X) :\n",
- " CategoryTheory.GrothendieckTopology.dense.Covers S f ↔ \n",
+ "# check Grothendieck. CoversTopologies. dense_covers_iff Grothendieck. CoversTopologies. dense_covers_iff. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C]\n",
+ " {X Y : C} (S : CategoryTheory. Sieve X) (f : Y ⟶ X) :\n",
+ " CategoryTheory. GrothendieckTopology. dense. Covers S f ↔ \n",
" ∀ {Z : C} (g : Z ⟶ Y),\n",
- " ∃ W h, S.arrows (CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp g f)) ∃ W h, S. arrows (CategoryTheory. CategoryStruct. comp h (CategoryTheory. CategoryStruct. comp g f)) \n",
"
-- CoversZariskiArrow : le site de Zariski en forme flèche \n",
- "
#check Grothendieck.CoversZariskiArrow.covers_iff_zariski\n",
"
-- CoversCoverageArrow : la conversion coverage → topologie en forme flèche \n",
- "
#check Grothendieck.CoversCoverageArrow.covers_iff_toGrothendieck Grothendieck.CoversCoverageArrow.covers_iff_toGrothendieck. {u, v} {C : Type u} [CategoryTheory.Category. {v, u} C]\n",
- " (K : CategoryTheory.Coverage C) {X Y : C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X) :\n",
- " K.toGrothendieck.Covers S f ↔ K.Saturate Y (CategoryTheory.Sieve.pullback f S) \n",
+ "
# check Grothendieck. CoversCoverageArrow. covers_iff_toGrothendieck Grothendieck. CoversCoverageArrow. covers_iff_toGrothendieck. {u, v} {C : Type u} [CategoryTheory. Category. {v, u} C]\n",
+ " (K : CategoryTheory. Coverage C) {X Y : C} (S : CategoryTheory. Sieve X) (f : Y ⟶ X) :\n",
+ " K. toGrothendieck. Covers S f ↔ K. Saturate Y (CategoryTheory. Sieve. pullback f S) \n",
"
-- CoversPrecoverageArrow : la conversion pré-coverage → topologie \n",
- "
#check Grothendieck.CoversPrecoverageArrow.covers_iff_toGrothendieck Grothendieck.CoversPrecoverageArrow.covers_iff_toGrothendieck. {u, v} {C : Type u} [CategoryTheory.Category. {v, u} C]\n",
- " (J : CategoryTheory.Precoverage C) {X Y : C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X) :\n",
- " J.toGrothendieck.Covers S f ↔ J.Saturate Y (CategoryTheory.Sieve.pullback f S) \n",
+ "
# check Grothendieck. CoversPrecoverageArrow. covers_iff_toGrothendieck Grothendieck. CoversPrecoverageArrow. covers_iff_toGrothendieck. {u, v} {C : Type u} [CategoryTheory. Category. {v, u} C]\n",
+ " (J : CategoryTheory. Precoverage C) {X Y : C} (S : CategoryTheory. Sieve X) (f : Y ⟶ X) :\n",
+ " J. toGrothendieck. Covers S f ↔ J. Saturate Y (CategoryTheory. Sieve. pullback f S) \n",
"
-- CoversPretopologyArrow : la conversion pré-topologie → topologie \n",
- "
#check Grothendieck.CoversPretopologyArrow.covers_toGrothendieck_of_of Grothendieck.CoversPretopologyArrow.covers_toGrothendieck_of_of. {u, v} {C : Type u} [CategoryTheory.Category. {v, u} C]\n",
- " [CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C) {X : C} {R : CategoryTheory.Presieve X}\n",
- " (hR : R ∈ K.coverings X) :\n",
- " K.toGrothendieck.Covers (CategoryTheory.Sieve.generate R) (CategoryTheory.CategoryStruct.id X) \n",
- "
-- PullbackCoversLaws : l'associativité du pullback de recouvrements \n",
- "
#check Grothendieck.PullbackCoversLaws.covers_pullback_assoc Grothendieck.PullbackCoversLaws.covers_pullback_assoc. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C]\n",
- " {W X Y Z : C} (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve Z) (f : Y ⟶ Z) (g : X ⟶ Y)\n",
+ "# check Grothendieck. CoversPretopologyArrow. covers_toGrothendieck_of_of Grothendieck. CoversPretopologyArrow. covers_toGrothendieck_of_of. {u, v} {C : Type u} [CategoryTheory. Category. {v, u} C]\n",
+ " [CategoryTheory. Limits. HasPullbacks C] (K : CategoryTheory. Pretopology C) {X : C} {R : CategoryTheory. Presieve X}\n",
+ " (hR : R ∈ K. coverings X) :\n",
+ " K. toGrothendieck. Covers (CategoryTheory. Sieve. generate R) (CategoryTheory. CategoryStruct. id X) -- PullbackCoversLaws : l'associativité du pullback de recouvrements # check Grothendieck. PullbackCoversLaws. covers_pullback_assoc Grothendieck. PullbackCoversLaws. covers_pullback_assoc. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C]\n",
+ " {W X Y Z : C} (J : CategoryTheory. GrothendieckTopology C) (S : CategoryTheory. Sieve Z) (f : Y ⟶ Z) (g : X ⟶ Y)\n",
" (h : W ⟶ X) :\n",
- " J.Covers (CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.pullback f S)) h ↔ \n",
- " J.Covers (CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp g f) S) h J. Covers (CategoryTheory. Sieve. pullback g (CategoryTheory. Sieve. pullback f S)) h ↔ \n",
+ " J. Covers (CategoryTheory. Sieve. pullback (CategoryTheory. CategoryStruct. comp g f) S) h \n",
"
-- PullbackFunctor : le foncteur pullback et ses unités \n",
- "
#check Grothendieck.PullbackFunctor.pullback_triple Grothendieck.PullbackFunctor.pullback_triple. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C]\n",
- " {X Y Z W : C} (J : CategoryTheory.GrothendieckTopology C) (S : J.Cover W) (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) :\n",
- " ((S.pullback h). pullback g). pullback f = \n",
- " S.pullback (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) \n",
+ "
# check Grothendieck. PullbackFunctor. pullback_triple Grothendieck. PullbackFunctor. pullback_triple. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C]\n",
+ " {X Y Z W : C} (J : CategoryTheory. GrothendieckTopology C) (S : J. Cover W) (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) :\n",
+ " ((S. pullback h). pullback g). pullback f = \n",
+ " S. pullback (CategoryTheory. CategoryStruct. comp f (CategoryTheory. CategoryStruct. comp g h)) \n",
"
-- PullbackFunctorLaws : les lois du foncteur pullback \n",
- "
#check Grothendieck.PullbackFunctorLaws.covers_pullback_comp Grothendieck.PullbackFunctorLaws.covers_pullback_comp. {u_1, u_2} {C : Type u_1} [CategoryTheory.Category. {u_2, u_1} C]\n",
- " {X Y Z : C} (J : CategoryTheory.GrothendieckTopology C) (f : X ⟶ Y) (g : Y ⟶ Z) (S : J.Cover Z) :\n",
- " J.Covers (↑ S) (CategoryTheory.CategoryStruct.comp f g) ↔ J.Covers (↑ (S.pullback g)) f \n",
+ "
# check Grothendieck. PullbackFunctorLaws. covers_pullback_comp Grothendieck. PullbackFunctorLaws. covers_pullback_comp. {u_1, u_2} {C : Type u_1} [CategoryTheory. Category. {u_2, u_1} C]\n",
+ " {X Y Z : C} (J : CategoryTheory. GrothendieckTopology C) (f : X ⟶ Y) (g : Y ⟶ Z) (S : J. Cover Z) :\n",
+ " J. Covers (↑ S) (CategoryTheory. CategoryStruct. comp f g) ↔ J. Covers (↑ (S. pullback g)) f \n",
"
--% env 4 \n",
"
\n",
@@ -1434,10 +1396,10 @@
"id": "182b8f69",
"metadata": {
"papermill": {
- "duration": 0.00365,
- "end_time": "2026-09-07T11:09:53.657692+00:00",
+ "duration": 0.004743,
+ "end_time": "2026-09-20T09:10:45.241674+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:53.654042+00:00",
+ "start_time": "2026-09-20T09:10:45.236931+00:00",
"status": "completed"
},
"tags": []
@@ -1471,16 +1433,16 @@
"id": "1045f4c9",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-09-12T21:52:05.607043Z",
- "iopub.status.busy": "2026-09-12T21:52:05.606833Z",
- "iopub.status.idle": "2026-09-12T21:52:05.791350Z",
- "shell.execute_reply": "2026-09-12T21:52:05.790241Z"
+ "iopub.execute_input": "2026-09-20T09:10:45.254329Z",
+ "iopub.status.busy": "2026-09-20T09:10:45.254159Z",
+ "iopub.status.idle": "2026-09-20T09:10:45.461475Z",
+ "shell.execute_reply": "2026-09-20T09:10:45.460491Z"
},
"papermill": {
- "duration": 0.202698,
- "end_time": "2026-09-07T11:09:53.863925+00:00",
+ "duration": 0.214797,
+ "end_time": "2026-09-20T09:10:45.462286+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:53.661227+00:00",
+ "start_time": "2026-09-20T09:10:45.247489+00:00",
"status": "completed"
},
"tags": []
@@ -1499,38 +1461,38 @@
" \n",
" \n",
"
-- SheafBasics : un faisceau est en particulier séparé \n",
- "
#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]\n",
- " {J : CategoryTheory.GrothendieckTopology C} {P : CategoryTheory.Functor Cᵒᵖ (Type u_2)}\n",
- " (h : CategoryTheory.Presieve.IsSheaf J P) : CategoryTheory.Presieve.IsSeparated J P \n",
- "
#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]\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 \n",
+ "
# 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]\n",
+ " {J : CategoryTheory. GrothendieckTopology C} {P : CategoryTheory. Functor Cᵒᵖ (Type u_2)}\n",
+ " (h : CategoryTheory. Presieve. IsSheaf J P) : CategoryTheory. Presieve. IsSeparated J P \n",
+ "
# 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]\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 \n",
"
-- SheafHom : le faisceau interne des homomorphismes \n",
- "
#check Grothendieck.SheafHom.sheafHom_isSheaf 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 \n",
+ "
# check Grothendieck. SheafHom. sheafHom_isSheaf 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 \n",
"
-- Sheafification : la propriété universelle de la faisceautisation \n",
- "
#check Grothendieck.sheafification_universal 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)) \n",
+ "
# check Grothendieck. sheafification_universal 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)) \n",
"
-- ConstantSheaf : un faisceau constant caractérisé par son adjonction \n",
- "
#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]\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) \n",
+ "
# 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]\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) \n",
"
-- LeftExact : la faisceautisation préserve les limites finies (exactitude à gauche) \n",
- "
#check Grothendieck.plus_preserves_finite_limits 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))) \n",
+ "
# check Grothendieck. plus_preserves_finite_limits 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))) \n",
"
-- Subcanonical : sous-canonicalité : le plongement de Yoneda est un faisceau \n",
- "
#check Grothendieck.Subcanonical.subcanonical_of_yoneda_sheaf 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 \n",
+ "
# check Grothendieck. Subcanonical. subcanonical_of_yoneda_sheaf 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 \n",
"
-- CanonicalProps : la topologie canonique est sous-canonique \n",
- "
#check Grothendieck.canonical_is_subcanonical 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 \n",
+ "
# check Grothendieck. canonical_is_subcanonical 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 \n",
"
--% env 5 \n",
"
\n",
@@ -1702,10 +1664,10 @@
"id": "997867fc",
"metadata": {
"papermill": {
- "duration": 0.00385,
- "end_time": "2026-09-07T11:09:53.871853+00:00",
+ "duration": 0.005112,
+ "end_time": "2026-09-20T09:10:45.472728+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:53.868003+00:00",
+ "start_time": "2026-09-20T09:10:45.467616+00:00",
"status": "completed"
},
"tags": []
@@ -1737,16 +1699,16 @@
"id": "69e7ba56",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-09-12T21:52:05.795637Z",
- "iopub.status.busy": "2026-09-12T21:52:05.795473Z",
- "iopub.status.idle": "2026-09-12T21:52:05.990507Z",
- "shell.execute_reply": "2026-09-12T21:52:05.989666Z"
+ "iopub.execute_input": "2026-09-20T09:10:45.486086Z",
+ "iopub.status.busy": "2026-09-20T09:10:45.485852Z",
+ "iopub.status.idle": "2026-09-20T09:10:45.765224Z",
+ "shell.execute_reply": "2026-09-20T09:10:45.764066Z"
},
"papermill": {
- "duration": 0.195327,
- "end_time": "2026-09-07T11:09:54.071296+00:00",
+ "duration": 0.287566,
+ "end_time": "2026-09-20T09:10:45.765909+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:53.875969+00:00",
+ "start_time": "2026-09-20T09:10:45.478343+00:00",
"status": "completed"
},
"tags": []
@@ -1764,40 +1726,40 @@
" \n",
" \n",
" \n",
- "
-- SitePoints : la fibre d'un point est une colimite \n",
- "
#check Grothendieck.is_colimit_presheaf_fiber 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) \n",
+ "
-- SitePoints : la fibre d'un point est une colimite \n",
+ "
# check Grothendieck. is_colimit_presheaf_fiber 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) \n",
"
-- DirectImage : le foncteur image directe \n",
- "
#check Grothendieck.DirectImage.pushforward_functor_field Grothendieck.DirectImage.pushforward_functor_field. {u} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :\n",
- " CategoryTheory.Functor X.Modules Y.Modules \n",
- "
-- ExceptionalDirect : l'image directe exceptionnelle \n",
- "
#check Grothendieck.ExceptionalDirect.exceptionalDirectImage 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) \n",
+ "
# check Grothendieck. DirectImage. pushforward_functor_field Grothendieck. DirectImage. pushforward_functor_field. {u} {X Y : AlgebraicGeometry. Scheme} (f : X ⟶ Y) :\n",
+ " CategoryTheory. Functor X. Modules Y. Modules \n",
+ "
-- ExceptionalDirect : l'image directe exceptionnelle \n",
+ "
# check Grothendieck. ExceptionalDirect. exceptionalDirectImage 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) \n",
"
-- SheafCohomology.Basic : H⁰ est la section globale \n",
- "
#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]\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)) \n",
- "
-- SheafCohomology.Cech : l'objet du complexe de Čech \n",
- "
#check Grothendieck.SheafCohomology.Cech.cechComplexObj 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 \n",
- "
-- SheafCohomology.MayerVietoris : l'exactitude de la suite de Mayer-Vietoris \n",
- "
#check Grothendieck.SheafCohomology.MayerVietoris.mv_sequence_exact 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 \n",
+ "
# 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]\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)) \n",
+ "
-- SheafCohomology.Cech : l'objet du complexe de Čech \n",
+ "
# check Grothendieck. SheafCohomology. Cech. cechComplexObj 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 \n",
+ "
-- SheafCohomology.MayerVietoris : l'exactitude de la suite de Mayer-Vietoris \n",
+ "
# check Grothendieck. SheafCohomology. MayerVietoris. mv_sequence_exact 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 \n",
"
-- MayerVietorisSquare : le complexe court du carré de Mayer-Vietoris \n",
- "
#check Grothendieck.MayerVietorisSquare.mv_short_complex 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) \n",
+ "
# check Grothendieck. MayerVietorisSquare. mv_short_complex 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) \n",
"
--% env 6 \n",
"
\n",
@@ -1958,10 +1920,10 @@
"id": "0d592cad",
"metadata": {
"papermill": {
- "duration": 0.004628,
- "end_time": "2026-09-07T11:09:54.080897+00:00",
+ "duration": 0.006549,
+ "end_time": "2026-09-20T09:10:45.780195+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:54.076269+00:00",
+ "start_time": "2026-09-20T09:10:45.773646+00:00",
"status": "completed"
},
"tags": []
@@ -1994,16 +1956,16 @@
"id": "aba6f95d",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-09-12T21:52:05.995683Z",
- "iopub.status.busy": "2026-09-12T21:52:05.995545Z",
- "iopub.status.idle": "2026-09-12T21:52:06.179039Z",
- "shell.execute_reply": "2026-09-12T21:52:06.178129Z"
+ "iopub.execute_input": "2026-09-20T09:10:45.796103Z",
+ "iopub.status.busy": "2026-09-20T09:10:45.795766Z",
+ "iopub.status.idle": "2026-09-20T09:10:46.030304Z",
+ "shell.execute_reply": "2026-09-20T09:10:46.029233Z"
},
"papermill": {
- "duration": 0.222076,
- "end_time": "2026-09-07T11:09:54.307636+00:00",
+ "duration": 0.243643,
+ "end_time": "2026-09-20T09:10:46.030869+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:54.085560+00:00",
+ "start_time": "2026-09-20T09:10:45.787226+00:00",
"status": "completed"
},
"tags": []
@@ -2022,28 +1984,28 @@
" \n",
" \n",
"
-- SchemesTour : les morphismes de schémas sont continus \n",
- "
#check Grothendieck.scheme_hom_continuous Grothendieck.scheme_hom_continuous. {u_1} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Continuous ⇑ f \n",
+ "
# check Grothendieck. scheme_hom_continuous Grothendieck. scheme_hom_continuous. {u_1} {X Y : AlgebraicGeometry. Scheme} (f : X ⟶ Y) : Continuous ⇑ f \n",
"
-- ZariskiSite : la topologie de Zariski est une topologie de Grothendieck \n",
- "
#check Grothendieck.zariski_topology_eq Grothendieck.zariski_topology_eq. {u_1} :\n",
- " AlgebraicGeometry.Scheme.zariskiTopology = AlgebraicGeometry.Scheme.zariskiPretopology.toGrothendieck \n",
+ "
# check Grothendieck. zariski_topology_eq Grothendieck. zariski_topology_eq. {u_1} :\n",
+ " AlgebraicGeometry. Scheme. zariskiTopology = AlgebraicGeometry. Scheme. zariskiPretopology. toGrothendieck \n",
"
-- Construction : la construction du préfaisceau de Grothendieck \n",
- "
#check Grothendieck.Construction.grothendieck_field 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) \n",
- "
#check Grothendieck.Construction.forget_family 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 \n",
+ "
# check Grothendieck. Construction. grothendieck_field 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) \n",
+ "
# check Grothendieck. Construction. forget_family 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 \n",
"
-- Conservative : une famille conservatrice de points \n",
- "
#check Grothendieck.Conservative.has_enough_points_field Grothendieck.Conservative.has_enough_points_field. {v, u, w} {C : Type u} [CategoryTheory.Category. {v, u} C]\n",
- " (J : CategoryTheory.GrothendieckTopology C) : Prop \n",
- "
#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]\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) \n",
+ "
# check Grothendieck. Conservative. has_enough_points_field Grothendieck. Conservative. has_enough_points_field. {v, u, w} {C : Type u} [CategoryTheory. Category. {v, u} C]\n",
+ " (J : CategoryTheory. GrothendieckTopology C) : Prop \n",
+ "
# 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]\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) \n",
"
--% env 7 \n",
"
\n",
@@ -2178,10 +2140,10 @@
"id": "8e6834d5",
"metadata": {
"papermill": {
- "duration": 0.004656,
- "end_time": "2026-09-07T11:09:54.317996+00:00",
+ "duration": 0.009513,
+ "end_time": "2026-09-20T09:10:46.047216+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:54.313340+00:00",
+ "start_time": "2026-09-20T09:10:46.037703+00:00",
"status": "completed"
},
"tags": []
@@ -2213,16 +2175,16 @@
"id": "d3d885e8",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-09-12T21:52:06.181790Z",
- "iopub.status.busy": "2026-09-12T21:52:06.181665Z",
- "iopub.status.idle": "2026-09-12T21:52:06.379819Z",
- "shell.execute_reply": "2026-09-12T21:52:06.378983Z"
+ "iopub.execute_input": "2026-09-20T09:10:46.061248Z",
+ "iopub.status.busy": "2026-09-20T09:10:46.061058Z",
+ "iopub.status.idle": "2026-09-20T09:10:46.272238Z",
+ "shell.execute_reply": "2026-09-20T09:10:46.270376Z"
},
"papermill": {
- "duration": 0.185809,
- "end_time": "2026-09-07T11:09:54.508495+00:00",
+ "duration": 0.219736,
+ "end_time": "2026-09-20T09:10:46.273776+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:54.322686+00:00",
+ "start_time": "2026-09-20T09:10:46.054040+00:00",
"status": "completed"
},
"tags": []
@@ -2241,22 +2203,22 @@
" \n",
" \n",
"
-- Calibration : micro-preuves : triviale ≤ discrète, pullback de top \n",
- "
#check Grothendieck.trivial_le_discrete 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 \n",
- "
#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) :\n",
- " CategoryTheory.Sieve.pullback f ⊤ = ⊤ \n",
+ "
# check Grothendieck. trivial_le_discrete 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 \n",
+ "
# 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) :\n",
+ " CategoryTheory. Sieve. pullback f ⊤ = ⊤ \n",
"
-- CategoryAndSites : les axiomes de topologie (top couvre) \n",
- "
#check Grothendieck.top_covers 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 \n",
+ "
# check Grothendieck. top_covers 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 \n",
"
-- Cover : la couverture bundlée : `J.Cover X = { S : Sieve X // S ∈ J X }` \n",
- "
#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}\n",
- " (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve X) : S ∈ J X ↔ ∃ T, ↑ T = S \n",
- "
#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}\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",
+ "# 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}\n",
+ " (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}\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 (↑ (T { Y := Z, f := e2, hf := hS })). arrows e1 ∧ CategoryTheory. CategoryStruct. comp e1 e2 = f \n",
"
--% env 8 \n",
"
\n",
@@ -2372,10 +2334,10 @@
"id": "d0925be0",
"metadata": {
"papermill": {
- "duration": 0.004398,
- "end_time": "2026-09-07T11:09:54.517505+00:00",
+ "duration": 0.010587,
+ "end_time": "2026-09-20T09:10:46.300585+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:54.513107+00:00",
+ "start_time": "2026-09-20T09:10:46.289998+00:00",
"status": "completed"
},
"tags": []
@@ -2400,16 +2362,16 @@
"id": "e59a248e",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-09-12T21:52:06.382834Z",
- "iopub.status.busy": "2026-09-12T21:52:06.382658Z",
- "iopub.status.idle": "2026-09-12T21:52:06.563898Z",
- "shell.execute_reply": "2026-09-12T21:52:06.562762Z"
+ "iopub.execute_input": "2026-09-20T09:10:46.328599Z",
+ "iopub.status.busy": "2026-09-20T09:10:46.328412Z",
+ "iopub.status.idle": "2026-09-20T09:10:46.575442Z",
+ "shell.execute_reply": "2026-09-20T09:10:46.574369Z"
},
"papermill": {
- "duration": 0.182732,
- "end_time": "2026-09-07T11:09:54.704900+00:00",
+ "duration": 0.260581,
+ "end_time": "2026-09-20T09:10:46.576170+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:54.522168+00:00",
+ "start_time": "2026-09-20T09:10:46.315589+00:00",
"status": "completed"
},
"tags": []
@@ -2428,9 +2390,9 @@
" \n",
" \n",
"
-- Chaque theoreme du lake ne depend que des axiomes standards de Lean \n",
- "
#print axioms Grothendieck.trivial_le_discrete ' Grothendieck.trivial_le_discrete' depends on axioms : [propext, Classical.choice, Quot.sound] \n",
- "
#print axioms Grothendieck.Adjunction.adj_toEquivalence ' Grothendieck.Adjunction.adj_toEquivalence' depends on axioms : [propext, Classical.choice, Quot.sound] \n",
- "
#print axioms Grothendieck.SheafCohomology.H0_equiv_global_sections ' Grothendieck.SheafCohomology.H0_equiv_global_sections' depends on axioms : [propext, Classical.choice, Quot.sound] \n",
+ "
# print axioms Grothendieck. trivial_le_discrete ' Grothendieck. trivial_le_discrete' depends on axioms: [propext, Classical. choice, Quot. sound] \n",
+ "
# print axioms Grothendieck. Adjunction. adj_toEquivalence ' Grothendieck. Adjunction. adj_toEquivalence' depends on axioms: [propext, Classical. choice, Quot. sound] \n",
+ "
# print axioms Grothendieck. SheafCohomology. H0_equiv_global_sections ' Grothendieck. SheafCohomology. H0_equiv_global_sections' depends on axioms: [propext, Classical. choice, Quot. sound] \n",
"
\n",
"
--% env 9 \n",
"
\n",
- "
-- Exercice 1 : verifier que la symetrie d'une equivalence est involutive \n",
+ "
-- 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",
+ "
-- (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 — la triviale est bien une topologie \n",
- "
-- (indice : trivial_le_discrete existe deja ; cherchez l'ordre) \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 — composer deux equivalences \n",
@@ -2615,7 +2577,7 @@
"
-- 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) \n",
- "
example : True := trivial\n",
+ "
example : True := trivial\n",
"
--% env 10 \n",
"
\n",
@@ -2691,10 +2653,10 @@
"id": "eb84c944",
"metadata": {
"papermill": {
- "duration": 0.004605,
- "end_time": "2026-09-07T11:09:54.929235+00:00",
+ "duration": 0.008453,
+ "end_time": "2026-09-20T09:10:46.918695+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:54.924630+00:00",
+ "start_time": "2026-09-20T09:10:46.910242+00:00",
"status": "completed"
},
"tags": []
@@ -2726,16 +2688,16 @@
"id": "84776eca",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-09-12T21:52:06.740550Z",
- "iopub.status.busy": "2026-09-12T21:52:06.740417Z",
- "iopub.status.idle": "2026-09-12T21:52:06.925692Z",
- "shell.execute_reply": "2026-09-12T21:52:06.924896Z"
+ "iopub.execute_input": "2026-09-20T09:10:46.937702Z",
+ "iopub.status.busy": "2026-09-20T09:10:46.937359Z",
+ "iopub.status.idle": "2026-09-20T09:10:47.137384Z",
+ "shell.execute_reply": "2026-09-20T09:10:47.136577Z"
},
"papermill": {
- "duration": 0.192508,
- "end_time": "2026-09-07T11:09:55.126408+00:00",
+ "duration": 0.211226,
+ "end_time": "2026-09-20T09:10:47.137981+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:54.933900+00:00",
+ "start_time": "2026-09-20T09:10:46.926755+00:00",
"status": "completed"
},
"tags": []
@@ -2755,31 +2717,31 @@
" \n",
"
-- 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 @ 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",
+ "# check @ Grothendieck. sheaf_iff_equalizer_sieve @ 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) ⋯ )) #check @ Grothendieck.sheaf_iff_equalizer_arrows @ 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",
+ " (CategoryTheory. Limits. IsLimit\n",
+ " (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]\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",
+ " 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 π) ⋯ )) #check @ Grothendieck.sheaf_pretopology_iff @ 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 (CategoryTheory. Limits. IsLimit\n",
+ " (CategoryTheory. Limits. Fork. ofι (CategoryTheory. Equalizer. Presieve. Arrows. forkMap P X π) ⋯ )) \n",
+ "
# check @ Grothendieck. sheaf_pretopology_iff @ 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 \n",
"
\n",
"
-- Integrite (meme protocole que la section 10) : aucun pont ne depend de sorryAx \n",
- "
#print axioms Grothendieck.sheaf_iff_equalizer_sieve ' Grothendieck.sheaf_iff_equalizer_sieve' depends on axioms : [propext, Classical.choice, Quot.sound] \n",
- "
#print axioms Grothendieck.sheaf_iff_equalizer_arrows ' Grothendieck.sheaf_iff_equalizer_arrows' depends on axioms : [propext, Classical.choice, Quot.sound] \n",
- "
#print axioms Grothendieck.sheaf_pretopology_iff ' Grothendieck.sheaf_pretopology_iff' depends on axioms : [propext, Classical.choice, Quot.sound] \n",
+ "
# print axioms Grothendieck. sheaf_iff_equalizer_sieve ' Grothendieck. sheaf_iff_equalizer_sieve' depends on axioms: [propext, Classical. choice, Quot. sound] \n",
+ "
# print axioms Grothendieck. sheaf_iff_equalizer_arrows ' Grothendieck. sheaf_iff_equalizer_arrows' depends on axioms: [propext, Classical. choice, Quot. sound] \n",
+ "
# print axioms Grothendieck. sheaf_pretopology_iff ' Grothendieck. sheaf_pretopology_iff' depends on axioms: [propext, Classical. choice, Quot. sound] \n",
"
\n",
"
--% env 11 \n",
"
\n",
"
-- Lawvere–Tierney : fermeture extensive, idempotente et monotone des cribles \n",
- "
#check @ Grothendieck.LawvereTierney.lawvereTierneyDiscrete @ Grothendieck.LawvereTierney.lawvereTierneyDiscrete : {C : Type u_1} → \n",
- " [inst : CategoryTheory.Category. {u_2, u_1} C] → Grothendieck.LawvereTierney.LawvereTierney C \n",
- "
#check @ Grothendieck.LawvereTierney.j_monotone @ Grothendieck.LawvereTierney.j_monotone : ∀ {C : Type u_1} [inst : CategoryTheory.Category. {u_2, u_1} C]\n",
- " (j : Grothendieck.LawvereTierney.LawvereTierney C) {X : C} {S T : CategoryTheory.Sieve X},\n",
- " S ≤ T → j.closure X S ≤ j.closure X T \n",
- "
#check @ Grothendieck.LawvereTierney.closure_isClosed @ Grothendieck.LawvereTierney.closure_isClosed : ∀ {C : Type u_1} [inst : CategoryTheory.Category. {u_2, u_1} C]\n",
- " (j : Grothendieck.LawvereTierney.LawvereTierney C) {X : C} (S : CategoryTheory.Sieve X),\n",
- " Grothendieck.LawvereTierney.IsClosed j (j.closure X S) \n",
+ "
# check @ Grothendieck. LawvereTierney. lawvereTierneyDiscrete @ Grothendieck. LawvereTierney. lawvereTierneyDiscrete : {C : Type u_1} → \n",
+ " [inst : CategoryTheory. Category. {u_2, u_1} C] → Grothendieck. LawvereTierney. LawvereTierney C \n",
+ "
# check @ Grothendieck. LawvereTierney. j_monotone @ Grothendieck. LawvereTierney. j_monotone : ∀ {C : Type u_1} [inst : CategoryTheory. Category. {u_2, u_1} C]\n",
+ " (j : Grothendieck. LawvereTierney. LawvereTierney C) {X : C} {S T : CategoryTheory. Sieve X},\n",
+ " S ≤ T → j. closure X S ≤ j. closure X T \n",
+ "
# check @ Grothendieck. LawvereTierney. closure_isClosed @ Grothendieck. LawvereTierney. closure_isClosed : ∀ {C : Type u_1} [inst : CategoryTheory. Category. {u_2, u_1} C]\n",
+ " (j : Grothendieck. LawvereTierney. LawvereTierney C) {X : C} (S : CategoryTheory. Sieve X),\n",
+ " Grothendieck. LawvereTierney. IsClosed j (j. closure X S) \n",
"
\n",
"
-- Dictionnaire : topologie de Grothendieck et opérateur de Lawvere–Tierney \n",
- "
#check @ Grothendieck.TopologyDictionary.grothendieckToLawvereTierney @ Grothendieck.TopologyDictionary.grothendieckToLawvereTierney : {C : Type u_1} → \n",
- " [inst : CategoryTheory.Category. {u_2, u_1} C] → \n",
- " CategoryTheory.GrothendieckTopology C → Grothendieck.LawvereTierney.LawvereTierney C \n",
- "
#check @ Grothendieck.TopologyDictionary.lawvereTierneyToGrothendieck_comp_grothendieckToLawvereTierney @ Grothendieck.TopologyDictionary.lawvereTierneyToGrothendieck_comp_grothendieckToLawvereTierney : ∀ {C : Type u_1}\n",
- " [inst : CategoryTheory.Category. {u_2, u_1} C] (J : CategoryTheory.GrothendieckTopology C),\n",
- " Grothendieck.TopologyDictionary.lawvereTierneyToGrothendieck\n",
- " (Grothendieck.TopologyDictionary.grothendieckToLawvereTierney J) = \n",
+ "# check @ Grothendieck. TopologyDictionary. grothendieckToLawvereTierney @ Grothendieck. TopologyDictionary. grothendieckToLawvereTierney : {C : Type u_1} → \n",
+ " [inst : CategoryTheory. Category. {u_2, u_1} C] → \n",
+ " CategoryTheory. GrothendieckTopology C → Grothendieck. LawvereTierney. LawvereTierney C # check @ Grothendieck. TopologyDictionary. lawvereTierneyToGrothendieck_comp_grothendieckToLawvereTierney @ Grothendieck. TopologyDictionary. lawvereTierneyToGrothendieck_comp_grothendieckToLawvereTierney : ∀ {C : Type u_1}\n",
+ " [inst : CategoryTheory. Category. {u_2, u_1} C] (J : CategoryTheory. GrothendieckTopology C),\n",
+ " Grothendieck. TopologyDictionary. lawvereTierneyToGrothendieck\n",
+ " (Grothendieck. TopologyDictionary. grothendieckToLawvereTierney J) = \n",
" J #check @ Grothendieck.TopologyDictionary.grothendieckToLawvereTierney_comp_lawvereTierneyToGrothendieck_closure @ Grothendieck.TopologyDictionary.grothendieckToLawvereTierney_comp_lawvereTierneyToGrothendieck_closure : ∀ \n",
- " {C : Type u_1} [inst : CategoryTheory.Category. {u_2, u_1} C] (j : Grothendieck.LawvereTierney.LawvereTierney C),\n",
- " (Grothendieck.TopologyDictionary.grothendieckToLawvereTierney\n",
- " (Grothendieck.TopologyDictionary.lawvereTierneyToGrothendieck j)). closure = \n",
- " j.closure # check @ Grothendieck. TopologyDictionary. grothendieckToLawvereTierney_comp_lawvereTierneyToGrothendieck_closure @ Grothendieck. TopologyDictionary. grothendieckToLawvereTierney_comp_lawvereTierneyToGrothendieck_closure : ∀ \n",
+ " {C : Type u_1} [inst : CategoryTheory. Category. {u_2, u_1} C] (j : Grothendieck. LawvereTierney. LawvereTierney C),\n",
+ " (Grothendieck. TopologyDictionary. grothendieckToLawvereTierney\n",
+ " (Grothendieck. TopologyDictionary. lawvereTierneyToGrothendieck j)). closure = \n",
+ " j. closure -- Construction Plus : naturalité, itération et propriété universelle #check @ Grothendieck.toPlus_naturality_field @ Grothendieck.toPlus_naturality_field : ∀ {C : Type u_1} [inst : CategoryTheory.Category. {u_3, u_1} C] {D : Type u_2}\n",
- " [inst_1 : CategoryTheory.Category. {u_4, u_2} D] (J : CategoryTheory.GrothendieckTopology C)\n",
+ "# check @ Grothendieck. toPlus_naturality_field @ Grothendieck. toPlus_naturality_field : ∀ {C : Type u_1} [inst : CategoryTheory. Category. {u_3, u_1} C] {D : Type u_2}\n",
+ " [inst_1 : CategoryTheory. Category. {u_4, u_2} D] (J : CategoryTheory. GrothendieckTopology C)\n",
" [inst_2 :\n",
- " ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]\n",
- " [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}\n",
+ " ∀ (P : CategoryTheory. Functor Cᵒᵖ D) (X : C) (S : J. Cover X), CategoryTheory. Limits. HasMultiequalizer (S. index P)]\n",
+ " [inst_3 : ∀ (X : C), CategoryTheory. Limits. HasColimitsOfShape (J. Cover X)ᵒᵖ D] {P Q : CategoryTheory. Functor Cᵒᵖ D}\n",
" (η : P ⟶ Q),\n",
- " CategoryTheory.CategoryStruct.comp η (J.toPlus Q) = CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusMap η) #check @ Grothendieck.plusMap_toPlus_field @ Grothendieck.plusMap_toPlus_field : ∀ {C : Type u_1} [inst : CategoryTheory.Category. {u_3, u_1} C] {D : Type u_2}\n",
- " [inst_1 : CategoryTheory.Category. {u_4, u_2} D] (J : CategoryTheory.GrothendieckTopology C)\n",
+ " CategoryTheory. CategoryStruct. comp η (J. toPlus Q) = CategoryTheory. CategoryStruct. comp (J. toPlus P) (J. plusMap η) # check @ Grothendieck. plusMap_toPlus_field @ Grothendieck. plusMap_toPlus_field : ∀ {C : Type u_1} [inst : CategoryTheory. Category. {u_3, u_1} C] {D : Type u_2}\n",
+ " [inst_1 : CategoryTheory. Category. {u_4, u_2} D] (J : CategoryTheory. GrothendieckTopology C)\n",
" [inst_2 :\n",
- " ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]\n",
- " [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D),\n",
- " J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P) #check @ Grothendieck.plusLift_unique_field @ Grothendieck.plusLift_unique_field : ∀ {C : Type u_1} [inst : CategoryTheory.Category. {u_3, u_1} C] {D : Type u_2}\n",
- " [inst_1 : CategoryTheory.Category. {u_4, u_2} D] (J : CategoryTheory.GrothendieckTopology C)\n",
+ " ∀ (P : CategoryTheory. Functor Cᵒᵖ D) (X : C) (S : J. Cover X), CategoryTheory. Limits. HasMultiequalizer (S. index P)]\n",
+ " [inst_3 : ∀ (X : C), CategoryTheory. Limits. HasColimitsOfShape (J. Cover X)ᵒᵖ D] (P : CategoryTheory. Functor Cᵒᵖ D),\n",
+ " J. plusMap (J. toPlus P) = J. toPlus (J. plusObj P) # check @ Grothendieck. plusLift_unique_field @ Grothendieck. plusLift_unique_field : ∀ {C : Type u_1} [inst : CategoryTheory. Category. {u_3, u_1} C] {D : Type u_2}\n",
+ " [inst_1 : CategoryTheory. Category. {u_4, u_2} D] (J : CategoryTheory. GrothendieckTopology C)\n",
" [inst_2 :\n",
- " ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]\n",
- " [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}\n",
- " (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : J.plusObj P ⟶ Q),\n",
- " CategoryTheory.CategoryStruct.comp (J.toPlus P) γ = η → γ = J.plusLift η hQ ∀ (P : CategoryTheory. Functor Cᵒᵖ D) (X : C) (S : J. Cover X), CategoryTheory. Limits. HasMultiequalizer (S. index P)]\n",
+ " [inst_3 : ∀ (X : C), CategoryTheory. Limits. HasColimitsOfShape (J. Cover X)ᵒᵖ D] {P Q : CategoryTheory. Functor Cᵒᵖ D}\n",
+ " (η : P ⟶ Q) (hQ : CategoryTheory. Presheaf. IsSheaf J Q) (γ : J. plusObj P ⟶ Q),\n",
+ " CategoryTheory. CategoryStruct. comp (J. toPlus P) γ = η → γ = J. plusLift η hQ #print axioms Grothendieck.LawvereTierney.j_monotone ' Grothendieck.LawvereTierney.j_monotone' depends on axioms : [propext, Classical.choice, Quot.sound] #print axioms Grothendieck.TopologyDictionary.lawvereTierneyToGrothendieck_comp_grothendieckToLawvereTierney ' Grothendieck.TopologyDictionary.lawvereTierneyToGrothendieck_comp_grothendieckToLawvereTierney' depends on axioms : [propext,\n",
- " Classical.choice,\n",
- " Quot.sound] #print axioms Grothendieck.plusLift_unique_field ' Grothendieck.plusLift_unique_field' depends on axioms : [propext, Classical.choice, Quot.sound] # print axioms Grothendieck. LawvereTierney. j_monotone ' Grothendieck. LawvereTierney. j_monotone' depends on axioms: [propext, Classical. choice, Quot. sound] # print axioms Grothendieck. TopologyDictionary. lawvereTierneyToGrothendieck_comp_grothendieckToLawvereTierney ' Grothendieck. TopologyDictionary. lawvereTierneyToGrothendieck_comp_grothendieckToLawvereTierney' depends on axioms: [propext,\n",
+ " Classical. choice,\n",
+ " Quot. sound] # print axioms Grothendieck. plusLift_unique_field ' Grothendieck. plusLift_unique_field' depends on axioms: [propext, Classical. choice, Quot. sound] --% env 12 \n",
"
\n",
@@ -3302,10 +3264,10 @@
"id": "534c7163",
"metadata": {
"papermill": {
- "duration": 0.006336,
- "end_time": "2026-09-07T11:09:55.384973+00:00",
+ "duration": 0.007825,
+ "end_time": "2026-09-20T09:10:47.482333+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:55.378637+00:00",
+ "start_time": "2026-09-20T09:10:47.474508+00:00",
"status": "completed"
},
"tags": []
@@ -3339,7 +3301,16 @@
{
"cell_type": "markdown",
"id": "0d4dbab3",
- "metadata": {},
+ "metadata": {
+ "papermill": {
+ "duration": 0.009645,
+ "end_time": "2026-09-20T09:10:47.499784+00:00",
+ "exception": false,
+ "start_time": "2026-09-20T09:10:47.490139+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
"source": [
"## Annexe — Les tiges (stalks) : du germe au recollement (#11703)\n",
"\n",
@@ -3390,11 +3361,19 @@
"id": "6628248e",
"metadata": {
"execution": {
- "iopub.execute_input": "2026-09-12T21:52:07.134166Z",
- "iopub.status.busy": "2026-09-12T21:52:07.134012Z",
- "iopub.status.idle": "2026-09-12T21:52:07.398514Z",
- "shell.execute_reply": "2026-09-12T21:52:07.397297Z"
- }
+ "iopub.execute_input": "2026-09-20T09:10:47.518709Z",
+ "iopub.status.busy": "2026-09-20T09:10:47.518368Z",
+ "iopub.status.idle": "2026-09-20T09:10:47.842015Z",
+ "shell.execute_reply": "2026-09-20T09:10:47.841101Z"
+ },
+ "papermill": {
+ "duration": 0.333641,
+ "end_time": "2026-09-20T09:10:47.843194+00:00",
+ "exception": false,
+ "start_time": "2026-09-20T09:10:47.509553+00:00",
+ "status": "completed"
+ },
+ "tags": []
},
"outputs": [
{
@@ -3413,127 +3392,127 @@
"-- 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 Grothendieck.unique_stalk_yoneda : (T : Type u_1) → \n",
+ "# check @ Grothendieck. unique_stalk_yoneda Grothendieck. unique_stalk_yoneda : (T : Type u_1) → \n",
" [inst : TopologicalSpace T] → \n",
- " (U : TopologicalSpace.Opens T) → {x : T} → x ∈ U → Unique (TopCat.Presheaf.stalk (CategoryTheory.yoneda.obj U) x) #check @ Grothendieck.isEmpty_stalk_yoneda Grothendieck.isEmpty_stalk_yoneda : ∀ (T : Type u_1) [inst : TopologicalSpace T] (U : TopologicalSpace.Opens T) {x : T},\n",
- " x ∉ U → IsEmpty (TopCat.Presheaf.stalk (CategoryTheory.yoneda.obj U) x) #check @ Grothendieck.nonempty_stalk_yoneda_iff Grothendieck.nonempty_stalk_yoneda_iff : ∀ (T : Type u_1) [inst : TopologicalSpace T] (U : TopologicalSpace.Opens T)\n",
- " (x : T), Nonempty (TopCat.Presheaf.stalk (CategoryTheory.yoneda.obj U) x) ↔ x ∈ U (U : TopologicalSpace. Opens T) → {x : T} → x ∈ U → Unique (TopCat. Presheaf. stalk (CategoryTheory. yoneda. obj U) x) # check @ Grothendieck. isEmpty_stalk_yoneda Grothendieck. isEmpty_stalk_yoneda : ∀ (T : Type u_1) [inst : TopologicalSpace T] (U : TopologicalSpace. Opens T) {x : T},\n",
+ " x ∉ U → IsEmpty (TopCat. Presheaf. stalk (CategoryTheory. yoneda. obj U) x) # check @ Grothendieck. nonempty_stalk_yoneda_iff Grothendieck. nonempty_stalk_yoneda_iff : ∀ (T : Type u_1) [inst : TopologicalSpace T] (U : TopologicalSpace. Opens T)\n",
+ " (x : T), Nonempty (TopCat. Presheaf. stalk (CategoryTheory. yoneda. obj U) x) ↔ x ∈ U -- StalkSeparated (Partie 74) : les tiges detectent l'egalite des sections #check @ Grothendieck.eq_of_germ_eq_of_isSeparated Grothendieck.eq_of_germ_eq_of_isSeparated : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)),\n",
- " CategoryTheory.Presheaf.IsSeparated (Grothendieck.opensTopology T) F → \n",
- " ∀ {U : TopologicalSpace.Opens T} {s t : F.obj (Opposite.op U)},\n",
+ "-- StalkSeparated (Partie 74) : les tiges detectent l'egalite des sections # check @ Grothendieck. eq_of_germ_eq_of_isSeparated Grothendieck. eq_of_germ_eq_of_isSeparated : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)),\n",
+ " CategoryTheory. Presheaf. IsSeparated (Grothendieck. opensTopology T) F → \n",
+ " ∀ {U : TopologicalSpace. Opens T} {s t : F. obj (Opposite. op U)},\n",
" (∀ (x : T) (hx : x ∈ U),\n",
- " (CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) s = \n",
- " (CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) t) → \n",
+ " (CategoryTheory. ConcreteCategory. hom (F. germ U x hx)) s = \n",
+ " (CategoryTheory. ConcreteCategory. hom (F. germ U x hx)) t) → \n",
" s = t #check @ Grothendieck.eq_of_germ_eq_of_isSheaf Grothendieck.eq_of_germ_eq_of_isSheaf : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)),\n",
- " F.IsSheaf → \n",
- " ∀ {U : TopologicalSpace.Opens T} {s t : F.obj (Opposite.op U)},\n",
+ "# check @ Grothendieck. eq_of_germ_eq_of_isSheaf Grothendieck. eq_of_germ_eq_of_isSheaf : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)),\n",
+ " F. IsSheaf → \n",
+ " ∀ {U : TopologicalSpace. Opens T} {s t : F. obj (Opposite. op U)},\n",
" (∀ (x : T) (hx : x ∈ U),\n",
- " (CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) s = \n",
- " (CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) t) → \n",
+ " (CategoryTheory. ConcreteCategory. hom (F. germ U x hx)) s = \n",
+ " (CategoryTheory. ConcreteCategory. hom (F. germ U x hx)) t) → \n",
" s = t #check @ Grothendieck.injective_germ_family_of_isSeparated Grothendieck.injective_germ_family_of_isSeparated : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)),\n",
- " CategoryTheory.Presheaf.IsSeparated (Grothendieck.opensTopology T) F → \n",
- " ∀ (U : TopologicalSpace.Opens T),\n",
- " Function.Injective fun s p => (CategoryTheory.ConcreteCategory.hom (F.germ U ↑ p ⋯ )) s # check @ Grothendieck. injective_germ_family_of_isSeparated Grothendieck. injective_germ_family_of_isSeparated : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)),\n",
+ " CategoryTheory. Presheaf. IsSeparated (Grothendieck. opensTopology T) F → \n",
+ " ∀ (U : TopologicalSpace. Opens T),\n",
+ " Function. Injective fun s p => (CategoryTheory. ConcreteCategory. hom (F. germ U ↑ p ⋯ )) s -- StalkGluing (Partie 75) : les familles de germes et leur recollement #check @ Grothendieck.GermFamily Grothendieck.GermFamily : (T : Type u_1) → \n",
- " [inst : TopologicalSpace T] → TopCat.Presheaf (Type u_1) (TopCat.of T) → TopologicalSpace.Opens T → Type u_1 #check @ Grothendieck.GermFamily.IsLocallyRepresentable Grothendieck.GermFamily.IsLocallyRepresentable : (T : Type u_1) → \n",
+ "# check @ Grothendieck. GermFamily Grothendieck. GermFamily : (T : Type u_1) → \n",
+ " [inst : TopologicalSpace T] → TopCat. Presheaf (Type u_1) (TopCat. of T) → TopologicalSpace. Opens T → Type u_1 # check @ Grothendieck. GermFamily. IsLocallyRepresentable Grothendieck. GermFamily. IsLocallyRepresentable : (T : Type u_1) → \n",
" [inst : TopologicalSpace T] → \n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) → \n",
- " (U : TopologicalSpace.Opens T) → Grothendieck.GermFamily T F U → Prop #check @ Grothendieck.germFamily_isLocallyRepresentable Grothendieck.germFamily_isLocallyRepresentable : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) (U : TopologicalSpace.Opens T) (s : F.obj (Opposite.op U)),\n",
- " Grothendieck.GermFamily.IsLocallyRepresentable T F U fun p => (CategoryTheory.ConcreteCategory.hom (F.germ U ↑ p ⋯ )) s #check @ Grothendieck.existsUnique_gluing'_of_isSheaf Grothendieck.existsUnique_gluing'_of_isSheaf : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)),\n",
- " F.IsSheaf → \n",
- " ∀ {ι : Type u_2} (V : ι → TopologicalSpace.Opens T) (U : TopologicalSpace.Opens T) (iVU : (i : ι) → V i ⟶ U),\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)) → \n",
+ " (U : TopologicalSpace. Opens T) → Grothendieck. GermFamily T F U → Prop # check @ Grothendieck. germFamily_isLocallyRepresentable Grothendieck. germFamily_isLocallyRepresentable : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)) (U : TopologicalSpace. Opens T) (s : F. obj (Opposite. op U)),\n",
+ " Grothendieck. GermFamily. IsLocallyRepresentable T F U fun p => (CategoryTheory. ConcreteCategory. hom (F. germ U ↑ p ⋯ )) s # check @ Grothendieck. existsUnique_gluing'_of_isSheaf Grothendieck. existsUnique_gluing'_of_isSheaf : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)),\n",
+ " F. IsSheaf → \n",
+ " ∀ {ι : Type u_2} (V : ι → TopologicalSpace. Opens T) (U : TopologicalSpace. Opens T) (iVU : (i : ι) → V i ⟶ U),\n",
" U ≤ iSup V → \n",
- " ∀ (sf : (i : ι) → F.obj (Opposite.op (V i))),\n",
- " F.IsCompatible V sf → ∃! s, ∀ (i : ι), (CategoryTheory.ConcreteCategory.hom (F.map (iVU i). op)) s = sf i #check @ Grothendieck.existsUnique_section_of_isLocallyRepresentable Grothendieck.existsUnique_section_of_isLocallyRepresentable : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)),\n",
- " F.IsSheaf → \n",
- " ∀ (U : TopologicalSpace.Opens T) (a : Grothendieck.GermFamily T F U),\n",
- " Grothendieck.GermFamily.IsLocallyRepresentable T F U a → \n",
- " ∃! s, ∀ (p : ↥ U), (CategoryTheory.ConcreteCategory.hom (F.germ U ↑ p ⋯ )) s = a p #check @ Grothendieck.surjective_germ_family_to_locallyRepresentable Grothendieck.surjective_germ_family_to_locallyRepresentable : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)),\n",
- " F.IsSheaf → \n",
- " ∀ (U : TopologicalSpace.Opens T),\n",
- " Function.Surjective fun s => ⟨fun p => (CategoryTheory.ConcreteCategory.hom (F.germ U ↑ p ⋯ )) s, ⋯ ⟩ ∀ (sf : (i : ι) → F. obj (Opposite. op (V i))),\n",
+ " F. IsCompatible V sf → ∃! s, ∀ (i : ι), (CategoryTheory. ConcreteCategory. hom (F. map (iVU i). op)) s = sf i # check @ Grothendieck. existsUnique_section_of_isLocallyRepresentable Grothendieck. existsUnique_section_of_isLocallyRepresentable : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)),\n",
+ " F. IsSheaf → \n",
+ " ∀ (U : TopologicalSpace. Opens T) (a : Grothendieck. GermFamily T F U),\n",
+ " Grothendieck. GermFamily. IsLocallyRepresentable T F U a → \n",
+ " ∃! s, ∀ (p : ↥ U), (CategoryTheory. ConcreteCategory. hom (F. germ U ↑ p ⋯ )) s = a p # check @ Grothendieck. surjective_germ_family_to_locallyRepresentable Grothendieck. surjective_germ_family_to_locallyRepresentable : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)),\n",
+ " F. IsSheaf → \n",
+ " ∀ (U : TopologicalSpace. Opens T),\n",
+ " Function. Surjective fun s => ⟨ fun p => (CategoryTheory. ConcreteCategory. hom (F. germ U ↑ p ⋯ )) s, ⋯⟩ -- StalkPoints (Partie 73) : la tige comme fibre du point du site #check @ Grothendieck.opensPoint Grothendieck.opensPoint : (T : Type u_1) → [inst : TopologicalSpace T] → T → (Grothendieck.opensTopology T). Point #check @ Grothendieck.mem_of_fiber Grothendieck.mem_of_fiber : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T) {U : TopologicalSpace.Opens T}\n",
- " (p : (Grothendieck.opensPoint T x). fiber.obj U), x ∈ U #check @ Grothendieck.fiberElem Grothendieck.fiberElem : (T : Type u_1) → \n",
+ "# check @ Grothendieck. opensPoint Grothendieck. opensPoint : (T : Type u_1) → [inst : TopologicalSpace T] → T → (Grothendieck. opensTopology T). Point # check @ Grothendieck. mem_of_fiber Grothendieck. mem_of_fiber : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T) {U : TopologicalSpace. Opens T}\n",
+ " (p : (Grothendieck. opensPoint T x). fiber. obj U), x ∈ U # check @ Grothendieck. fiberElem Grothendieck. fiberElem : (T : Type u_1) → \n",
" [inst : TopologicalSpace T] → \n",
- " (x : T) → {U : TopologicalSpace.Opens T} → x ∈ U → (Grothendieck.opensPoint T x). fiber.obj U #check @ Grothendieck.fiberToStalkCocone Grothendieck.fiberToStalkCocone : (T : Type u_1) → \n",
+ " (x : T) → {U : TopologicalSpace. Opens T} → x ∈ U → (Grothendieck. opensPoint T x). fiber. obj U # check @ Grothendieck. fiberToStalkCocone Grothendieck. fiberToStalkCocone : (T : Type u_1) → \n",
" [inst : TopologicalSpace T] → \n",
" (x : T) → \n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) → \n",
- " CategoryTheory.Limits.Cocone\n",
- " ((CategoryTheory.CategoryOfElements.π (Grothendieck.opensPoint T x). fiber). op.comp F) #check @ Grothendieck.fiberToStalk Grothendieck.fiberToStalk : (T : Type u_1) → \n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)) → \n",
+ " CategoryTheory. Limits. Cocone\n",
+ " ((CategoryTheory. CategoryOfElements. π (Grothendieck. opensPoint T x). fiber). op. comp F) # check @ Grothendieck. fiberToStalk Grothendieck. fiberToStalk : (T : Type u_1) → \n",
" [inst : TopologicalSpace T] → \n",
" (x : T) → \n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) → (Grothendieck.opensPoint T x). presheafFiber.obj F ⟶ F.stalk x #check @ Grothendieck.stalkToFiberCocone Grothendieck.stalkToFiberCocone : (T : Type u_1) → \n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)) → (Grothendieck. opensPoint T x). presheafFiber. obj F ⟶ F. stalk x # check @ Grothendieck. stalkToFiberCocone Grothendieck. stalkToFiberCocone : (T : Type u_1) → \n",
" [inst : TopologicalSpace T] → \n",
" (x : T) → \n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) → \n",
- " CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion x). op.comp F) #check @ Grothendieck.stalkToFiber Grothendieck.stalkToFiber : (T : Type u_1) → \n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)) → \n",
+ " CategoryTheory. Limits. Cocone ((TopologicalSpace. OpenNhds. inclusion x). op. comp F) # check @ Grothendieck. stalkToFiber Grothendieck. stalkToFiber : (T : Type u_1) → \n",
" [inst : TopologicalSpace T] → \n",
" (x : T) → \n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) → F.stalk x ⟶ (Grothendieck.opensPoint T x). presheafFiber.obj F #check @ Grothendieck.toPresheafFiber_fiberToStalk Grothendieck.toPresheafFiber_fiberToStalk : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T)\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) (U : TopologicalSpace.Opens T)\n",
- " (p : (Grothendieck.opensPoint T x). fiber.obj U),\n",
- " CategoryTheory.CategoryStruct.comp ((Grothendieck.opensPoint T x). toPresheafFiber U p F)\n",
- " (Grothendieck.fiberToStalk T x F) = \n",
- " F.germ U x ⋯ #check @ Grothendieck.germ_stalkToFiber Grothendieck.germ_stalkToFiber : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T)\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) (U : TopologicalSpace.Opens T) (hx : x ∈ U),\n",
- " CategoryTheory.CategoryStruct.comp (F.germ U x hx) (Grothendieck.stalkToFiber T x F) = \n",
- " (Grothendieck.opensPoint T x). toPresheafFiber U { down := { down := hx } } F #check @ Grothendieck.stalkToFiber_comp_fiberToStalk Grothendieck.stalkToFiber_comp_fiberToStalk : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T)\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)),\n",
- " CategoryTheory.CategoryStruct.comp (Grothendieck.stalkToFiber T x F) (Grothendieck.fiberToStalk T x F) = \n",
- " CategoryTheory.CategoryStruct.id (F.stalk x) #check @ Grothendieck.fiberToStalk_comp_stalkToFiber Grothendieck.fiberToStalk_comp_stalkToFiber : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T)\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)),\n",
- " CategoryTheory.CategoryStruct.comp (Grothendieck.fiberToStalk T x F) (Grothendieck.stalkToFiber T x F) = \n",
- " CategoryTheory.CategoryStruct.id ((Grothendieck.opensPoint T x). presheafFiber.obj F) #check @ Grothendieck.stalkFiberIso Grothendieck.stalkFiberIso : (T : Type u_1) → \n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)) → F. stalk x ⟶ (Grothendieck. opensPoint T x). presheafFiber. obj F # check @ Grothendieck. toPresheafFiber_fiberToStalk Grothendieck. toPresheafFiber_fiberToStalk : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T)\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)) (U : TopologicalSpace. Opens T)\n",
+ " (p : (Grothendieck. opensPoint T x). fiber. obj U),\n",
+ " CategoryTheory. CategoryStruct. comp ((Grothendieck. opensPoint T x). toPresheafFiber U p F)\n",
+ " (Grothendieck. fiberToStalk T x F) = \n",
+ " F. germ U x ⋯ # check @ Grothendieck. germ_stalkToFiber Grothendieck. germ_stalkToFiber : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T)\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)) (U : TopologicalSpace. Opens T) (hx : x ∈ U),\n",
+ " CategoryTheory. CategoryStruct. comp (F. germ U x hx) (Grothendieck. stalkToFiber T x F) = \n",
+ " (Grothendieck. opensPoint T x). toPresheafFiber U { down := { down := hx } } F # check @ Grothendieck. stalkToFiber_comp_fiberToStalk Grothendieck. stalkToFiber_comp_fiberToStalk : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T)\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)),\n",
+ " CategoryTheory. CategoryStruct. comp (Grothendieck. stalkToFiber T x F) (Grothendieck. fiberToStalk T x F) = \n",
+ " CategoryTheory. CategoryStruct. id (F. stalk x) # check @ Grothendieck. fiberToStalk_comp_stalkToFiber Grothendieck. fiberToStalk_comp_stalkToFiber : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T)\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)),\n",
+ " CategoryTheory. CategoryStruct. comp (Grothendieck. fiberToStalk T x F) (Grothendieck. stalkToFiber T x F) = \n",
+ " CategoryTheory. CategoryStruct. id ((Grothendieck. opensPoint T x). presheafFiber. obj F) # check @ Grothendieck. stalkFiberIso Grothendieck. stalkFiberIso : (T : Type u_1) → \n",
" [inst : TopologicalSpace T] → \n",
" (x : T) → \n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) → (Grothendieck.opensPoint T x). presheafFiber.obj F ≅ F.stalk x #check @ Grothendieck.stalkFiberIso_naturality Grothendieck.stalkFiberIso_naturality : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T)\n",
- " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) {G : TopCat.Presheaf (Type u_1) (TopCat.of T)} (f : F ⟶ G),\n",
- " CategoryTheory.CategoryStruct.comp ((Grothendieck.opensPoint T x). presheafFiber.map f)\n",
- " (Grothendieck.fiberToStalk T x G) = \n",
- " CategoryTheory.CategoryStruct.comp (Grothendieck.fiberToStalk T x F)\n",
- " ((TopCat.Presheaf.stalkFunctor (Type u_1) x). map f) (F : TopCat. Presheaf (Type u_1) (TopCat. of T)) → (Grothendieck. opensPoint T x). presheafFiber. obj F ≅ F. stalk x # check @ Grothendieck. stalkFiberIso_naturality Grothendieck. stalkFiberIso_naturality : ∀ (T : Type u_1) [inst : TopologicalSpace T] (x : T)\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)) {G : TopCat. Presheaf (Type u_1) (TopCat. of T)} (f : F ⟶ G),\n",
+ " CategoryTheory. CategoryStruct. comp ((Grothendieck. opensPoint T x). presheafFiber. map f)\n",
+ " (Grothendieck. fiberToStalk T x G) = \n",
+ " CategoryTheory. CategoryStruct. comp (Grothendieck. fiberToStalk T x F)\n",
+ " ((TopCat. Presheaf. stalkFunctor (Type u_1) x). map f) -- Integrite (meme protocole que la section 10) : un pivot par module, aucun -- ne doit dependre de sorryAx #print axioms Grothendieck.nonempty_stalk_yoneda_iff ' Grothendieck.nonempty_stalk_yoneda_iff' depends on axioms : [propext, Classical.choice, Quot.sound] #print axioms Grothendieck.eq_of_germ_eq_of_isSheaf ' Grothendieck.eq_of_germ_eq_of_isSheaf' depends on axioms : [propext, Classical.choice, Quot.sound] #print axioms Grothendieck.existsUnique_section_of_isLocallyRepresentable ' Grothendieck.existsUnique_section_of_isLocallyRepresentable' depends on axioms : [propext, Classical.choice, Quot.sound] #print axioms Grothendieck.stalkFiberIso_naturality ' Grothendieck.stalkFiberIso_naturality' depends on axioms : [propext, Classical.choice, Quot.sound] # print axioms Grothendieck. nonempty_stalk_yoneda_iff ' Grothendieck. nonempty_stalk_yoneda_iff' depends on axioms: [propext, Classical. choice, Quot. sound] # print axioms Grothendieck. eq_of_germ_eq_of_isSheaf ' Grothendieck. eq_of_germ_eq_of_isSheaf' depends on axioms: [propext, Classical. choice, Quot. sound] # print axioms Grothendieck. existsUnique_section_of_isLocallyRepresentable ' Grothendieck. existsUnique_section_of_isLocallyRepresentable' depends on axioms: [propext, Classical. choice, Quot. sound] # print axioms Grothendieck. stalkFiberIso_naturality ' Grothendieck. stalkFiberIso_naturality' depends on axioms: [propext, Classical. choice, Quot. sound] --% env 13 \n",
@@ -4055,7 +4034,16 @@
{
"cell_type": "markdown",
"id": "d77b57c0",
- "metadata": {},
+ "metadata": {
+ "papermill": {
+ "duration": 0.008752,
+ "end_time": "2026-09-20T09:10:47.861100+00:00",
+ "exception": false,
+ "start_time": "2026-09-20T09:10:47.852348+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
"source": [
"### Lecture de la sortie\n",
"\n",
@@ -4101,15 +4089,626 @@
"aussi le sien.\n"
]
},
+ {
+ "cell_type": "markdown",
+ "id": "8dbc577e",
+ "metadata": {
+ "papermill": {
+ "duration": 0.008557,
+ "end_time": "2026-09-20T09:10:47.877891+00:00",
+ "exception": false,
+ "start_time": "2026-09-20T09:10:47.869334+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "source": [
+ "## Annexe — Des ouverts au préfaisceau gratte-ciel (#11703)\n",
+ "\n",
+ "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.\n",
+ "\n",
+ "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."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "id": "b8bb566d",
+ "metadata": {
+ "execution": {
+ "iopub.execute_input": "2026-09-20T09:10:47.895760Z",
+ "iopub.status.busy": "2026-09-20T09:10:47.895587Z",
+ "iopub.status.idle": "2026-09-20T09:10:48.153425Z",
+ "shell.execute_reply": "2026-09-20T09:10:48.152599Z"
+ },
+ "papermill": {
+ "duration": 0.267654,
+ "end_time": "2026-09-20T09:10:48.154207+00:00",
+ "exception": false,
+ "start_time": "2026-09-20T09:10:47.886553+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/html": [
+ "\n",
+ " \n",
+ "
\n",
+ "
\n",
+ "
\n",
+ " \n",
+ " \n",
+ " \n",
+ "
\n",
+ "
-- SpacesMathlib : le site construit dans le lake coïncide avec celui de Mathlib \n",
+ "
# check @ Grothendieck. opensTopology_eq Grothendieck. opensTopology_eq : ∀ (T : Type u_1) [inst : TopologicalSpace T],\n",
+ " Grothendieck. opensTopology T = Opens. grothendieckTopology T \n",
+ "
# check @ Grothendieck. isSheaf_opensTopology_iff @ Grothendieck. isSheaf_opensTopology_iff : ∀ {T : Type u_1} [inst : TopologicalSpace T] {C : Type u_2}\n",
+ " [inst_1 : CategoryTheory. Category. {u_3, u_2} C] (F : TopCat. Presheaf C (TopCat. of T)),\n",
+ " CategoryTheory. Presheaf. IsSheaf (Grothendieck. opensTopology T) F ↔ F. IsSheaf \n",
+ "
# check @ Grothendieck. coversTop_opensTopology_iff @ Grothendieck. coversTop_opensTopology_iff : ∀ {T : Type u_1} [inst : TopologicalSpace T] {ι : Type u_2}\n",
+ " (U : ι → TopologicalSpace. Opens T),\n",
+ " (Grothendieck. opensTopology T). CoversTop U ↔ (Opens. grothendieckTopology T). CoversTop U \n",
+ "
\n",
+ "
-- SpacesSubcanonical : tout représentable sur le site des ouverts est un faisceau \n",
+ "
# check @ Grothendieck. isSheaf_yoneda_opensTopology Grothendieck. isSheaf_yoneda_opensTopology : ∀ (T : Type u_1) [inst : TopologicalSpace T] (U : TopologicalSpace. Opens T),\n",
+ " CategoryTheory. Presieve. IsSheaf (Grothendieck. opensTopology T) (CategoryTheory. yoneda. obj U) \n",
+ "
# check @ Grothendieck. opensTopology_subcanonical Grothendieck. opensTopology_subcanonical : ∀ (T : Type u_1) [inst : TopologicalSpace T],\n",
+ " (Grothendieck. opensTopology T). Subcanonical \n",
+ "
\n",
+ "
-- StalkCharacterization : séparation et recollement se lisent sur les germes \n",
+ "
# check @ Grothendieck. GermSeparated Grothendieck. GermSeparated : (T : Type u_1) → \n",
+ " [inst : TopologicalSpace T] → TopCat. Presheaf (Type u_1) (TopCat. of T) → Prop \n",
+ "
# check @ Grothendieck. GermGluing Grothendieck. GermGluing : (T : Type u_1) → [inst : TopologicalSpace T] → TopCat. Presheaf (Type u_1) (TopCat. of T) → Prop \n",
+ "
# check @ Grothendieck. germ_eq_of_isCompatible Grothendieck. germ_eq_of_isCompatible : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)) {ι : Type u_2} (U : ι → TopologicalSpace. Opens T)\n",
+ " (sf : (i : ι) → F. obj (Opposite. op (U i))),\n",
+ " F. IsCompatible U sf → \n",
+ " ∀ {i j : ι} {x : T} (hi : x ∈ U i) (hj : x ∈ U j),\n",
+ " (CategoryTheory. ConcreteCategory. hom (F. germ (U i) x hi)) (sf i) = \n",
+ " (CategoryTheory. ConcreteCategory. hom (F. germ (U j) x hj)) (sf j) \n",
+ "
# check @ Grothendieck. isSheaf_iff_germSeparated_and_germGluing Grothendieck. isSheaf_iff_germSeparated_and_germGluing : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
+ " (F : TopCat. Presheaf (Type u_1) (TopCat. of T)),\n",
+ " F. IsSheaf ↔ Grothendieck. GermSeparated T F ∧ Grothendieck. GermGluing T F \n",
+ "
\n",
+ "
-- Skyscraper : support et dichotomie des tiges autour du point choisi \n",
+ "
# check @ Grothendieck. Contenu. skyscraper @ Grothendieck. Contenu. skyscraper : {X : TopCat} → \n",
+ " (p₀ : ↑ X) → \n",
+ " [(U : TopologicalSpace. Opens ↑ X) → Decidable (p₀ ∈ U)] → \n",
+ " {C : Type u_2} → \n",
+ " [inst : CategoryTheory. Category. {u_1, u_2} C] → [CategoryTheory. Limits. HasTerminal C] → C → TopCat. Presheaf C X \n",
+ "
# check @ Grothendieck. Contenu. stalkIsoOfMemClosure @ Grothendieck. Contenu. stalkIsoOfMemClosure : {X : TopCat} → \n",
+ " (p₀ : ↑ X) → \n",
+ " [inst : (U : TopologicalSpace. Opens ↑ X) → Decidable (p₀ ∈ U)] → \n",
+ " {C : Type u_2} → \n",
+ " [inst_1 : CategoryTheory. Category. {u_1, u_2} C] → \n",
+ " [inst_2 : CategoryTheory. Limits. HasTerminal C] → \n",
+ " [inst_3 : CategoryTheory. Limits. HasColimits C] → \n",
+ " (A : C) → {y : ↑ X} → y ∈ closure {p₀} → ((Grothendieck. Contenu. skyscraper p₀ A). stalk y ≅ A) \n",
+ "
# check @ Grothendieck. Contenu. stalkIsoOfNotMemClosure @ Grothendieck. Contenu. stalkIsoOfNotMemClosure : {X : TopCat} → \n",
+ " (p₀ : ↑ X) → \n",
+ " [inst : (U : TopologicalSpace. Opens ↑ X) → Decidable (p₀ ∈ U)] → \n",
+ " {C : Type u_2} → \n",
+ " [inst_1 : CategoryTheory. Category. {u_1, u_2} C] → \n",
+ " [inst_2 : CategoryTheory. Limits. HasTerminal C] → \n",
+ " [inst_3 : CategoryTheory. Limits. HasColimits C] → \n",
+ " (A : C) → {y : ↑ X} → y ∉ closure {p₀} → ((Grothendieck. Contenu. skyscraper p₀ A). stalk y ≅ ⊤_ C) \n",
+ "
# check @ Grothendieck. Contenu. support_skyscraper @ Grothendieck. Contenu. support_skyscraper : ∀ {X : TopCat} (p₀ : ↑ X)\n",
+ " [inst : (U : TopologicalSpace. Opens ↑ X) → Decidable (p₀ ∈ U)] {C : Type u_2}\n",
+ " [inst_1 : CategoryTheory. Category. {u_1, u_2} C] [inst_2 : CategoryTheory. Limits. HasTerminal C]\n",
+ " [inst_3 : CategoryTheory. Limits. HasColimits C] (A : C),\n",
+ " IsEmpty (CategoryTheory. Limits. IsTerminal A) → \n",
+ " Grothendieck. Contenu. support (Grothendieck. Contenu. skyscraper p₀ A) = closure {p₀} \n",
+ "
# check @ Grothendieck. Contenu. support_skyscraper_of_closed @ Grothendieck. Contenu. support_skyscraper_of_closed : ∀ {X : TopCat} (p₀ : ↑ X)\n",
+ " [inst : (U : TopologicalSpace. Opens ↑ X) → Decidable (p₀ ∈ U)] {C : Type u_2}\n",
+ " [inst_1 : CategoryTheory. Category. {u_1, u_2} C] [inst_2 : CategoryTheory. Limits. HasTerminal C]\n",
+ " [inst_3 : CategoryTheory. Limits. HasColimits C] (A : C),\n",
+ " IsEmpty (CategoryTheory. Limits. IsTerminal A) → \n",
+ " IsClosed {p₀} → Grothendieck. Contenu. support (Grothendieck. Contenu. skyscraper p₀ A) = {p₀} \n",
+ "
# check @ Grothendieck. Contenu. stalk_dichotomy @ Grothendieck. Contenu. stalk_dichotomy : ∀ {X : TopCat} (p₀ : ↑ X)\n",
+ " [inst : (U : TopologicalSpace. Opens ↑ X) → Decidable (p₀ ∈ U)] {C : Type u_2}\n",
+ " [inst_1 : CategoryTheory. Category. {u_1, u_2} C] [inst_2 : CategoryTheory. Limits. HasTerminal C]\n",
+ " [inst_3 : CategoryTheory. Limits. HasColimits C] (A : C),\n",
+ " IsEmpty (CategoryTheory. Limits. IsTerminal A) → \n",
+ " ∀ (y : ↑ X),\n",
+ " y ∈ Grothendieck. Contenu. support (Grothendieck. Contenu. skyscraper p₀ A) ∧ \n",
+ " Nonempty ((Grothendieck. Contenu. skyscraper p₀ A). stalk y ≅ A) ∨ \n",
+ " y ∉ Grothendieck. Contenu. support (Grothendieck. Contenu. skyscraper p₀ A) ∧ \n",
+ " Nonempty ((Grothendieck. Contenu. skyscraper p₀ A). stalk y ≅ ⊤_ C) \n",
+ "
\n",
+ "
-- Les résultats pivots restent auditables par le noyau Lean \n",
+ "
# print axioms Grothendieck. opensTopology_subcanonical ' Grothendieck. opensTopology_subcanonical' depends on axioms: [propext, Classical. choice, Quot. sound] \n",
+ "
# print axioms Grothendieck. isSheaf_iff_germSeparated_and_germGluing ' Grothendieck. isSheaf_iff_germSeparated_and_germGluing' depends on axioms: [propext, Classical. choice, Quot. sound] \n",
+ "
# print axioms Grothendieck. Contenu. support_skyscraper ' Grothendieck. Contenu. support_skyscraper' depends on axioms: [propext, Classical. choice, Quot. sound] \n",
+ "
--% env 14 \n",
+ "
\n",
+ "
\n",
+ " Raw input \n",
+ " {\"cmd\": \"-- SpacesMathlib : le site construit dans le lake co\\u00efncide avec celui de Mathlib\\n#check @Grothendieck.opensTopology_eq\\n#check @Grothendieck.isSheaf_opensTopology_iff\\n#check @Grothendieck.coversTop_opensTopology_iff\\n\\n-- SpacesSubcanonical : tout repr\\u00e9sentable sur le site des ouverts est un faisceau\\n#check @Grothendieck.isSheaf_yoneda_opensTopology\\n#check @Grothendieck.opensTopology_subcanonical\\n\\n-- StalkCharacterization : s\\u00e9paration et recollement se lisent sur les germes\\n#check @Grothendieck.GermSeparated\\n#check @Grothendieck.GermGluing\\n#check @Grothendieck.germ_eq_of_isCompatible\\n#check @Grothendieck.isSheaf_iff_germSeparated_and_germGluing\\n\\n-- Skyscraper : support et dichotomie des tiges autour du point choisi\\n#check @Grothendieck.Contenu.skyscraper\\n#check @Grothendieck.Contenu.stalkIsoOfMemClosure\\n#check @Grothendieck.Contenu.stalkIsoOfNotMemClosure\\n#check @Grothendieck.Contenu.support_skyscraper\\n#check @Grothendieck.Contenu.support_skyscraper_of_closed\\n#check @Grothendieck.Contenu.stalk_dichotomy\\n\\n-- Les r\\u00e9sultats pivots restent auditables par le noyau Lean\\n#print axioms Grothendieck.opensTopology_subcanonical\\n#print axioms Grothendieck.isSheaf_iff_germSeparated_and_germGluing\\n#print axioms Grothendieck.Contenu.support_skyscraper\", \"env\": 13}\n",
+ " \n",
+ "
\n",
+ " Raw output \n",
+ " {\"messages\":\r\n",
+ " [{\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 2, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 2, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.opensTopology_eq : ∀ (T : Type u_1) [inst : TopologicalSpace T],\\n Grothendieck.opensTopology T = Opens.grothendieckTopology T\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 3, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 3, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.isSheaf_opensTopology_iff : ∀ {T : Type u_1} [inst : TopologicalSpace T] {C : Type u_2}\\n [inst_1 : CategoryTheory.Category.{u_3, u_2} C] (F : TopCat.Presheaf C (TopCat.of T)),\\n CategoryTheory.Presheaf.IsSheaf (Grothendieck.opensTopology T) F ↔ F.IsSheaf\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 4, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 4, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.coversTop_opensTopology_iff : ∀ {T : Type u_1} [inst : TopologicalSpace T] {ι : Type u_2}\\n (U : ι → TopologicalSpace.Opens T),\\n (Grothendieck.opensTopology T).CoversTop U ↔ (Opens.grothendieckTopology T).CoversTop U\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 7, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 7, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.isSheaf_yoneda_opensTopology : ∀ (T : Type u_1) [inst : TopologicalSpace T] (U : TopologicalSpace.Opens T),\\n CategoryTheory.Presieve.IsSheaf (Grothendieck.opensTopology T) (CategoryTheory.yoneda.obj U)\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 8, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 8, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.opensTopology_subcanonical : ∀ (T : Type u_1) [inst : TopologicalSpace T],\\n (Grothendieck.opensTopology T).Subcanonical\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 11, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 11, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.GermSeparated : (T : Type u_1) →\\n [inst : TopologicalSpace T] → TopCat.Presheaf (Type u_1) (TopCat.of T) → Prop\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 12, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 12, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.GermGluing : (T : Type u_1) → [inst : TopologicalSpace T] → TopCat.Presheaf (Type u_1) (TopCat.of T) → Prop\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 13, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 13, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.germ_eq_of_isCompatible : ∀ (T : Type u_1) [inst : TopologicalSpace T]\\n (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) {ι : Type u_2} (U : ι → TopologicalSpace.Opens T)\\n (sf : (i : ι) → F.obj (Opposite.op (U i))),\\n F.IsCompatible U sf →\\n ∀ {i j : ι} {x : T} (hi : x ∈ U i) (hj : x ∈ U j),\\n (CategoryTheory.ConcreteCategory.hom (F.germ (U i) x hi)) (sf i) =\\n (CategoryTheory.ConcreteCategory.hom (F.germ (U j) x hj)) (sf j)\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 14, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 14, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.isSheaf_iff_germSeparated_and_germGluing : ∀ (T : Type u_1) [inst : TopologicalSpace T]\\n (F : TopCat.Presheaf (Type u_1) (TopCat.of T)),\\n F.IsSheaf ↔ Grothendieck.GermSeparated T F ∧ Grothendieck.GermGluing T F\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 17, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 17, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.skyscraper : {X : TopCat} →\\n (p₀ : ↑X) →\\n [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →\\n {C : Type u_2} →\\n [inst : CategoryTheory.Category.{u_1, u_2} C] → [CategoryTheory.Limits.HasTerminal C] → C → TopCat.Presheaf C X\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 18, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 18, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.stalkIsoOfMemClosure : {X : TopCat} →\\n (p₀ : ↑X) →\\n [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →\\n {C : Type u_2} →\\n [inst_1 : CategoryTheory.Category.{u_1, u_2} C] →\\n [inst_2 : CategoryTheory.Limits.HasTerminal C] →\\n [inst_3 : CategoryTheory.Limits.HasColimits C] →\\n (A : C) → {y : ↑X} → y ∈ closure {p₀} → ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ A)\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 19, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 19, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.stalkIsoOfNotMemClosure : {X : TopCat} →\\n (p₀ : ↑X) →\\n [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →\\n {C : Type u_2} →\\n [inst_1 : CategoryTheory.Category.{u_1, u_2} C] →\\n [inst_2 : CategoryTheory.Limits.HasTerminal C] →\\n [inst_3 : CategoryTheory.Limits.HasColimits C] →\\n (A : C) → {y : ↑X} → y ∉ closure {p₀} → ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ ⊤_ C)\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 20, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 20, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.support_skyscraper : ∀ {X : TopCat} (p₀ : ↑X)\\n [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_2}\\n [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]\\n [inst_3 : CategoryTheory.Limits.HasColimits C] (A : C),\\n IsEmpty (CategoryTheory.Limits.IsTerminal A) →\\n Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) = closure {p₀}\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 21, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 21, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.support_skyscraper_of_closed : ∀ {X : TopCat} (p₀ : ↑X)\\n [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_2}\\n [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]\\n [inst_3 : CategoryTheory.Limits.HasColimits C] (A : C),\\n IsEmpty (CategoryTheory.Limits.IsTerminal A) →\\n IsClosed {p₀} → Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) = {p₀}\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 22, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 22, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.stalk_dichotomy : ∀ {X : TopCat} (p₀ : ↑X)\\n [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_2}\\n [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]\\n [inst_3 : CategoryTheory.Limits.HasColimits C] (A : C),\\n IsEmpty (CategoryTheory.Limits.IsTerminal A) →\\n ∀ (y : ↑X),\\n y ∈ Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) ∧\\n Nonempty ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ A) ∨\\n y ∉ Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) ∧\\n Nonempty ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ ⊤_ C)\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 25, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 25, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"'Grothendieck.opensTopology_subcanonical' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 26, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 26, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"'Grothendieck.isSheaf_iff_germSeparated_and_germGluing' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 27, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 27, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"'Grothendieck.Contenu.support_skyscraper' depends on axioms: [propext, Classical.choice, Quot.sound]\"}],\r\n",
+ " \"env\": 14}\n",
+ " \n",
+ " "
+ ],
+ "text/plain": [
+ "-- SpacesMathlib : le site construit dans le lake coïncide avec celui de Mathlib\n",
+ "#check @Grothendieck.opensTopology_eq\n",
+ "──────▶ Grothendieck.opensTopology_eq : ∀ (T : Type u_1) [inst : TopologicalSpace T],\n",
+ " Grothendieck.opensTopology T = Opens.grothendieckTopology T\n",
+ "#check @Grothendieck.isSheaf_opensTopology_iff\n",
+ "──────▶ @Grothendieck.isSheaf_opensTopology_iff : ∀ {T : Type u_1} [inst : TopologicalSpace T] {C : Type u_2}\n",
+ " [inst_1 : CategoryTheory.Category.{u_3, u_2} C] (F : TopCat.Presheaf C (TopCat.of T)),\n",
+ " CategoryTheory.Presheaf.IsSheaf (Grothendieck.opensTopology T) F ↔ F.IsSheaf\n",
+ "#check @Grothendieck.coversTop_opensTopology_iff\n",
+ "──────▶ @Grothendieck.coversTop_opensTopology_iff : ∀ {T : Type u_1} [inst : TopologicalSpace T] {ι : Type u_2}\n",
+ " (U : ι → TopologicalSpace.Opens T),\n",
+ " (Grothendieck.opensTopology T).CoversTop U ↔ (Opens.grothendieckTopology T).CoversTop U\n",
+ "\n",
+ "-- SpacesSubcanonical : tout représentable sur le site des ouverts est un faisceau\n",
+ "#check @Grothendieck.isSheaf_yoneda_opensTopology\n",
+ "──────▶ Grothendieck.isSheaf_yoneda_opensTopology : ∀ (T : Type u_1) [inst : TopologicalSpace T] (U : TopologicalSpace.Opens T),\n",
+ " CategoryTheory.Presieve.IsSheaf (Grothendieck.opensTopology T) (CategoryTheory.yoneda.obj U)\n",
+ "#check @Grothendieck.opensTopology_subcanonical\n",
+ "──────▶ Grothendieck.opensTopology_subcanonical : ∀ (T : Type u_1) [inst : TopologicalSpace T],\n",
+ " (Grothendieck.opensTopology T).Subcanonical\n",
+ "\n",
+ "-- StalkCharacterization : séparation et recollement se lisent sur les germes\n",
+ "#check @Grothendieck.GermSeparated\n",
+ "──────▶ Grothendieck.GermSeparated : (T : Type u_1) →\n",
+ " [inst : TopologicalSpace T] → TopCat.Presheaf (Type u_1) (TopCat.of T) → Prop\n",
+ "#check @Grothendieck.GermGluing\n",
+ "──────▶ Grothendieck.GermGluing : (T : Type u_1) → [inst : TopologicalSpace T] → TopCat.Presheaf (Type u_1) (TopCat.of T) → Prop\n",
+ "#check @Grothendieck.germ_eq_of_isCompatible\n",
+ "──────▶ Grothendieck.germ_eq_of_isCompatible : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
+ " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) {ι : Type u_2} (U : ι → TopologicalSpace.Opens T)\n",
+ " (sf : (i : ι) → F.obj (Opposite.op (U i))),\n",
+ " F.IsCompatible U sf →\n",
+ " ∀ {i j : ι} {x : T} (hi : x ∈ U i) (hj : x ∈ U j),\n",
+ " (CategoryTheory.ConcreteCategory.hom (F.germ (U i) x hi)) (sf i) =\n",
+ " (CategoryTheory.ConcreteCategory.hom (F.germ (U j) x hj)) (sf j)\n",
+ "#check @Grothendieck.isSheaf_iff_germSeparated_and_germGluing\n",
+ "──────▶ Grothendieck.isSheaf_iff_germSeparated_and_germGluing : ∀ (T : Type u_1) [inst : TopologicalSpace T]\n",
+ " (F : TopCat.Presheaf (Type u_1) (TopCat.of T)),\n",
+ " F.IsSheaf ↔ Grothendieck.GermSeparated T F ∧ Grothendieck.GermGluing T F\n",
+ "\n",
+ "-- Skyscraper : support et dichotomie des tiges autour du point choisi\n",
+ "#check @Grothendieck.Contenu.skyscraper\n",
+ "──────▶ @Grothendieck.Contenu.skyscraper : {X : TopCat} →\n",
+ " (p₀ : ↑X) →\n",
+ " [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →\n",
+ " {C : Type u_2} →\n",
+ " [inst : CategoryTheory.Category.{u_1, u_2} C] → [CategoryTheory.Limits.HasTerminal C] → C → TopCat.Presheaf C X\n",
+ "#check @Grothendieck.Contenu.stalkIsoOfMemClosure\n",
+ "──────▶ @Grothendieck.Contenu.stalkIsoOfMemClosure : {X : TopCat} →\n",
+ " (p₀ : ↑X) →\n",
+ " [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →\n",
+ " {C : Type u_2} →\n",
+ " [inst_1 : CategoryTheory.Category.{u_1, u_2} C] →\n",
+ " [inst_2 : CategoryTheory.Limits.HasTerminal C] →\n",
+ " [inst_3 : CategoryTheory.Limits.HasColimits C] →\n",
+ " (A : C) → {y : ↑X} → y ∈ closure {p₀} → ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ A)\n",
+ "#check @Grothendieck.Contenu.stalkIsoOfNotMemClosure\n",
+ "──────▶ @Grothendieck.Contenu.stalkIsoOfNotMemClosure : {X : TopCat} →\n",
+ " (p₀ : ↑X) →\n",
+ " [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →\n",
+ " {C : Type u_2} →\n",
+ " [inst_1 : CategoryTheory.Category.{u_1, u_2} C] →\n",
+ " [inst_2 : CategoryTheory.Limits.HasTerminal C] →\n",
+ " [inst_3 : CategoryTheory.Limits.HasColimits C] →\n",
+ " (A : C) → {y : ↑X} → y ∉ closure {p₀} → ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ ⊤_ C)\n",
+ "#check @Grothendieck.Contenu.support_skyscraper\n",
+ "──────▶ @Grothendieck.Contenu.support_skyscraper : ∀ {X : TopCat} (p₀ : ↑X)\n",
+ " [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_2}\n",
+ " [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]\n",
+ " [inst_3 : CategoryTheory.Limits.HasColimits C] (A : C),\n",
+ " IsEmpty (CategoryTheory.Limits.IsTerminal A) →\n",
+ " Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) = closure {p₀}\n",
+ "#check @Grothendieck.Contenu.support_skyscraper_of_closed\n",
+ "──────▶ @Grothendieck.Contenu.support_skyscraper_of_closed : ∀ {X : TopCat} (p₀ : ↑X)\n",
+ " [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_2}\n",
+ " [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]\n",
+ " [inst_3 : CategoryTheory.Limits.HasColimits C] (A : C),\n",
+ " IsEmpty (CategoryTheory.Limits.IsTerminal A) →\n",
+ " IsClosed {p₀} → Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) = {p₀}\n",
+ "#check @Grothendieck.Contenu.stalk_dichotomy\n",
+ "──────▶ @Grothendieck.Contenu.stalk_dichotomy : ∀ {X : TopCat} (p₀ : ↑X)\n",
+ " [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_2}\n",
+ " [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]\n",
+ " [inst_3 : CategoryTheory.Limits.HasColimits C] (A : C),\n",
+ " IsEmpty (CategoryTheory.Limits.IsTerminal A) →\n",
+ " ∀ (y : ↑X),\n",
+ " y ∈ Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) ∧\n",
+ " Nonempty ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ A) ∨\n",
+ " y ∉ Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) ∧\n",
+ " Nonempty ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ ⊤_ C)\n",
+ "\n",
+ "-- Les résultats pivots restent auditables par le noyau Lean\n",
+ "#print axioms Grothendieck.opensTopology_subcanonical\n",
+ "──────▶ 'Grothendieck.opensTopology_subcanonical' depends on axioms: [propext, Classical.choice, Quot.sound]\n",
+ "#print axioms Grothendieck.isSheaf_iff_germSeparated_and_germGluing\n",
+ "──────▶ 'Grothendieck.isSheaf_iff_germSeparated_and_germGluing' depends on axioms: [propext, Classical.choice, Quot.sound]\n",
+ "#print axioms Grothendieck.Contenu.support_skyscraper\n",
+ "──────▶ 'Grothendieck.Contenu.support_skyscraper' depends on axioms: [propext, Classical.choice, Quot.sound]\n",
+ "--% env 14\n",
+ "\n",
+ "Raw input:\n",
+ "{\"cmd\": \"-- SpacesMathlib : le site construit dans le lake co\\u00efncide avec celui de Mathlib\\n#check @Grothendieck.opensTopology_eq\\n#check @Grothendieck.isSheaf_opensTopology_iff\\n#check @Grothendieck.coversTop_opensTopology_iff\\n\\n-- SpacesSubcanonical : tout repr\\u00e9sentable sur le site des ouverts est un faisceau\\n#check @Grothendieck.isSheaf_yoneda_opensTopology\\n#check @Grothendieck.opensTopology_subcanonical\\n\\n-- StalkCharacterization : s\\u00e9paration et recollement se lisent sur les germes\\n#check @Grothendieck.GermSeparated\\n#check @Grothendieck.GermGluing\\n#check @Grothendieck.germ_eq_of_isCompatible\\n#check @Grothendieck.isSheaf_iff_germSeparated_and_germGluing\\n\\n-- Skyscraper : support et dichotomie des tiges autour du point choisi\\n#check @Grothendieck.Contenu.skyscraper\\n#check @Grothendieck.Contenu.stalkIsoOfMemClosure\\n#check @Grothendieck.Contenu.stalkIsoOfNotMemClosure\\n#check @Grothendieck.Contenu.support_skyscraper\\n#check @Grothendieck.Contenu.support_skyscraper_of_closed\\n#check @Grothendieck.Contenu.stalk_dichotomy\\n\\n-- Les r\\u00e9sultats pivots restent auditables par le noyau Lean\\n#print axioms Grothendieck.opensTopology_subcanonical\\n#print axioms Grothendieck.isSheaf_iff_germSeparated_and_germGluing\\n#print axioms Grothendieck.Contenu.support_skyscraper\", \"env\": 13}\n",
+ "Raw output:\n",
+ "{\"messages\":\r\n",
+ " [{\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 2, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 2, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.opensTopology_eq : ∀ (T : Type u_1) [inst : TopologicalSpace T],\\n Grothendieck.opensTopology T = Opens.grothendieckTopology T\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 3, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 3, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.isSheaf_opensTopology_iff : ∀ {T : Type u_1} [inst : TopologicalSpace T] {C : Type u_2}\\n [inst_1 : CategoryTheory.Category.{u_3, u_2} C] (F : TopCat.Presheaf C (TopCat.of T)),\\n CategoryTheory.Presheaf.IsSheaf (Grothendieck.opensTopology T) F ↔ F.IsSheaf\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 4, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 4, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.coversTop_opensTopology_iff : ∀ {T : Type u_1} [inst : TopologicalSpace T] {ι : Type u_2}\\n (U : ι → TopologicalSpace.Opens T),\\n (Grothendieck.opensTopology T).CoversTop U ↔ (Opens.grothendieckTopology T).CoversTop U\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 7, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 7, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.isSheaf_yoneda_opensTopology : ∀ (T : Type u_1) [inst : TopologicalSpace T] (U : TopologicalSpace.Opens T),\\n CategoryTheory.Presieve.IsSheaf (Grothendieck.opensTopology T) (CategoryTheory.yoneda.obj U)\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 8, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 8, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.opensTopology_subcanonical : ∀ (T : Type u_1) [inst : TopologicalSpace T],\\n (Grothendieck.opensTopology T).Subcanonical\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 11, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 11, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.GermSeparated : (T : Type u_1) →\\n [inst : TopologicalSpace T] → TopCat.Presheaf (Type u_1) (TopCat.of T) → Prop\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 12, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 12, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.GermGluing : (T : Type u_1) → [inst : TopologicalSpace T] → TopCat.Presheaf (Type u_1) (TopCat.of T) → Prop\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 13, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 13, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.germ_eq_of_isCompatible : ∀ (T : Type u_1) [inst : TopologicalSpace T]\\n (F : TopCat.Presheaf (Type u_1) (TopCat.of T)) {ι : Type u_2} (U : ι → TopologicalSpace.Opens T)\\n (sf : (i : ι) → F.obj (Opposite.op (U i))),\\n F.IsCompatible U sf →\\n ∀ {i j : ι} {x : T} (hi : x ∈ U i) (hj : x ∈ U j),\\n (CategoryTheory.ConcreteCategory.hom (F.germ (U i) x hi)) (sf i) =\\n (CategoryTheory.ConcreteCategory.hom (F.germ (U j) x hj)) (sf j)\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 14, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 14, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Grothendieck.isSheaf_iff_germSeparated_and_germGluing : ∀ (T : Type u_1) [inst : TopologicalSpace T]\\n (F : TopCat.Presheaf (Type u_1) (TopCat.of T)),\\n F.IsSheaf ↔ Grothendieck.GermSeparated T F ∧ Grothendieck.GermGluing T F\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 17, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 17, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.skyscraper : {X : TopCat} →\\n (p₀ : ↑X) →\\n [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →\\n {C : Type u_2} →\\n [inst : CategoryTheory.Category.{u_1, u_2} C] → [CategoryTheory.Limits.HasTerminal C] → C → TopCat.Presheaf C X\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 18, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 18, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.stalkIsoOfMemClosure : {X : TopCat} →\\n (p₀ : ↑X) →\\n [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →\\n {C : Type u_2} →\\n [inst_1 : CategoryTheory.Category.{u_1, u_2} C] →\\n [inst_2 : CategoryTheory.Limits.HasTerminal C] →\\n [inst_3 : CategoryTheory.Limits.HasColimits C] →\\n (A : C) → {y : ↑X} → y ∈ closure {p₀} → ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ A)\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 19, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 19, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.stalkIsoOfNotMemClosure : {X : TopCat} →\\n (p₀ : ↑X) →\\n [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →\\n {C : Type u_2} →\\n [inst_1 : CategoryTheory.Category.{u_1, u_2} C] →\\n [inst_2 : CategoryTheory.Limits.HasTerminal C] →\\n [inst_3 : CategoryTheory.Limits.HasColimits C] →\\n (A : C) → {y : ↑X} → y ∉ closure {p₀} → ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ ⊤_ C)\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 20, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 20, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.support_skyscraper : ∀ {X : TopCat} (p₀ : ↑X)\\n [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_2}\\n [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]\\n [inst_3 : CategoryTheory.Limits.HasColimits C] (A : C),\\n IsEmpty (CategoryTheory.Limits.IsTerminal A) →\\n Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) = closure {p₀}\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 21, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 21, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.support_skyscraper_of_closed : ∀ {X : TopCat} (p₀ : ↑X)\\n [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_2}\\n [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]\\n [inst_3 : CategoryTheory.Limits.HasColimits C] (A : C),\\n IsEmpty (CategoryTheory.Limits.IsTerminal A) →\\n IsClosed {p₀} → Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) = {p₀}\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 22, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 22, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"@Grothendieck.Contenu.stalk_dichotomy : ∀ {X : TopCat} (p₀ : ↑X)\\n [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_2}\\n [inst_1 : CategoryTheory.Category.{u_1, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]\\n [inst_3 : CategoryTheory.Limits.HasColimits C] (A : C),\\n IsEmpty (CategoryTheory.Limits.IsTerminal A) →\\n ∀ (y : ↑X),\\n y ∈ Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) ∧\\n Nonempty ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ A) ∨\\n y ∉ Grothendieck.Contenu.support (Grothendieck.Contenu.skyscraper p₀ A) ∧\\n Nonempty ((Grothendieck.Contenu.skyscraper p₀ A).stalk y ≅ ⊤_ C)\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 25, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 25, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"'Grothendieck.opensTopology_subcanonical' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 26, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 26, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"'Grothendieck.isSheaf_iff_germSeparated_and_germGluing' depends on axioms: [propext, Classical.choice, Quot.sound]\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 27, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 27, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"'Grothendieck.Contenu.support_skyscraper' depends on axioms: [propext, Classical.choice, Quot.sound]\"}],\r\n",
+ " \"env\": 14}"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "-- SpacesMathlib : le site construit dans le lake coïncide avec celui de Mathlib\n",
+ "#check @Grothendieck.opensTopology_eq\n",
+ "#check @Grothendieck.isSheaf_opensTopology_iff\n",
+ "#check @Grothendieck.coversTop_opensTopology_iff\n",
+ "\n",
+ "-- SpacesSubcanonical : tout représentable sur le site des ouverts est un faisceau\n",
+ "#check @Grothendieck.isSheaf_yoneda_opensTopology\n",
+ "#check @Grothendieck.opensTopology_subcanonical\n",
+ "\n",
+ "-- StalkCharacterization : séparation et recollement se lisent sur les germes\n",
+ "#check @Grothendieck.GermSeparated\n",
+ "#check @Grothendieck.GermGluing\n",
+ "#check @Grothendieck.germ_eq_of_isCompatible\n",
+ "#check @Grothendieck.isSheaf_iff_germSeparated_and_germGluing\n",
+ "\n",
+ "-- Skyscraper : support et dichotomie des tiges autour du point choisi\n",
+ "#check @Grothendieck.Contenu.skyscraper\n",
+ "#check @Grothendieck.Contenu.stalkIsoOfMemClosure\n",
+ "#check @Grothendieck.Contenu.stalkIsoOfNotMemClosure\n",
+ "#check @Grothendieck.Contenu.support_skyscraper\n",
+ "#check @Grothendieck.Contenu.support_skyscraper_of_closed\n",
+ "#check @Grothendieck.Contenu.stalk_dichotomy\n",
+ "\n",
+ "-- Les résultats pivots restent auditables par le noyau Lean\n",
+ "#print axioms Grothendieck.opensTopology_subcanonical\n",
+ "#print axioms Grothendieck.isSheaf_iff_germSeparated_and_germGluing\n",
+ "#print axioms Grothendieck.Contenu.support_skyscraper"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "c8a3b365",
+ "metadata": {
+ "papermill": {
+ "duration": 0.009009,
+ "end_time": "2026-09-20T09:10:48.171940+00:00",
+ "exception": false,
+ "start_time": "2026-09-20T09:10:48.162931+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "source": [
+ "### Lecture du résultat\n",
+ "\n",
+ "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`).\n",
+ "\n",
+ "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."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "f3d749b9",
+ "metadata": {
+ "papermill": {
+ "duration": 0.009368,
+ "end_time": "2026-09-20T09:10:48.189798+00:00",
+ "exception": false,
+ "start_time": "2026-09-20T09:10:48.180430+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "source": [
+ "### Exercice — retrouver la concentration au point fermé\n",
+ "\n",
+ "**Objectif.** Identifier le corollaire qui réduit le support du préfaisceau gratte-ciel au singleton du point lorsque celui-ci est fermé.\n",
+ "\n",
+ "1. Repérez la déclaration dont le nom prolonge `support_skyscraper`.\n",
+ "2. Comparez son hypothèse de fermeture avec celle du théorème général.\n",
+ "3. Décommentez le `#check`, puis ajoutez sous le message exécutable une micro-preuve qui applique ce corollaire dans un contexte de votre choix."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "id": "c359c91e",
+ "metadata": {
+ "execution": {
+ "iopub.execute_input": "2026-09-20T09:10:48.208323Z",
+ "iopub.status.busy": "2026-09-20T09:10:48.208131Z",
+ "iopub.status.idle": "2026-09-20T09:10:48.395441Z",
+ "shell.execute_reply": "2026-09-20T09:10:48.394448Z"
+ },
+ "papermill": {
+ "duration": 0.197638,
+ "end_time": "2026-09-20T09:10:48.396064+00:00",
+ "exception": false,
+ "start_time": "2026-09-20T09:10:48.198426+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/html": [
+ "\n",
+ " \n",
+ "
\n",
+ "
\n",
+ "
\n",
+ " \n",
+ " \n",
+ " \n",
+ "
\n",
+ "
-- 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" "Exercice a completer : instancier le corollaire pour un point ferme" \n",
+ "
--% env 15 \n",
+ "
\n",
+ "
\n",
+ " Raw input \n",
+ " {\"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}\n",
+ " \n",
+ "
\n",
+ " Raw output \n",
+ " {\"messages\":\r\n",
+ " [{\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 8, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 8, \"column\": 5},\r\n",
+ " \"data\":\r\n",
+ " \"\\\"Exercice a completer : instancier le corollaire pour un point ferme\\\"\"}],\r\n",
+ " \"env\": 15}\n",
+ " \n",
+ " "
+ ],
+ "text/plain": [
+ "-- 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\"\n",
+ "─────▶ \"Exercice a completer : instancier le corollaire pour un point ferme\"\n",
+ "--% env 15\n",
+ "\n",
+ "Raw input:\n",
+ "{\"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}\n",
+ "Raw output:\n",
+ "{\"messages\":\r\n",
+ " [{\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 8, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 8, \"column\": 5},\r\n",
+ " \"data\":\r\n",
+ " \"\\\"Exercice a completer : instancier le corollaire pour un point ferme\\\"\"}],\r\n",
+ " \"env\": 15}"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "-- 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\""
+ ]
+ },
{
"cell_type": "markdown",
"id": "6f06ac85",
"metadata": {
"papermill": {
- "duration": 0.006462,
- "end_time": "2026-09-07T11:09:55.397724+00:00",
+ "duration": 0.009878,
+ "end_time": "2026-09-20T09:10:48.414579+00:00",
"exception": false,
- "start_time": "2026-09-07T11:09:55.391262+00:00",
+ "start_time": "2026-09-20T09:10:48.404701+00:00",
"status": "completed"
},
"tags": []
@@ -4149,10 +4748,22 @@
"name": "lean4-wsl"
},
"language_info": {
- "codemirror_mode": "python",
+ "codemirror_mode": "lean4",
"file_extension": ".lean",
"mimetype": "text/x-lean4",
"name": "lean4"
+ },
+ "papermill": {
+ "default_parameters": {},
+ "duration": 236.082829,
+ "end_time": "2026-09-20T09:10:51.736274+00:00",
+ "environment_variables": {},
+ "exception": null,
+ "input_path": "Lean-15c-Lean-Grothendieck-Companion.ipynb",
+ "output_path": "Lean-15c-Lean-Grothendieck-Companion.ipynb",
+ "parameters": {},
+ "start_time": "2026-09-20T09:06:55.653445+00:00",
+ "version": "2.7.0"
}
},
"nbformat": 4,