Reflective functors #
Basic properties of reflective functors, especially those relating to their essential image.
Note properties of reflective functors relating to limits and colimits are included in
category_theory.monad.limits
.
- to_is_right_adjoint : category_theory.is_right_adjoint R
- to_full : category_theory.full R
- to_faithful : category_theory.faithful R
A functor is reflective, or a reflective inclusion, if it is fully faithful and right adjoint.
For a reflective functor i
(with left adjoint L
), with unit η
, we have η_iL = iL η
.
When restricted to objects in D
given by i : D ⥤ C
, the unit is an isomorphism. In other words,
η_iX
is an isomorphism for any X
in D
.
More generally this applies to objects essentially in the reflective subcategory, see
functor.ess_image.unit_iso
.
Equations
- category_theory.is_iso_unit_obj = category_theory.is_iso_unit_obj._proof_1.mpr category_theory.is_iso.inv_is_iso
If A
is essentially in the image of a reflective functor i
, then η_A
is an isomorphism.
This gives that the "witness" for A
being in the essential image can instead be given as the
reflection of A
, with the isomorphism as η_A
.
(For any B
in the reflective subcategory, we automatically have that ε_B
is an iso.)
If η_A
is an isomorphism, then A
is in the essential image of i
.
If η_A
is a split monomorphism, then A
is in the reflective subcategory.
Composition of reflective functors.