English
For a precoherent category, if a sieve on X contains an EffectiveEpiFamily arrows, then it belongs to the coherent topology on X.
Русский
Для предкоерентной категории, если на X сита содержатся стрелки, образующие эффективную эпиморфную семью, то такое множество относится к когерентной топологии на X.
LaTeX
$$$(\exists α, Finite α, Y, π,\; EffectiveEpiFamily Y π \wedge \forall a, (S.arrows)(π a)) \Rightarrow S \in (\mathrm{coherentTopology}\ C) X$$$
Lean4
/-- For a precoherent category, any sieve that contains an `EffectiveEpiFamily` is a sieve of the
coherent topology.
Note: This is one direction of `mem_sieves_iff_hasEffectiveEpiFamily`, but is needed for the proof.
-/
theorem mem_sieves_of_hasEffectiveEpiFamily (S : Sieve X) :
(∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → (Y a ⟶ X)),
EffectiveEpiFamily Y π ∧ (∀ a : α, (S.arrows) (π a))) →
(S ∈ (coherentTopology C) X) :=
by
intro ⟨α, _, Y, π, hπ⟩
apply (coherentCoverage C).mem_toGrothendieck_sieves_of_superset (R := Presieve.ofArrows Y π)
· exact fun _ _ h ↦ by cases h; exact hπ.2 _
· exact ⟨_, inferInstance, Y, π, rfl, hπ.1⟩
