Essential Injective Functors

Stream: maths

[Pieter Cuijpers]

To anyone working on category theory: I can find a definition Functor.EssSurj for essential surjectivity of a functor, but I cannot find a definition for essential injectivity. More precisely, I need the definition of when a functor is an embedding. Is there someone working on this?

[Joël Riou]

We have Functor.Full, Functor.Faithful and Functor.FullyFaithful.

[Pieter Cuijpers]

We also have 'FullSubcategory' and 'WideSubcategory', but not simply 'Subcategory' it seems?

[Pieter Cuijpers]

Essential surjectivity and injectivity are about surjection and injection on objects modulo isomorphism, rather than on morphisms.

[Pieter Cuijpers]

But "EssImageSubcategory" may be in the direction I need.

[Robert Maxton]

Pieter Cuijpers said:

Essential surjectivity and injectivity are about surjection and injection on objects modulo isomorphism, rather than on morphisms.

Yes, but morphisms are enough, because as you say, essential <foo> is about objects modulo isomorphisms.
The property you want is that $FX$ and $FY$ are isomorphic (there exists an invertible morphism between them) iff $X$ and $Y$ were already isomorphic. This can be shown to be equivalent to docs#CategoryTheory.Functor.ReflectsIsomorphisms plus being full: then given some $g : FX \hom FY$, by fullness $g$ has a preimage $f$ under $F$, and since $F$ reflects isomorphisms and $g = Ff$ is iso then $f$ must have been iso as well, QED.

[Robert Maxton]

(A similar proof follows from simply being fully faithful, as any fully faithful functor reflects isomorphisms)

[Christian Merten]

If M is a monoid that is not a group and C = SingleObj M and F the endofunctor of C corresponding to the trivial monoid homomorphism(i.e. everything maps to 1), I believe F is essentially injective, but neither full nor reflects isos.