English
Let J be a Grothendieck topology on a category C and P' an abelian-presheaf valued in A'. Then the standard sheaf condition is equivalent to the equalizer-based (isSheaf') formulation for P'.
Русский
Пусть J — топология Гротендикa на категорию C и P' — абелева-предображение с кодировкой значений в A'. Тогда стандартное условие sheaf эквивалентно условию, заданному через равнозначник (isSheaf'), для P'.
LaTeX
$$$\IsSheaf(J, P') \iff \IsSheaf'(J, P')$$$
Lean4
/-- The equalizer definition of a sheaf given by `isSheaf'` is equivalent to `isSheaf`. -/
theorem isSheaf_iff_isSheaf' : IsSheaf J P' ↔ IsSheaf' J P' :=
by
constructor
· intro h U R hR
refine ⟨?_⟩
apply coyonedaJointlyReflectsLimits
intro X
have q : Presieve.IsSheafFor (P' ⋙ coyoneda.obj X) _ := h X.unop _ hR
rw [← Presieve.isSheafFor_iff_generate] at q
rw [Equalizer.Presieve.sheaf_condition] at q
replace q := Classical.choice q
apply (isSheafForIsSheafFor' _ _ _ _).symm q
· intro h U X S hS
rw [Equalizer.Presieve.sheaf_condition]
refine ⟨?_⟩
refine isSheafForIsSheafFor' _ _ _ _ ?_
letI := preservesSmallestLimits_of_preservesLimits (coyoneda.obj (op U))
apply isLimitOfPreserves
apply Classical.choice (h _ S.arrows _)
simpa
