CategoryTheory.Sheaf.isSheaf_of_isLimit

theorem CategoryTheory.Sheaf.isSheaf_of_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [inst_1 : CategoryTheory.Category.{w', w} D] {K : Type z} [inst_2 : CategoryTheory.Category.{z', z} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K D] (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)) (E : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.sheafToPresheaf J D))), CategoryTheory.Limits.IsLimit E → CategoryTheory.Presheaf.IsSheaf J E.pt

The theorem `CategoryTheory.Sheaf.isSheaf_of_isLimit` states that if `E` is a cone which represents a limit in the category of presheaves, then the limit presheaf represented by `E` is also a sheaf. This theorem is important because it is used to show that the forgetful functor, which maps from the category of sheaves to the category of presheaves, creates limits. In other words, the process of forgetting extra structure from a sheaf to a presheaf preserves the limit property. This theorem holds for any Grothendieck topology `J` on a category `C` and for any category `D` with limits of shape `K`.

More concisely: If a cone `E` represents a limit in the category of presheaves over a Grothendieck topology `J` on a category `C`, then the limit presheaf represented by `E` is a sheaf.