Documentation

Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent

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] :