English
For a precoherent category C and a presheaf P, P is a sheaf for the coherent topology iff for all finite families forming an effective epi in X, the corresponding presieve is a sheaf for P.
Русский
Для предкоерентной категории C и предсет P выполнение условия шейфа относительно когерентной топологии эквивалентно тому, что для любых конечных семей, образующих эффективный эпиморфизм в X, соответствующее предсет является шейфом для P.
LaTeX
$$$\mathrm{IsSheaf}(\mathrm{coherentTopology}\ C, P) \iff \forall B, \alpha, X, \pi, \mathrm{EffectiveEpiFamily}\ X \pi \to \mathrm{IsSheafFor}(P, \mathrm{Presieve.ofArrows}(X, \pi))$$$
Lean4
theorem isSheaf_coherent (P : Cᵒᵖ ⥤ Type w) :
Presieve.IsSheaf (coherentTopology C) P ↔
(∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → (X a ⟶ B)),
EffectiveEpiFamily X π → (Presieve.ofArrows X π).IsSheafFor P) :=
by
constructor
· intro hP B α _ X π h
simp only [coherentTopology, Presieve.isSheaf_coverage] at hP
apply hP
exact ⟨α, inferInstance, X, π, rfl, h⟩
· intro h
simp only [coherentTopology, Presieve.isSheaf_coverage]
rintro B S ⟨α, _, X, π, rfl, hS⟩
exact h _ _ _ _ hS
