Colimits of presheafed spaces with sheaf structure presheaves

The structure presheaf of a colimit X of a diagram F of presheafed spaces is the limit of the pushforwards to X of the structure presheaves of the F j (AlgebraicGeometry.PresheafedSpace.colimitCocone). Pushforwards and limits of sheaves are sheaves, so if every F j has a sheaf structure presheaf, so does every colimit of F. This is the statement behind Mathlib's instance that the forgetful functor from sheafed spaces to presheafed spaces creates colimits, phrased for an arbitrary colimit cocone of presheafed spaces, so that it applies to colimits constructed in other categories and transported to presheafed spaces, such as glued spaces.

Main results

• AlgebraicGeometry.PresheafedSpace.isSheaf_of_isColimit: the structure presheaf of a colimit of presheafed spaces whose structure presheaves are sheaves is a sheaf.

theorem AlgebraicGeometry.PresheafedSpace.isSheaf_of_isColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.HasColimitsOfShape J TopCat] [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] (F : CategoryTheory.Functor J (PresheafedSpace C)) (hF : ∀ (j : J), (F.obj j).presheaf.IsSheaf) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) : c.pt.presheaf.IsSheaf

A colimit of sheafed spaces, computed among presheafed spaces, is a sheafed space. If every object of a diagram F of presheafed spaces has a sheaf structure presheaf, then so does the cocone point of every colimit cocone of F: the structure presheaf of the colimit is a limit of pushforwards of sheaves.