noncomputable def TopCat.Sheaf.sectionsAt (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} (U : TopologicalSpace.Opens ↑X) : CategoryTheory.Functor (Sheaf C X) C

The functor sending a sheaf to its sections over a fixed open U.

theorem noetherianSpace_sectionsAt_preservesFilteredColimits (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} [TopologicalSpace.NoetherianSpace ↑X] (U : TopologicalSpace.Opens ↑X) : CategoryTheory.Limits.PreservesFilteredColimits (TopCat.Sheaf.sectionsAt C U)

On a Noetherian space, the sectionsAt U functor preserves filtered colimits (Lem 22, Lec 12).

noncomputable def noetherianSpace_colimit_sections_iso (C : Type u) [CategoryTheory.Category.{v, u} C] {X : TopCat} [TopologicalSpace.NoetherianSpace ↑X] (U : TopologicalSpace.Opens ↑X) {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (TopCat.Sheaf C X)) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasColimit (F.comp (TopCat.Sheaf.sectionsAt C U))] : (TopCat.Sheaf.sectionsAt C U).obj (CategoryTheory.Limits.colimit F) ≅ CategoryTheory.Limits.colimit (F.comp (TopCat.Sheaf.sectionsAt C U))

Over a Noetherian space, sections of a filtered colimit of sheaves at U agree with the colimit of the sections at U.