English
If C is preregular and finitaryExtensive and HasPullback f f for all arrows f with EffectiveEpi, and s preserves finite limits, then IsSheaf(coherentTopology C) F implies IsSheaf(coherentTopology C) (F ⋙ s).
Русский
Если C — preregular, finitaryExtensive и для каждого f с effective epi выполняется HasPullback f f, а s сохраняет конечные предельные, то из IsSheaf(coherentTopology C) F следует IsSheaf(coherentTopology C) (F ⋙ s).
LaTeX
$$$\text{IsSheaf(coherentTopology C) } F \Rightarrow \text{IsSheaf(coherentTopology C) } (F \circ s)$$$
Lean4
theorem isSheaf_coherent_of_hasPullbacks_comp [Preregular C] [FinitaryExtensive C]
[h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f] [PreservesFiniteLimits s]
(hF : IsSheaf (coherentTopology C) F) : IsSheaf (coherentTopology C) (F ⋙ s) :=
by
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition (h := h)] at hF ⊢
have := hF.1
refine ⟨inferInstance, fun _ _ π _ c hc ↦ ⟨?_⟩⟩
exact isLimitForkMapOfIsLimit s _ (hF.2 π c hc).some
