Full images of functors
The full image of a functor is a version of its image? that gets its objects from the functor's source but its morphisms from the functor's target .
You may think of it as (up to equivalence) the full subcategory of whose objects lie in the literal image of .
We may call it the -image of the functor, because it reduces (again, up to equivalence) to the ordinary image for a functor between -categories.
Let and be categories, and let be a functor. Then the full image of is the category with:
- as objects, the objects of ;
- as morphisms from to , the morphisms in from to .
If is a subcategory of , then the full image is the full subcategory of whose objects belong to .
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.