I'm having trouble understanding why the "essential image" is defined the way it is.
The nlab article gives the following definition:
(A concrete realization of) the essential image of a functor $F: A\to B$ between categories or $n$-categories is the smallest replete subcategory of the target $n$-category $B$ containing the image of $F$
This obviously breaks the principle of equivalence as stated later in the article.
When I think about how to define the essential image, the first thing that comes to mind is if we remember the identification of the functor as a new functor from the source to the essential image - then we don't have to break equivalence:
Say: The "essential image" of a functor $F:A\to B$ is the initial object in the category of triples $(D, i:D\hookrightarrow B, F':A \to D)$ such that $F= i\circ F'$ (with morphisms the same as in $Cat/B$ that also require post composing them with $F'$ of the domain gives the $F'$ of the codomain)
It exists as the classical image of $F$ satisfies the universal property.
All the different choices of an initial object form a contractible groupoid whose skeleton yields a subcategory of the classical essential image, as the classical image satisfies the universal property and is contained in the classical essential image (but this is not obvious these are equivalent, I suspect in general they are not, but came short of examples).
Questions:
- How large is the difference between this definition and the classical one? To break this down a little:
a. For what categories we have different subcategories of the two constructions (I believe this highly depends on AC to build pathological cases)
b. (Aside) Is this difference between the definitions equivalent to AC?
- Which definition behaves better (this is vague in purpose as there are many interpretations to the question that give different points of view on "which" definition is "the right one").
An argument for this new one is that this definition respects the principle of equivalence.
An argument for the classical definition is simplicity - the classical definition is a subcategory and not an equivalence class of subcategories equipped with extra information)?
Other arguments I can think about can come from higher categorial properties:
For example, gluing essential images (in both definitions) of different functors into a pseudofunctor - when can you do this?