Essential image of a functor #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The essential image
ess_image of a functor consists of the objects in the target category which
are isomorphic to an object in the image of the object function.
This, for instance, allows us to talk about objects belonging to a subcategory expressed as a
functor rather than a subtype, preserving the principle of equivalence. For example this lets us
define exponential ideals.
The essential image can also be seen as a subcategory of the target category, and witnesses that a functor decomposes into a essentially surjective functor and a fully faithful functor. (TODO: show that this decomposition forms an orthogonal factorisation system).
The essential image of a functor
F consists of those objects in the target category which are
isomorphic to an object in the image of the function
F.obj. In other words, this is the closure
under isomorphism of the function
This is the "non-evil" way of describing the image of a functor.
Get the witnessing object that
Y is in the subcategory given by
Extract the isomorphism between
F.obj h.witness and
Being in the essential image is a "hygenic" property: it is preserved under isomorphism.
Y is in the essential image of
F then it is in the essential image of
F' as long as
F ≅ F'.
The essential image of a functor, interpreted of a full subcategory of the target category.
The essential image as a subcategory has a fully faithful inclusion into the target category.
Given a functor
F : C ⥤ D, we have an (essentially surjective) functor from
C to the essential
F factorises through its essential image, where the first functor is essentially
surjective and the second is fully faithful.
F : C ⥤ D is essentially surjective if every object of
D is in the essential image
F. In other words, for every
Y : D, there is some
X : C with
F.obj X ≅ Y.
Instances of this typeclass
Given an essentially surjective functor, we can find a preimage for every object
Y in the
codomain. Applying the functor to this preimage will yield an object isomorphic to
Applying an essentially surjective functor to a preimage of
Y yields an object that is
The induced functor of a full functor is full