Effectively enough objects in the image of a functor #

We define the class F.EffectivelyEnough on a functor F : C ⥤ D which says that for every object in D, there exists an effective epi to it from an object in the image of F.

source

structure CategoryTheory.Functor.EffectivePresentation {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) (X : D) :

Type (max u_1 u_4)

An effective presentation of an object X with respect to a functor F is the data of an effective epimorphism of the form F.obj p ⟶ X.

p : C
The object of C giving the source of the effective epi
f : F.obj self.p ⟶ X
The morphism F.obj p ⟶ X
effectiveEpi : CategoryTheory.EffectiveEpi self.f
f is an effective epi

Instances For

source

theorem CategoryTheory.Functor.EffectivePresentation.effectiveEpi {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} {X : D} (self : F.EffectivePresentation X) :

CategoryTheory.EffectiveEpi self.f

f is an effective epi

source

class CategoryTheory.Functor.EffectivelyEnough {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) :

Prop

D has *effectively enough objects with respect to the functor F if every object has an effective presentation.

presentation : ∀ (X : D), Nonempty (F.EffectivePresentation X)
For every X : D, there exists an object p of C with an effective epi F.obj p ⟶ X.

Instances

source

theorem CategoryTheory.Functor.EffectivelyEnough.presentation {C : Type u_1} {D : Type u_2} :

∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Category.{u_4, u_2} D} {F : CategoryTheory.Functor C D} [self : F.EffectivelyEnough] (X : D), Nonempty (F.EffectivePresentation X)

For every X : D, there exists an object p of C with an effective epi F.obj p ⟶ X.

source

noncomputable def CategoryTheory.Functor.effectiveEpiOverObj {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.EffectivelyEnough] (X : D) :

F.effectiveEpiOverObj X provides an arbitrarily chosen object in the image of F equipped with an effective epimorphism F.effectiveEpiOver : F.effectiveEpiOverObj X ⟶ X.

Equations