Reflecting the property of being precoherent #
We prove that given a fully faithful functor F : C ⥤ D which preserves and reflects finite
effective epimorphic families, 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 Precoherent whenever D is.
theorem
CategoryTheory.Functor.reflects_precoherent
{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.PreservesFiniteEffectiveEpiFamilies]
[F.ReflectsFiniteEffectiveEpiFamilies]
[F.EffectivelyEnough]
[CategoryTheory.Precoherent D]
[F.Full]
[F.Faithful]
: