English
If HasPullbacks holds for all arrows and s preserves finite limits, then IsSheaf(coherentTopology C) F implies IsSheaf(coherentTopology C) (F ⋙ s).
Русский
При условии HasPullbacks для всех стрелок и сохранении конечных ограничений функционалом s, IsSheaf(coherentTopology C) F влечет IsSheaf(coherentTopology C) (F ⋙ s).
LaTeX
$$$\text{HasPullbacks} \Rightarrow (F \mapsto F \circ s) \text{ preserves isSheaf}$$$
Lean4
instance [Preregular C] [FinitaryExtensive C] [h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f]
[PreservesFiniteLimits s] : (coherentTopology C).HasSheafCompose s where
isSheaf F hF := isSheaf_coherent_of_hasPullbacks_comp (h := h) F s hF
