English
If a diagram F: J ⥤ Presheaf C X is such that each F.obj j is a sheaf, and c: Cone F is a limit, then the underlying presheaf of the limit cone is a sheaf.
Русский
Если диаграмма F: J ⥤ Presheaf C X такова, что каждый F(j) является пучком, и c является пределом, то предшествующая пучковая структура предела тоже является пучком.
LaTeX
$$$ [HasLimitsOfShape J C] \\; \\forall X,\\; \\forall F: J \\to Presheaf\\; C\\; X,\\; (\\forall j, (F.obj j).IsSheaf) \\Rightarrow (\\mathrm{limit}\\; F).IsSheaf. $$$
Lean4
theorem isSheaf_of_isLimit [HasLimitsOfShape J C] {X : TopCat} (F : J ⥤ Presheaf.{v} C X) (H : ∀ j, (F.obj j).IsSheaf)
{c : Cone F} (hc : IsLimit c) : c.pt.IsSheaf :=
by
let F' : J ⥤ Sheaf C X :=
{ obj := fun j => ⟨F.obj j, H j⟩
map := fun f => ⟨F.map f⟩ }
let e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents fun _ => Iso.refl _
exact
Presheaf.isSheaf_of_iso ((isLimitOfPreserves (Sheaf.forget C X) (limit.isLimit F')).conePointsIsoOfNatIso hc e)
(limit F').2
