The full image should be taken as equipped with a functor to , which acts as on objects and the identity on morphisms. This functor is fully faithful, so is always equivalent to a full subcategory of .
From in internal point of view, if is the category with object set and a unique arrow between any ordered pair of objects (that is, ), the full image can be defined as a pullback:
in the category Cat. Here is the object component of and is the obvious functor. This determines up to canonical isomorphism as a strict category (or other internal category).
Full images of forgetful functors
Let be interpreted as a forgetful functor, so that the objects of are thought of as objects of with some stuff, structure, property. Then the full image of consists of objects of with only a property: specifically the property that they are capable of taking the stuff or structure of being an object of .
For example, any inhabited set is capable of taking the structure of a group (at least, assuming the axiom of choice). So the full image of the forgetful functor from Grp to Set is equivalent to the category of inhabited sets.
Revised on April 13, 2016 15:39:24
by Eponymous Howard?