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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preregular C] {X : C} (S : CategoryTheory.Sieve X) : (∃ (Y : C) (π : Y ⟶ X), CategoryTheory.EffectiveEpi π ∧ S.arrows π) → S ∈ (CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preregular C] {X Y Y' : C} (π : Y ⟶ X) [CategoryTheory.EffectiveEpi π] (π' : Y' ⟶ Y) [CategoryTheory.EffectiveEpi π'] : CategoryTheory.EffectiveEpi (CategoryTheory.CategoryStruct.comp π' π)

Effective epis in a preregular category are stable under composition.

Equations

• ⋯ = ⋯

theorem CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preregular C] {X : C} (S : CategoryTheory.Sieve X) : S ∈ (CategoryTheory.regularTopology C) X ↔ ∃ (Y : C) (π : Y ⟶ X), CategoryTheory.EffectiveEpi π ∧ S.arrows π

A sieve is a cover for the regular topology if and only if it contains an EffectiveEpi.