noncomputable def TopCat.Sheaf.sectionsAtU {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {J : Type t} [CategoryTheory.Category.{t, t} J] (F : CategoryTheory.Functor J (Sheaf C X)) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : CategoryTheory.Functor J C

The diagram of sections at a fixed open U of a J-shaped diagram of sheaves.

theorem TopCat.Sheaf.filteredColimitPresheafIsSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {J : Type t} [CategoryTheory.Category.{t, t} J] [CategoryTheory.IsFiltered J] [TopologicalSpace.NoetherianSpace ↑X] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J (Sheaf C X)) (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf (Opens.grothendieckTopology ↑X) C))) (hc : CategoryTheory.Limits.IsColimit c) : Presheaf.IsSheaf c.pt

On a Noetherian space, the presheaf colimit of a filtered diagram of sheaves is already a sheaf (Lem 22, Lec 12).

noncomputable def TopCat.Sheaf.sectionsColimitIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {J : Type t} [CategoryTheory.Category.{t, t} J] [CategoryTheory.IsFiltered J] [TopologicalSpace.NoetherianSpace ↑X] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.HasColimitsOfShape J (Sheaf C X)] (F : CategoryTheory.Functor J (Sheaf C X)) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (CategoryTheory.Limits.colimit F).obj.obj U ≅ CategoryTheory.Limits.colimit (sectionsAtU F U)

Over a Noetherian space, sections of the sheaf colimit at any open U agree with the colimit of sections at U (Lem 22, Lec 12).