Theorems · Theorem · category theory

CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C] {X : C}
  (S : CategoryTheory.Sieve X),
  S ∈ (CategoryTheory.regularTopology C) X ↔ ∃ Y π, CategoryTheory.EffectiveEpi π ∧ S.arrows π

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

Defined in

Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preregular