theorem
presheaf_colimit_isSheaf_of_noetherian
{X : Type w}
[TopologicalSpace X]
[TopologicalSpace.NoetherianSpace X]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{K : Type u_1}
[CategoryTheory.SmallCategory K]
[CategoryTheory.IsFiltered K]
(F : CategoryTheory.Functor K (CategoryTheory.Sheaf (Opens.grothendieckTopology X) C))
(E : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf (Opens.grothendieckTopology X) C)))
(hE : CategoryTheory.Limits.IsColimit E)
:
Lemma 22 (Lec 6/12): on a Noetherian topological space, the colimit of a filtered diagram of sheaves, taken in the presheaf category, is itself a sheaf.
@[implicit_reducible]
noncomputable def
sheafToPresheaf_createsFilteredColimits_of_noetherian
{X : Type w}
[TopologicalSpace X]
[TopologicalSpace.NoetherianSpace X]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{K : Type u_1}
[CategoryTheory.SmallCategory K]
[CategoryTheory.IsFiltered K]
(F : CategoryTheory.Functor K (CategoryTheory.Sheaf (Opens.grothendieckTopology X) C))
:
On a Noetherian space, the sheafification functor Sheaf → Presheaf creates filtered
colimits.