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 . It is the object through which the (bo, ff) factorization of a functor factors.
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:
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).
The full image of is equivalently the Kleisli category for the trivial -relative monad .
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.
Last revised on August 2, 2024 at 18:41:17. See the history of this page for a list of all contributions to it.