English
Assume preregular C, finitaryExtensive C, and a condition that HasPullback f f holds for all arrows f that are effective epis. Then IsSheaf(coherentTopology C) F is equivalent to (PreservesFiniteProducts F) ∧ EqualizerCondition F.
Русский
Пусть C — preregular, finitaryExtensive, и для каждого стрелочного f, являющегося эффективной эпиморфией, выполняется HasPullback f f. Тогда IsSheaf(coherentTopology C) F эквивалентно (PreservesFiniteProducts F) ∧ EqualizerCondition F.
LaTeX
$$$IsSheaf(coherentTopology\, C)\, F \iff (PreservesFiniteProducts\, F) \wedge EqualizerCondition\, F$$$
Lean4
theorem isSheaf_iff_preservesFiniteProducts_and_equalizerCondition [Preregular C] [FinitaryExtensive C]
[h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f] :
IsSheaf (coherentTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F :=
by
rw [isSheaf_coherent_iff_regular_and_extensive]
exact and_congr (isSheaf_iff_preservesFiniteProducts _) (@equalizerCondition_iff_isSheaf _ _ _ _ F _ h).symm
