English
Let C be a category, J a Grothendieck topology on C, and A a category with small coproducts, Preadditive structure, and HasWeakSheafify J A. If A has a separator, then the category of J-sheaves with values in A also has a separator.
Русский
Пусть C — категория, J — топология Гротендрика на C, и A — категория с малыми копроизведениями, преддобавитной структурой и слабой шелффикацией по J. Если у A есть разделитель, то категория J-шейфов, значащаяся в A, также имеет разделитель.
LaTeX
$$$\\operatorname{HasSeparator}(\\text{Sh}(J,A))\\quad\\text{whenever}\\quad \\operatorname{HasSeparator}(A),\\, \\text{Preadditive}(A),\\, \\text{HasCoproducts}(A),\\, \\text{HasWeakSheafify}(J,A).$$$
Lean4
instance hasSeparator [HasSeparator A] [Preadditive A] [HasCoproducts.{u} A] : HasSeparator (Sheaf J A) where
hasSeparator := ⟨_, isSeparator J (S := fun (_ : Unit) ↦ separator A) (by simpa using isSeparator_separator A)⟩
