Theorems · Theorem · category theory

CategoryTheory.regularTopology.mem_sieves_of_hasEffectiveEpi

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C] {X : C}
  (S : CategoryTheory.Sieve X),
  (∃ Y π, 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.

Defined in

Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Cited by

1 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Preregular