instance
TopCat.Sheaf.hasColimitsOfShape_of_hasWeakSheafify
{C : Type (u + 1)}
[CategoryTheory.Category.{u, u + 1} C]
{J : Type w}
[CategoryTheory.SmallCategory J]
{X : TopCat}
[CategoryTheory.Limits.HasColimitsOfShape J C]
[CategoryTheory.HasWeakSheafify (Opens.grothendieckTopology ↑X) C]
:
If the target category C has J-shaped colimits and weak sheafification, then the
category of C-valued sheaves on X also has J-shaped colimits.
theorem
noetherian_filtered_colimit_presheaf_isSheaf
{C : Type (u + 1)}
[CategoryTheory.Category.{u, u + 1} C]
{J : Type w}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
{X : TopCat}
[TopologicalSpace.NoetherianSpace ↑X]
[CategoryTheory.Limits.HasColimitsOfShape J C]
(F : CategoryTheory.Functor J (TopCat.Sheaf C X))
(c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf (Opens.grothendieckTopology ↑X) C)))
(hc : CategoryTheory.Limits.IsColimit c)
:
On a Noetherian space, a filtered colimit of sheaves, computed at the level of presheaves, is again a sheaf (the key sheaf-theoretic content of Lemma 22).
noncomputable def
noetherian_filtered_colimit_sheaf_sections_iso
{C : Type (u + 1)}
[CategoryTheory.Category.{u, u + 1} C]
{J : Type w}
[CategoryTheory.SmallCategory J]
[CategoryTheory.IsFiltered J]
{X : TopCat}
[TopologicalSpace.NoetherianSpace ↑X]
[CategoryTheory.Limits.HasColimitsOfShape J C]
[CategoryTheory.HasWeakSheafify (Opens.grothendieckTopology ↑X) C]
(F : CategoryTheory.Functor J (TopCat.Sheaf C X))
(U : TopologicalSpace.Opens ↑X)
:
((TopCat.Sheaf.forget C X).obj (CategoryTheory.Limits.colimit F)).obj (Opposite.op U) ≅ CategoryTheory.Limits.colimit
(F.comp
((TopCat.Sheaf.forget C X).comp
((CategoryTheory.evaluation (TopologicalSpace.Opens ↑X)ᵒᵖ C).obj (Opposite.op U))))
Lemma 22 (Noetherian): On a Noetherian space, sections of a filtered colimit of sheaves
on an open U are computed as the filtered colimit of sections on U.