English
For a presheaf F on C with preregular C and pullbacks preserved by EffectiveEpi maps, F satisfies the equalizer condition iff it is a sheaf for the regular topology on C.
Русский
Для префунктора F над C, где C является прегеорегулярной, и где отображения с эвфективной эпиморфией сохраняют pullbacks, условие равнозначителя эквивалентно тому, что F является sheaf для регулярной топологии на C.
LaTeX
$$EqualizerCondition F ↔ Presheaf.IsSheaf (regularTopology C) F$$
Lean4
theorem equalizerCondition_iff_isSheaf (F : Cᵒᵖ ⥤ D) [Preregular C]
[∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f] :
EqualizerCondition F ↔ Presheaf.IsSheaf (regularTopology C) F :=
by
dsimp [regularTopology]
rw [Presheaf.isSheaf_iff_isLimit_coverage]
constructor
· rintro hF X _ ⟨Y, f, rfl, _⟩
exact (equalizerConditionMap_iff_nonempty_isLimit F f).1 (hF f)
· intro hF Y X f _
exact (equalizerConditionMap_iff_nonempty_isLimit F f).2 (hF _ ⟨_, f, rfl, inferInstance⟩)
