CategoryTheory.Presieve.regular.single_epi

theorem CategoryTheory.Presieve.regular.single_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {X : C} {R : CategoryTheory.Presieve X} [self : R.regular], ∃ Y f, (R = CategoryTheory.Presieve.ofArrows (fun x => Y) fun x => f) ∧ CategoryTheory.EffectiveEpi f

This theorem states that for any category `C`, object `X` in `C` and a `Presieve` `R` on `X` that is regular, there exists an object `Y` in `C` and a morphism `f` from `Y` to `X` such that `R` consists of this single morphism `f`, and `f` is an effective epimorphism. Here, a `Presieve` on `X` is a collection of arrows (morphisms) all with codomain `X`. An effective epimorphism is a morphism that is right-cancellable, i.e., for any pair of morphisms `g`, `h` such that `f ∘ g = f ∘ h`, we have `g = h`. The regularity condition on `R` is not specified in the provided Lean code.

More concisely: For any regular presheaf `R` on object `X` in a category `C`, there exists an effective epimorphism `f : Y → X` in `C` such that the set of morphisms in `R` is exactly the set containing `f`.