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
- 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
More generally this applies to objects essentially in the reflective subcategory, see
A is essentially in the image of a reflective functor
η_A is an isomorphism.
This gives that the "witness" for
A being in the essential image can instead be given as the
A, with the isomorphism as
B in the reflective subcategory, we automatically have that
ε_B is an iso.)
η_A is an isomorphism, then
A is in the essential image of
η_A is a split monomorphism, then
A is in the reflective subcategory.
Composition of reflective functors.
(Implementation) Auxiliary definition for
The description of the inverse of the bijection
i has a reflector
L, then the function
(i.obj (L.obj A) ⟶ B) → (A ⟶ B) given by
η.app A is a bijection provided
B is in the essential image of
That is, the function
λ (f : i.obj (L.obj A) ⟶ B), η.app A ≫ f is bijective, as long as
B is in
the essential image of
This definition gives an equivalence: the key property that the inverse can be described
nicely is shown in
This establishes there is a natural bijection
(A ⟶ B) ≃ (i.obj (L.obj A) ⟶ B). In other words,
from the point of view of objects in
i.obj (L.obj A) look the same: specifically
η.app A is an isomorphism.
- category_theory.unit_comp_partial_bijective A hB = (((category_theory.iso.refl A).hom_congr (category_theory.functor.ess_image.get_iso hB).symm).trans (category_theory.unit_comp_partial_bijective_aux A (category_theory.functor.ess_image.witness hB))).trans ((category_theory.iso.refl (i.obj ((category_theory.left_adjoint i).obj A))).hom_congr (category_theory.functor.ess_image.get_iso hB))