precoherent_isSheaf_iff_of_essentiallySmall

English

For an essentially small C, the coherent sheaf condition transfers to SmallModel(C).

Русский

Для существенно малой C условие шейфности переносится на SmallModel(C).

LaTeX

$$$\text{PrecoherentIsSheaf}_{essentiallySmall}$$$

Lean4

/-- The coherent sheaf condition on an essentially small site can be checked after precomposing with
the equivalence with a small category.
-/
theorem precoherent_isSheaf_iff_of_essentiallySmall [EssentiallySmall C] (F : Cᵒᵖ ⥤ A) :
    IsSheaf (coherentTopology C) F ↔ IsSheaf (coherentTopology (SmallModel C)) ((equivSmallModel C).inverse.op ⋙ F) :=
  precoherent_isSheaf_iff _ _ _

Похожие утверждения