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.

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

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

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.

theorem CategoryTheory.Functor.EffectivelyEnough.presentation {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} [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.

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

• F.effectiveEpiOverObj X = F.obj ⋯.some.p

noncomputable def CategoryTheory.Functor.effectiveEpiOver {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 ⟶ X

The epimorphism F.effectiveEpiOver : F.effectiveEpiOverObj X ⟶ X from the arbitrarily chosen object in the image of F over X.

Equations

• F.effectiveEpiOver X = ⋯.some.f

instance CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOver {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] (F : CategoryTheory.Functor C D) [F.EffectivelyEnough] (X : D) : CategoryTheory.EffectiveEpi (F.effectiveEpiOver X)

Equations

• ⋯ = ⋯

def CategoryTheory.Functor.equivalenceEffectivePresentation {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (e : C ≌ D) (X : D) : e.functor.EffectivePresentation X

An effective presentation of an object with respect to an equivalence of categories.

Equations

• CategoryTheory.Functor.equivalenceEffectivePresentation e X = { p := e.inverse.obj X, f := e.counit.app X, effectiveEpi := ⋯ }

instance CategoryTheory.Functor.instEffectivelyEnoughOfIsEquivalence {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.IsEquivalence] : F.EffectivelyEnough

Equations

• ⋯ = ⋯