English
Let F: K ⥤ Sheaf J D be a diagram of J-sheaves and let E be a cone on F composed with the presheaf functor, E is a limit cone; then the apex presheaf E.pt is a sheaf on C with respect to J.
Русский
Пусть F: K ⥤ Шейф J D задаёт диаграмму шейфов J, и E — конус над F ⋙ presheafToPresheaf J D, являющийся пределом; тогда аппекс‑прешейф E.pt является шейфом по топологии J.
LaTeX
$$$F : K \to \mathrm{Sh}(J,D),\ E : \mathrm{Cone}(F \circ \mathrm{sheafToPresheaf}(J,D)),\ hE : \mathrm{IsLimit}(E)\;\Rightarrow\; \mathrm{Presheaf.IsSheaf}(J, E.pt).$$$
Lean4
/-- If `E` is a cone which is a limit on the level of presheaves,
then the limit presheaf is again a sheaf.
This is used to show that the forgetful functor from sheaves to presheaves creates limits.
-/
theorem isSheaf_of_isLimit (F : K ⥤ Sheaf J D) (E : Cone (F ⋙ sheafToPresheaf J D)) (hE : IsLimit E) :
Presheaf.IsSheaf J E.pt := by
rw [Presheaf.isSheaf_iff_multifork]
intro X S
exact ⟨isLimitMultiforkOfIsLimit _ _ hE _ _⟩
