English
Let K be a coverage on C and P a functor from the opposite of C to some category D. Then P is a sheaf for the Grothendieck topology generated by K if and only if, for every X and every presieve R on X with R ∈ K X, a certain cone built from P has a limit.
Русский
Пусть K — покрытие на C и P — многопротяжный функтор обратно от C в D. Тогда P является sheaf для топологии Гротендейка, порождаемой K, тогда и только тогда, для каждого X и любого предсемени R на X с R ∈ K X, соответствующий конус по P имеет предел.
LaTeX
$$$\\mathrm{IsSheaf}_{K^{\\mathrm{Gro}}}(P) \\iff \\forall X, \\forall R \\in K(X), \\ \\mathrm{Nonempty}(\\mathrm{IsLimit}(P.mapCone(\\mathrm{Sieve.generate R}.arrows.cocone.op)))$$$
Lean4
theorem isSheaf_iff_isLimit_coverage (K : Coverage C) (P : Cᵒᵖ ⥤ D) :
Presheaf.IsSheaf K.toGrothendieck P ↔
∀ ⦃X : C⦄ (R : Presieve X), R ∈ K X → Nonempty (IsLimit (P.mapCone (Sieve.generate R).arrows.cocone.op)) :=
by
simp only [Presheaf.IsSheaf, Presieve.isSheaf_coverage, isLimit_iff_isSheafFor, ← Presieve.isSheafFor_iff_generate]
aesop
