English
Let C be preregular and essentially small. For any functor F from the opposite of C to an arbitrary category A, the regular topology sheaf condition for F is equivalent to the regular topology sheaf condition after transporting F along the equivalence with SmallModel C.
Русский
Пусть C удовлетворяет свойству preregular и является essentially small. Для любого функтора F: C^op → A равносильно условию шарообразности по регулярной топологии после переноса F через эквивалентность с SmallModel C.
LaTeX
$$$\mathrm{IsSheaf}(\mathrm{regularTopology}(C), F) \iff \mathrm{IsSheaf}(\mathrm{regularTopology}(\mathrm{SmallModel}(C)), ((\mathrm{equivSmallModel}(C).inverse.op) \circ F))$$$
Lean4
/-- The regular sheaf condition on an essentially small site can be checked after precomposing with
the equivalence with a small category.
-/
theorem preregular_isSheaf_iff_of_essentiallySmall [EssentiallySmall C] (F : Cᵒᵖ ⥤ A) :
IsSheaf (regularTopology C) F ↔ IsSheaf (regularTopology (SmallModel C)) ((equivSmallModel C).inverse.op ⋙ F) :=
preregular_isSheaf_iff _ _ _
