Reflecting the property of being preregular #
We prove that given a fully faithful functor F : C ⥤ D, with Preregular D, such that for every
object X of D there exists an object W of C with an effective epi π : F.obj W ⟶ X, the
category C is Preregular.
theorem
CategoryTheory.Functor.reflects_preregular
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
[F.PreservesEffectiveEpis]
[F.ReflectsEffectiveEpis]
[F.EffectivelyEnough]
[CategoryTheory.Preregular D]
[F.Full]
[F.Faithful]
: