Description of the covering sieves of the regular topology #
This file characterises the covering sieves of the regular topology.
Main result #
regularTopology.mem_sieves_iff_hasEffectiveEpi: a sieve is a covering sieve for the regular topology if and only if it contains an effective epi.
theorem CategoryTheory.regularTopology.mem_sieves_of_hasEffectiveEpi {C : Type u_1} [Category.{v_1, u_1} C] [Preregular C] {X : C} (S : Sieve X) :
(∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) → S ∈ (regularTopology C) X
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.
instance CategoryTheory.regularTopology.instEffectiveEpiComp {C : Type u_1} [Category.{v_1, u_1} C] [Preregular C] {X Y Y' : C} (π : Y ⟶ X) [EffectiveEpi π] (π' : Y' ⟶ Y) [EffectiveEpi π'] :
EffectiveEpi (CategoryStruct.comp π' π)
Effective epis in a preregular category are stable under composition.
theorem CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi {C : Type u_1} [Category.{v_1, u_1} C] [Preregular C] {X : C} (S : Sieve X) :
A sieve is a cover for the regular topology if and only if it contains an EffectiveEpi.