English
A sieve contains an EffectiveEpi if and only if it is a covering sieve for the regular topology.
Русский
Сито содержит эффективную эпиморфию тогда и только тогда, когда является покрывающим сито для регулярной топологии.
LaTeX
$$mem_sieves_of_hasEffectiveEpi S$$
Lean4
/-- For a preregular category, any sieve that contains an `EffectiveEpi` is a covering sieve of the
regular topology.
Note: This is one direction of `mem_sieves_iff_hasEffectiveEpi`, but is needed for the proof.
-/
theorem mem_sieves_of_hasEffectiveEpi (S : Sieve X) :
(∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) → (S ∈ (regularTopology C) X) :=
by
rintro ⟨Y, π, h⟩
have h_le : Sieve.generate (Presieve.ofArrows (fun () ↦ Y) (fun _ ↦ π)) ≤ S :=
by
rw [Sieve.generate_le_iff (Presieve.ofArrows _ _) S]
apply Presieve.le_of_factorsThru_sieve (Presieve.ofArrows _ _) S _
intro W g f
refine ⟨W, 𝟙 W, ?_⟩
cases f
exact ⟨π, ⟨h.2, Category.id_comp π⟩⟩
apply Coverage.saturate_of_superset (regularCoverage C) h_le
exact Coverage.Saturate.of X _ ⟨Y, π, rfl, h.1⟩
