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.

TODO

• Show that Stonean.toCompHaus and Stonean.toProfinite satisfy this property.
• Use this as one of the sufficient conditions for a functor to induce an equivalence of sheaf categories of coherent and regular sheaves.

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

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 (CategoryTheory.Functor.EffectivePresentation F 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) [CategoryTheory.Functor.EffectivelyEnough F] (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

• CategoryTheory.Functor.effectiveEpiOverObj F X = F.obj (Nonempty.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) [CategoryTheory.Functor.EffectivelyEnough F] (X : D) : CategoryTheory.Functor.effectiveEpiOverObj F X ⟶ X

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

Equations

• CategoryTheory.Functor.effectiveEpiOver F X = (Nonempty.some ⋯).f

instance CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOverObjEffectiveEpiOver {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) [CategoryTheory.Functor.EffectivelyEnough F] (X : D) : CategoryTheory.EffectiveEpi (CategoryTheory.Functor.effectiveEpiOver F 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) : CategoryTheory.Functor.EffectivePresentation e.functor 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.instEffectivelyEnough {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) [CategoryTheory.IsEquivalence F] : CategoryTheory.Functor.EffectivelyEnough F

Equations

• ⋯ = ⋯